Commit Graph

495 Commits

Author SHA1 Message Date
Marenz
f426b5988e Disallow comparison operators on contracts 2022-08-18 17:56:22 +02:00
chriseth
3c2cee5836
Merge pull request #13026 from ethereum/develop
Merge develop into breaking.
2022-05-16 15:29:39 +02:00
Leo Alt
6a126f6ccb Update tests and hashes for z3 4.8.17 2022-05-13 15:25:10 +02:00
Leo Alt
cbaba6f913 update tests 2022-05-11 20:02:31 +02:00
chriseth
a137d42094
Merge pull request #13007 from ethereum/develop
Merge develop into breaking.
2022-05-11 16:39:24 +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
Leo Alt
201c6c6819 fix smt flaky test 2022-05-05 11:38:16 +02:00
Leo Alt
cba3d18f66 adjust for osx nondeterminism 2022-05-04 19:04:54 +02:00
Leo Alt
4fd7de36f1 update smt tests z3 4.8.16 2022-05-03 14:23:27 +02:00
chriseth
a433511128 Merge remote-tracking branch 'origin/develop' into breaking 2022-04-13 17:08:27 +02:00
Leo Alt
f9fa76c9d3 smt encode call 2022-04-11 12:19:41 +02:00
chriseth
6b88e470ff Merge remote-tracking branch 'origin/develop' into breaking 2022-03-07 16:34:55 +01:00
Leo Alt
bef69b595b Ignore cex in SMT test 2022-02-28 18:56:20 +01:00
chriseth
814e233b67
Merge pull request #12604 from ethereum/develop
Merge develop into breaking
2022-01-31 17:59:03 +01:00
Leo Alt
098a3cb537 adjust tests for nondeterminism 2022-01-12 18:43:18 +01:00
Daniel Kirchner
1655626e0a Remove counterexample from test. 2022-01-12 17:58:05 +01:00
Leo Alt
9f171c0f06 update smtchecker tests for new z3 2022-01-12 15:13:34 +01:00
Leo Alt
fb8c138b8b Do not analyze unecessary contracts 2021-12-24 19:36:32 +01:00
chriseth
923d1cf2d2
Merge pull request #12423 from ethereum/develop
Merge develop into breaking.
2021-12-20 11:40:40 +01:00
Marenz
7a96953e78 Implement typechecked abi.encodeCall() 2021-12-16 17:35:58 +01:00
chriseth
c79ced0558
Merge pull request #12407 from ethereum/develop
Merge develop into breaking.
2021-12-14 18:54:25 +01:00
Leo Alt
316be7206f Fix soundness of storage/memory pointers that were not erasing enough knowledge 2021-12-14 12:02:18 +01:00
chriseth
0bbf58ec5e
Merge pull request #12376 from ethereum/develop
Merge `develop` into `breaking`
2021-12-13 12:59:33 +01:00
Leo Alt
16535aae32 Fix ICE when unsafe targets are solved more than once and the cex is different 2021-12-03 00:21:38 +01:00
Leo Alt
a2588533e5 macos nondeterminism 2021-11-24 20:41:22 +01:00
Leo Alt
0c34d9df88 Adjust tests for nondeterminism 2021-11-24 20:41:22 +01:00
Leo Alt
ff5c842d67 update smtchecker tests 2021-11-24 20:41:22 +01:00
chriseth
88cc42230f Merge remote-tracking branch 'origin/develop' into breaking 2021-11-09 18:26:34 +01:00
Leo Alt
dff280cadc Fix ICE in CHC when using gas in the function options 2021-11-03 15:40:54 +01:00
Leo Alt
e40cf92b1d [SMTChecker] Merge all entry points for a target 2021-11-03 11:12:58 +01:00
chriseth
8c6e5e501b Merge remote-tracking branch 'origin/develop' into breaking 2021-10-27 18:09:13 +02:00
Leo Alt
38b0cf7f9c SMTChecker tests 2021-10-26 11:30:30 +02:00
chriseth
8bcbe946c6 Merge remote-tracking branch 'origin/develop' into breaking 2021-10-06 12:00:17 +02:00
Leo Alt
4c2b661eaa [SMTChecker] Report values for block, msg and tx variables in counterexamples 2021-10-05 15:19:10 +02:00
Leo Alt
d81ebe97c3 Fix magic access 2021-10-01 12:57:06 +02:00
Leo Alt
d25fb29178 Add isoltest option to ignore OS 2021-10-01 12:45:36 +02:00
Leo Alt
e74f853c6b [SMTChecker] Support user types 2021-09-21 13:23:17 +02:00
Leo Alt
a1bea368cb [SMTChecker] Support constants via modules 2021-09-16 14:35:05 +02:00
Leo Alt
b731957e65 Fix BMCs constraints on internal functions 2021-09-15 14:42:39 +02:00
Leo Alt
d91f75deb8 Fix ICE on unique errors 2021-09-09 16:37:43 +02:00
Leo Alt
6e2fe1e340 [SMTChecker] Cleanup spurious messages about TypeTypes 2021-09-07 16:55:25 +02:00
Leo Alt
106c591dde Support the external call option 2021-09-01 20:18:37 +02:00
chriseth
e6b642699b Merge remote-tracking branch 'origin/develop' into breaking 2021-08-31 10:36:23 +02:00
Leo Alt
ac528cfd1b add static array length constraint 2021-08-30 17:15:16 +02:00
Leo Alt
16bc15acac Fix false negative on storage array references returned by internal functions 2021-08-28 09:30:53 +02:00
Leo Alt
60b866f9d8 Fix ICE on multi-source use of abi.* 2021-08-27 18:55:36 +02:00
Leo Alt
0cc9162fb5 Update SMTChecker tests 2021-08-27 16:25:09 +02:00
Leo Alt
a9af63187e Adjust tests for nondeterminism 2021-08-25 21:10:43 +02:00
Leo Alt
4cf4ccafd7 New tests 2021-08-25 21:10:08 +02:00
Leo Alt
85378b1770 Update existing tests 2021-08-25 21:10:08 +02:00