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

Merge pull request #7995 from ethereum/smt_layout_docs

Browse Source 
Update contract layout SMTChecker
This commit is contained in:
chriseth 2019-12-12 16:56:50 +01:00 committed by GitHub
commit c8a59d9fd3
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 4 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
docs/layout-of-source-files.rst
View File

@ -87,8 +87,10 @@ This component has to be enabled when the Solidity compiler is built
and therefore it is not available in all Solidity binaries. and therefore it is not available in all Solidity binaries.
The :ref:`build instructions<smt_solvers_build>` explain how to activate this option. The :ref:`build instructions<smt_solvers_build>` explain how to activate this option.
It is activated for the Ubuntu PPA releases in most versions, It is activated for the Ubuntu PPA releases in most versions,
but not for solc-js, the Docker images, Windows binaries or the but not for the Docker images, Windows binaries or the
statically-built Linux binaries. statically-built Linux binaries. It can be activated for solc-js via the
`smtCallback <https://github.com/ethereum/solc-js#example-usage-with-smtsolver-callback>`_ if you have an SMT solver
installed locally and run solc-js via node (not via the browser).
If you use ``pragma experimental SMTChecker;``, then you get additional If you use ``pragma experimental SMTChecker;``, then you get additional
:ref:`safety warnings<formal_verification>` which are obtained by querying an :ref:`safety warnings<formal_verification>` which are obtained by querying an