add changelog entry and docs note

This commit is contained in:
Leo Alt 2022-05-11 17:16:10 +02:00
parent 60b405aaa9
commit 2fe143f7d0
2 changed files with 6 additions and 0 deletions

View File

@ -15,6 +15,7 @@ Bugfixes:
* Type Checker: Properly check restrictions of ``using ... global`` in conjunction with libraries. * Type Checker: Properly check restrictions of ``using ... global`` in conjunction with libraries.
* Assembly-Json: Fix assembly json export to store jump types of operations in `jumpType` field instead of `value`. * Assembly-Json: Fix assembly json export to store jump types of operations in `jumpType` field instead of `value`.
* SMTChecker: Fix bug when z3 is selected but not available at runtime. * SMTChecker: Fix bug when z3 is selected but not available at runtime.
* SMTChecker: Fix ABI compatibility with z3 >=4.8.16.
* TypeChecker: Convert parameters of function type to how they would be called for ``abi.encodeCall``. * TypeChecker: Convert parameters of function type to how they would be called for ``abi.encodeCall``.
* View Pure Checker: Mark ``returndatasize`` and ``returndatacopy`` as view to disallow them in inline assembly blocks in pure functions. * View Pure Checker: Mark ``returndatasize`` and ``returndatacopy`` as view to disallow them in inline assembly blocks in pure functions.

View File

@ -629,6 +629,11 @@ option ``--model-checker-solvers {all,cvc4,smtlib2,z3}`` or the JSON option
- if a dynamic ``z3`` library of version 4.8.x is installed in a Linux system (from Solidity 0.7.6); - if a dynamic ``z3`` library of version 4.8.x is installed in a Linux system (from Solidity 0.7.6);
- statically in ``soljson.js`` (from Solidity 0.6.9), that is, the Javascript binary of the compiler. - statically in ``soljson.js`` (from Solidity 0.6.9), that is, the Javascript binary of the compiler.
.. note::
z3 version 4.8.16 broke ABI compatibility with previous versions and cannot
be used with solc <=0.8.13. If you are using z3 >=4.8.16 please use solc
>=0.8.14.
Since both BMC and CHC use ``z3``, and ``z3`` is available in a greater variety Since both BMC and CHC use ``z3``, and ``z3`` is available in a greater variety
of environments, including in the browser, most users will almost never need to be of environments, including in the browser, most users will almost never need to be
concerned about this option. More advanced users might apply this option to try concerned about this option. More advanced users might apply this option to try