cerc-io/solidity
11
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

Changelog and docs

Browse Source
This commit is contained in:
Leo Alt 2022-05-15 17:45:52 +02:00
parent ee9773bcff
commit d70d137898
2 changed files with 4 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Changelog.md
View File

@ -12,7 +12,9 @@ Compiler Features:
* Assembly-Json: Export: Include source list in `sourceList` field.
* Commandline Interface: option ``--pretty-json`` works also with the following options: ``--abi``, ``--asm-json``, ``--ast-compact-json``, ``--devdoc``, ``--storage-layout``, ``--userdoc``.
* SMTChecker: Support ``abi.encodeCall`` taking into account the called selector.
* SMTChecker: Use the Horn solver Eldarica via its binary if installed in the system. It can be enabled via the CLI option ``--model-checker-solvers eld`` or the JSON field ``settings.modelChecker.solvers=["eld"]``.
* SMTChecker: New trusted mode that assumes that any compile-time available code is the actual used code even in external calls. This can be used via the CLI option ``--model-checker-ext-calls=trusted`` or the JSON field ``settings.modelChecker.extCalls: "trusted"``.
>>>>>>> e0e01b952 (Changelog and docs)
* Language Server: Allow full filesystem access to language server.

3
docs/smtchecker.rst
View File

@ -653,10 +653,11 @@ which is primarily an SMT solver and makes `Spacer
<https://github.com/uuverifiers/eldarica>`_ which does both.
The user can choose which solvers should be used, if available, via the CLI
option ``--model-checker-solvers {all,cvc4,smtlib2,z3}`` or the JSON option
option ``--model-checker-solvers {all,cvc4,eld,smtlib2,z3}`` or the JSON option
``settings.modelChecker.solvers=[smtlib2,z3]``, where:
- ``cvc4`` is only available if the ``solc`` binary is compiled with it. Only BMC uses ``cvc4``.
- ``eld`` is used via its binary which must be installed in the system. Only CHC uses ``eld``.
- ``smtlib2`` outputs SMT/Horn queries in the `smtlib2 <http://smtlib.cs.uiowa.edu/>`_ format.
These can be used together with the compiler's `callback mechanism <https://github.com/ethereum/solc-js>`_ so that
any solver binary from the system can be employed to synchronously return the results of the queries to the compiler.