cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity
23,865 Commits 348 Branches 121 Tags 100 MiB
201259d50b
Commit Graph

61 Commits

Author SHA1 Message Date
Martin Blicha
cdfc19b503 SMTChecker: Bring back counterexample checks in regression tests 
Since the default is now to ignore the counterexamples when checking
test output, we bring back counterexample checks in tests where the
counterexample is (mostly) deterministic.
 2023-07-25 12:26:21 +02:00
Martin Blicha
b0419da654 [SMTChecker] Remember verification targets from trusted external calls 
Previously, we did not remember trusted external calls for later phase
when we compute possible verification targets for each function.
This led to false negative in cases where verification target can be
violated, but not by calling a public function directly, but only when
it is called as an external function from other function.

The added test cases witnesses this behaviour. The underflow in
`dec` cannot happen in any other way except what the `dec` is called
from `f`.

The same problem did not occur when the functions are called internally,
because for such cases, we have already been remembering these calls in
the callgraph in the CHC engine.
 2023-05-26 13:03:44 +02:00
Leo Alt
ce9a7ee954 update smtchecker tests 2023-03-28 18:23:54 +02:00
Leo Alt
21c0f78650 Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
Leo Alt
8d91ccf028 [SMTChecker] Add a new trusted mode which assumes that code that is 
available at compile time is trusted.
 2023-02-06 17:02:33 +01:00
Rodrigo Q. Saramago
feba4de509
Add paris constraints to SMTChecker 
Co-authored-by: Daniel <daniel@ekpyron.org>
Co-authored-by: Kamil Śliwak <kamil.sliwak@codepoets.it>
Co-authored-by: Leo <leo@ethereum.org>
 2023-01-31 11:03:04 +01:00
Leo Alt
d660f0cab0 adjust nondeterministic tests 2022-11-24 13:08:06 +01:00
Leo Alt
504b70b6af update smt tests 2022-11-24 13:08:06 +01:00
Leo Alt
16c0838f75 Update docker images and tests 2022-08-30 11:51:59 +02:00
Leo Alt
6a126f6ccb Update tests and hashes for z3 4.8.17 2022-05-13 15:25:10 +02:00
Leo Alt
4fd7de36f1 update smt tests z3 4.8.16 2022-05-03 14:23:27 +02:00
Leo Alt
098a3cb537 adjust tests for nondeterminism 2022-01-12 18:43:18 +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
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
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
Leo Alt
38b0cf7f9c SMTChecker tests 2021-10-26 11:30:30 +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
d25fb29178 Add isoltest option to ignore OS 2021-10-01 12:45:36 +02:00
Leo Alt
106c591dde Support the external call option 2021-09-01 20:18:37 +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
85378b1770 Update existing tests 2021-08-25 21:10:08 +02:00
Leo Alt
9ea4576664 Update tests 2021-08-19 16:34:01 +02:00
Leo Alt
937af7d722 Fix SMT test 2021-08-12 22:34:18 +02:00
Leo Alt
6ee60aa628 Fix false positive on external calls from constructors 2021-08-12 18:51:55 +02:00
Leo Alt
3c1f555f71 Tests 2021-08-04 13:54:50 +02:00
Leo Alt
20e23171da Update tests to z3 4.8.12 2021-07-16 14:43:52 +02:00
Leo Alt
547a6915ad Fix ICE on external calls from constructor 2021-06-01 14:21:48 +02:00
Alex Beregszaszi
1be07c2b36 Trivial isoltest updates: missing // ---- at the end 2021-04-20 17:38:29 +02:00
Alex Beregszaszi
84c05d35f3 Trivial isoltest updates: normalized whitespace 2021-04-20 17:38:29 +02:00
Leonardo Alt
6ae82fcec2 Add tests for the library bug 2021-04-19 19:23:18 +02:00
Leonardo Alt
0a4afa71bd Update old tests 2021-04-08 21:03:39 +02:00
Leonardo Alt
ba97d6ac4e Add local vars to cex 2021-03-30 17:55:21 +02:00
Leonardo Alt
998346e599 Fix bug in virtual functions called by constructor. 2021-03-12 16:42:28 +01:00
Martin Blicha
a49950cdf3 [SMTChecker] Added transaction constraints also for contract deployment 2021-02-01 16:46:34 +01:00
Leonardo Alt
a612daa783 Add msgvalue to cex 2021-01-21 19:05:44 +01:00
Leonardo Alt
007d39871b [SMTChecker] Synthesize untrusted functions called externally 2021-01-15 11:56:26 +01:00
Leonardo Alt
f1ae24abc7 Remove extra line breaks 2021-01-12 14:00:07 +01:00
Leonardo Alt
b02722ebda Add contract name to called function in cex 2021-01-04 10:03:16 +01:00
Leonardo Alt
78d55e6b4a [SMTChecker] Support check/unchecked 2020-12-30 12:14:30 +01:00
Martin Blicha
41d31fe4d4 updates to the tests 2020-12-28 20:05:52 +01:00
Martin Blicha
745466b71f updates to the tests 2020-12-28 14:32:53 +01:00
Leonardo Alt
50be39fc21 Add and update tests 2020-12-17 14:42:49 +01:00
chriseth
0dd2f1edbe Update counter-examples. 2020-12-14 14:21:35 +01:00
chriseth
561280a5cc Merge remote-tracking branch 'origin/develop' into breaking 2020-12-14 11:33:40 +01:00
Martin Blicha
8927015e5a [SMTChecker] Adding unary increment and decrement as under/overflow verification targets for the CHC engine 2020-12-11 17:41:50 +01:00