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-10-06 11:53:20 +02:00
parent 4f823c6342
commit d04ad57ee7
2 changed files with 20 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
docs/smtchecker.rst
View File

@ -412,7 +412,7 @@ is already "locked", so it would not be possible to change the value of ``x``,
regardless of what the unknown called code does.
If we "forget" to use the ``mutex`` modifier on function ``set``, the
SMTChecker is able to synthesize the behavior of the externally called code so
SMTChecker is able to synthesize the behaviour of the externally called code so
that the assertion fails:
.. code-block:: text
@ -518,6 +518,23 @@ which has the following form:
"source2.sol": ["contract2", "contract3"]
}
Reported Inferred Inductive Invariants
======================================
For properties that were proved safe with the CHC engine,
the SMTChecker can retrieve inductive invariants that were inferred by the Horn
solver as part of the proof.
Currently two types of invariants can be reported to the user:
- Contract Invariants: these are properties over the contract's state variables
that are true before and after every possible transaction that the contract may ever run. For example, ``x >= y``, where ``x`` and ``y`` are a contract's state variables.
- Reentrancy Properties: they represent the behavior of the contract
in the presence of external calls to unknown code. These properties can express a relation
between the value of the state variables before and after the external call, where the external call is free to do anything, including making reentrant calls to the analyzed contract. Primed variables represent the state variables' values after said external call. Example: ``lock -> x = x'``.
The user can choose the type of invariants to be reported using the CLI option ``--model-checker-invariants "contract,reentrancy"`` or as an array in the field ``settings.modelChecker.invariants`` in the :ref:`JSON input<compiler-api>`.
By default the SMTChecker does not report invariants.
Division and Modulo With Slack Variables
========================================

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

@ -418,6 +418,8 @@ Input Description
"divModWithSlacks": true,
// Choose which model checker engine to use: all (default), bmc, chc, none.
"engine": "chc",
// Choose which types of invariants should be reported to the user: contract, reentrancy.
"invariants": ["contract", "reentrancy"],
// Choose whether to output all unproved targets. The default is `false`.
"showUnproved": true,
// Choose which solvers should be used, if available.