Commit Graph

22219 Commits

Author SHA1 Message Date
Matheus Aguiar
9465feecd8 Revert "Disallow RETURNDATASIZE and RETURNDATACOPY in inline assembly blocks in pure functions"
This reverts commit f567eb1fb2.

Correcting Bugfixes section of Changelog.
2022-05-15 19:00:22 +02:00
Daniel Kirchner
d9c46f444b Update docker images for new z3 version. 2022-05-15 19:00:22 +02:00
Daniel Kirchner
33a0f9c02a Update Z3 deps ppa script. 2022-05-15 19:00:22 +02:00
alpharush
6414891d79 document that pop does not return last element
It's already documented for push and this would clarify my incorrect assumption (that pop returns a value as in other languages) that caused confusion with https://github.com/ethereum/solidity/issues/13017
2022-05-15 19:00:22 +02:00
Leo Alt
673e9fc0e2 Update tests and hashes for z3 4.8.17 2022-05-15 19:00:21 +02:00
Daniel Kirchner
16f58bca72 Increase CircleCI node size for soltest_all runs. 2022-05-15 19:00:08 +02:00
Daniel Kirchner
824b71c5e5 Bug list entry, changelog entry and tests. 2022-05-15 19:00:08 +02:00
Daniel Kirchner
cee2427771 Bugfix. 2022-05-15 19:00:08 +02:00
Daniel Kirchner
634c7f036c Test case for the buggy behaviour. 2022-05-15 19:00:08 +02:00
Leo Alt
b5a1de909a fixup Changelog 2022-05-15 18:59:45 +02:00
Leo Alt
321bf8a595 Increase memory for clang tests 2022-05-12 17:37:03 +02:00
Leo Alt
d85494a77d adjust nondet 2022-05-12 17:35:44 +02:00
Leo Alt
0d0add2afc more smtchecker tests 2022-05-12 15:52:29 +02:00
Leo Alt
98930344e8 new tests with address state variables 2022-05-12 15:19:51 +02:00
Leo Alt
ff01c7275c fixup new tests external calls 2022-05-12 15:19:51 +02:00
Leo Alt
5daa97f417 fixup external low calls 2022-05-12 15:19:51 +02:00
Leo Alt
7092caf6bf Adjust tests for nondeterminism 2022-05-12 15:19:51 +02:00
Leo Alt
17add47a27 Fix compilation after rebase 2022-05-12 15:19:51 +02:00
Leo Alt
671adfb644 Havoc the state when state variables of reference type contain contract type 2022-05-12 15:19:51 +02:00
Leo Alt
43e08ba243 Fix getters to this 2022-05-12 15:19:51 +02:00
Leo Alt
e7dede36d0 adjust old tests 2022-05-12 15:19:51 +02:00
Leo Alt
d982e1613c commandline tests 2022-05-12 15:19:51 +02:00
Leo Alt
ba4173cd8a Add new tests with semantic this and indirect storage changes 2022-05-12 15:19:51 +02:00
Leo Alt
8234e238b2 Docs 2022-05-12 15:19:51 +02:00
Leo Alt
8cb5f04356 Changelog 2022-05-12 15:19:51 +02:00
Leo Alt
154e7619e0 Add smtchecker isoltest options for contract and trusted external calls 2022-05-12 15:19:51 +02:00
Leo Alt
9c7e1bbbb5 Support getters in trusted mode too 2022-05-12 15:19:51 +02:00
Leo Alt
4b1cfcd54e Adjust tests/tools 2022-05-12 15:19:51 +02:00
Leo Alt
397bd7da4f Add CLI option for smtchecker trusted external calls 2022-05-12 15:19:51 +02:00
Leo Alt
d4e4189a85 Adjust counterexamples for synthesized calls to external contracts that are state variables in the analyzed contract 2022-05-12 15:19:51 +02:00
Leo Alt
a66ba81dad State variables of contract type may have their state changed between txs of the analyzed contract in trusted mode 2022-05-12 15:19:51 +02:00
Leo Alt
99e7622a89 Support external calls as trusted code 2022-05-12 15:19:51 +02:00
Leo Alt
4fa765172c Refactor usesStaticCall 2022-05-12 15:19:51 +02:00
Leo Alt
e0cda47603 Support deployment 2022-05-12 15:19:51 +02:00
Leo Alt
287ea63cde Create setting for trusted/untrusted external calls 2022-05-12 15:19:51 +02:00
Leo Alt
37f6dc1f88 Add storage to state 2022-05-12 15:19:51 +02:00
Leo Alt
08781eb8f5 Extract contractAddressValue into own function 2022-05-12 15:19:51 +02:00
Leo
2aba061bde
Merge pull request #12967 from ethereum/update_z3_docker
Update docker z3 version 4.8.16
2022-05-12 15:23:03 +02:00
Leo
96bf85b35b
Merge pull request #13012 from ethereum/z3-use-rebuilt-buildpack-images
Switch to newly built buildpack-deps images with Z3 4.8.16 in CI
2022-05-12 15:16:12 +02:00
Leo
80a055103e
Merge pull request #13009 from ethereum/smt_support_z3_16
Support new z3 AST node
2022-05-12 14:28:38 +02:00
Kamil Śliwak
c0cc8ff7e7 Switch to newly built buildpack-deps images in CI 2022-05-12 14:26:07 +02:00
Leo Alt
2fe143f7d0 add changelog entry and docs note 2022-05-12 13:43:28 +02:00
Leo Alt
60b405aaa9 Support new z3 AST node 2022-05-12 10:50:30 +02:00
Leo
0c0ff4fce6
Merge pull request #13000 from ethereum/smt_fix_recursive
[SMTChecker] Fix check that solver is available
2022-05-11 21:52:52 +02:00
Leo Alt
4c00815c53 Changelog entry 2022-05-11 20:02:31 +02:00
Leo Alt
cbaba6f913 update tests 2022-05-11 20:02:31 +02:00
Leo Alt
93f9638a1b Add error id to script 2022-05-11 20:02:31 +02:00
Leo Alt
75d08ea924 Check early if solvers are available. 2022-05-11 20:02:31 +02:00
Daniel Kirchner
1d7b4704bb
Merge pull request #13006 from ethereum/initializationOrderFix
Fix asorted compilation issues with GCC 12.
2022-05-11 17:19:45 +02:00
Daniel Kirchner
cf311e5780 Disable maybe-unitialized warning for boost headers using a pragma. 2022-05-11 16:21:53 +02:00