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

Update docs

Browse Source
This commit is contained in:
Leonardo Alt 2021-03-31 17:20:30 +02:00
parent c43ae60938
commit d89be74e4a
1 changed files with 20 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

41
docs/smtchecker.rst
View File

@ -39,8 +39,17 @@ The potential warnings that the SMTChecker reports are:
- ``<failing property> happens here.``. This means that the SMTChecker proved that a certain property fails. A counterexample may be given, however in complex situations it may also not show a counterexample. This result may also be a false positive in certain cases, when the SMT encoding adds abstractions for Solidity code that is either hard or impossible to express.
- ``<failing property> might happen here``. This means that the solver could not prove either case within the given timeout. Since the result is unknown, the SMTChecker reports the potential failure for soundness. This may be solved by increasing the query timeout, but the problem might also simply be too hard for the engine to solve.
It is currently an experimental feature, therefore in order to use it you need
to enable it via :ref:`a pragma directive<smt_checker>`.
To enable the SMTChecker, you must select :ref:`which engine should run<smtchecker_engines>`,
where the default is no engine. Selecting the engine enables the SMTChecker on all files.
.. note::
Prior to Solidity 0.8.4, the default way to enable the SMTChecker was via
``pragma experimental SMTChecker;`` and only the contracts containing the
pragma would be analyzed. That pragma has been deprecated, and although it
still enables the SMTChecker for backwards compatibility, it will be removed
in Solidity 0.9.0. Note also that now using the pragma even in a single file
enables the SMTChecker for all files.
.. note::
The lack of warnings for a verification target represents an undisputed
@ -62,9 +71,8 @@ Overflow
.. code-block:: Solidity
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
pragma experimental SMTChecker;
// This may report a warning if no SMT solver is available.
contract Overflow {
uint immutable x;
@ -110,9 +118,8 @@ the SMTChecker proves that no overflow is reachable (by not reporting warnings):
.. code-block:: Solidity
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
pragma experimental SMTChecker;
// This may report a warning if no SMT solver is available.
contract Overflow {
uint immutable x;
@ -149,9 +156,8 @@ definition to see what results come out!
.. code-block:: Solidity
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
pragma experimental SMTChecker;
// This may report a warning if no SMT solver is available.
contract Monotonic {
function f(uint _x) internal pure returns (uint) {
@ -172,9 +178,8 @@ equal every element in the array.
.. code-block:: Solidity
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
pragma experimental SMTChecker;
// This may report a warning if no SMT solver is available.
contract Max {
function max(uint[] memory _a) public pure returns (uint) {
@ -206,9 +211,8 @@ For example, changing the code to
.. code-block:: Solidity
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
pragma experimental SMTChecker;
// This may report a warning if no SMT solver is available.
contract Max {
function max(uint[] memory _a) public pure returns (uint) {
@ -259,10 +263,8 @@ below.
.. code-block:: Solidity
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
pragma experimental SMTChecker;
// This may report a warning if no SMT solver is available.
contract Robot {
int x = 0;
@ -361,9 +363,8 @@ anything, including reenter the caller contract.
.. code-block:: Solidity
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
pragma experimental SMTChecker;
// This may report a warning if no SMT solver is available.
interface Unknown {
function run() external;
@ -469,6 +470,8 @@ 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.
.. _smtchecker_engines:
Model Checking Engines
======================
@ -624,8 +627,6 @@ not mean loss of proving power.
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
pragma experimental SMTChecker;
// This may report a warning if no SMT solver is available.
contract Recover
{
@ -673,8 +674,6 @@ types.
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;
pragma experimental SMTChecker;
// This will report a warning
contract Aliasing
{