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
Daniel Kirchner
cbf9a4f1ed
Add bogus return to switch.
2022-05-11 13:58:06 +02:00
Daniel Kirchner
alpharush
Leo Alt
Kamil Śliwak