Commit Graph

22205 Commits

Author SHA1 Message Date
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
ece547204a Reorder member variables of unique error reporter to ensure proper initialization order. 2022-05-11 13:40:02 +02:00
Kamil Śliwak
c64fb7a258 docker_upgrade.sh: Workaround for git refusing to work with a repo in attached volume 2022-05-10 18:24:21 +02:00
Leo Alt
571d94b051 Update docker z3 version 2022-05-10 18:24:21 +02:00
Leo
9f6d3deaea
Merge pull request #12999 from ethereum/disable-non-deterministic-counterexamples-in-some-smt-tests
Disable non-deterministic counterexamples in some SMT tests
2022-05-10 14:32:40 +02:00
Kamil Śliwak
0e0d1972f9 Disable non-deterministic counterexamples in some SMT tests
- The counterexamples sometimes do appear and the tests fail.
2022-05-10 12:48:01 +02:00
Christian Parpart
463e417508
Merge pull request #12960 from ethereum/lsp-make-import-error-fatal
lsp.py enhancements
2022-05-09 16:37:34 +02:00
Marenz
893122eb89 lsp.py: Support subdirectories 2022-05-09 14:54:55 +02:00
Marenz
02dfeb5427 lsp.py: Trigger fatal error when importing outside of test dir 2022-05-09 14:22:23 +02:00
Christian Parpart
59e054bb9b
Merge pull request #12468 from ethereum/allowAllLSP
Always allow full filesystem access to LSP.
2022-05-09 14:20:59 +02:00
Christian Parpart
e8d07772d9 lsp.py: Port to support running on Windows & adapt to changes due to prior merged PR.
- lsp.py: Fixes invalid-syntax by Python interpreter on Windows CI (older Python version).
- lsp.py: Savely strip CRLF from right side of the string, ignoring accidental multiple occurrences of \r (such as \r\r\n).
- lsp.py: Fixes reading single character from stdin (wrt. Windows platform).
- lsp.py: Adds header line reading to I/O tracing (useful for debugging).
- lsp.py: When running the tests on Windows, don't care test file content's newlines but simply expect LFs (instead of CRLF for example).
- Apply pylint notes.
- Fixing use of @functools.lru_cache for older python versions (CircleCI Windows)
2022-05-09 11:37:11 +02:00
Christian Parpart
c2f245b40a Fixes to lsp.py with respect to Windows drive-letter paths in URI. 2022-05-09 11:37:11 +02:00
Christian Parpart
f308f1a1f8 Always allow full filesystem access to LSP. 2022-05-09 11:37:11 +02:00
Christian Parpart
49d27eaa5d [Circle CI] Adds LSP tests to Windows CI. 2022-05-09 11:37:11 +02:00