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
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
Leonardo Alt
64f81fe82b
Fix SMT tests
2020-12-10 18:54:52 +01:00
Martin Blicha
Leo Alt
Alex Beregszaszi
Martin Blicha
chriseth