cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Docs

Browse Source
This commit is contained in:
Leo Alt 2021-07-28 18:58:03 +02:00
parent 3c1f555f71
commit 847dd5cf92
2 changed files with 10 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
docs/smtchecker.rst
View File

@ -474,6 +474,14 @@ A common subset of targets might be, for example:
There is no precise heuristic on how and when to split verification targets,
but it can be useful especially when dealing with large contracts.
Unproved Targets
================
If there are any unproved targets, the SMTChecker issues one warning stating
how many unproved targets there are. If the user wishes to see all the specific
unproved targets, the CLI option ``--model-checker-show-unproved true`` and
the JSON option ``settings.modelChecker.showUnproved = true`` can be used.
Verified Contracts
==================

2
docs/using-the-compiler.rst
View File

@ -402,6 +402,8 @@ Input Description
},
// Choose which model checker engine to use: all (default), bmc, chc, none.
"engine": "chc",
// Choose whether to output all unproved targets. The default is `false`.
"showUnproved": true,
// Choose which targets should be checked: constantCondition,
// underflow, overflow, divByZero, balance, assert, popEmptyArray, outOfBounds.
// If the option is not given all targets are checked by default.