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
Leo Alt
21c0f78650
Report safe properties in BMC and CHC
2023-03-09 14:59:32 +01:00
Leo Alt
16c0838f75
Update docker images and tests
2022-08-30 11:51:59 +02: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
85378b1770
Update existing tests
2021-08-25 21:10:08 +02:00
chriseth
c87c0f02bd
Test updates.
2021-08-12 16:56:12 +02:00
Leo Alt
3c1f555f71
Tests
2021-08-04 13:54:50 +02:00
Leo Alt
e46abd0ca1
Update tests due to nondeterminism
2021-07-19 15:20:11 +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
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
Martin Blicha
85358dfe30
[SMTChecker] Do not create targets for contracts that cannot be deployed
2021-03-25 15:38:37 +01:00
Leonardo Alt
998346e599
Fix bug in virtual functions called by constructor.
2021-03-12 16:42:28 +01:00
Leonardo Alt
665ce27c18
Fix inheritance bug in CHC cex
2021-02-02 18:06:32 +01:00
Martin Blicha
a49950cdf3
[SMTChecker] Added transaction constraints also for contract deployment
2021-02-01 16:46:34 +01:00
Leonardo Alt
545305a31f
[SMTChecker] Fix super and virtual
2021-01-28 18:51:29 +01:00
Leonardo Alt
a612daa783
Add msgvalue to cex
2021-01-21 19:05:44 +01:00
Leonardo Alt
c7ca87c012
Fix static virtual resolution
2021-01-18 16:23:38 +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
d90b9da4f0
[SMTChecker] Refactoring
2020-12-22 13:10:48 +01:00
Leonardo Alt
50be39fc21
Add and update tests
2020-12-17 14:42:49 +01:00
Leonardo Alt
3c142e0e94
Move CHC counterexamples to primary location
2020-12-09 19:55:18 +01:00
Leonardo Alt
7490ffbe13
Use nonlinear clauses instead of inlining for base constructors
2020-12-04 13:25:56 +01:00
Leonardo Alt
e6bd18525b
[SMTChecker] Add engine prefix to verification target error messages
2020-09-25 19:09:06 +02:00
Leonardo Alt
00f6b303b1
[SMTChecker] Change warning message
2020-09-09 16:14:21 +02:00
Leonardo Alt
0a160b1ba0
Update remaining tests
2020-08-14 12:58:27 +02:00
Leonardo Alt
95484d9969
Fix tests after rebase
2020-07-23 18:49:03 +02:00
Leonardo Alt
003c9b9a5b
Update tests
2020-07-23 18:49:03 +02:00
chriseth
9743390a53
Update tests.
2020-07-07 12:16:18 +02:00
a3d4
e04cedafc5
Added error codes to SyntaxTest expectations (updated tests)
2020-06-22 16:51:47 +02:00
Leonardo Alt
07368c2e1e
Add support to internal function calls
2020-03-11 16:29:07 +01:00
chriseth
f6916a637e
Merge remote-tracking branch 'origin/develop' into develop_060
2019-12-09 17:16:58 +01:00
Leonardo Alt
beed0f6a27
Set tests that CVC4 can't handle to Z3 only
2019-12-09 15:32:08 +01:00
Leonardo Alt
d6e8ca4c54
Fix SMTChecker tests in 060
2019-12-03 21:44:10 +01:00
chriseth
2d42da3b7d
Merge pull request #7817 from ethereum/bail-on-shadowing-state-vars
...
Report error on shadowing state variables
2019-12-03 21:22:39 +01:00
Christian Parpart
7bbdfe070f
Make shadowing of inherited state variables an error.
2019-12-03 21:20:03 +01:00
chriseth
96d777d7f1
Merge commit 'a7d481fb9' into develop_060
2019-12-03 20:47:30 +01:00
Leonardo Alt
a352abe00d
[SMTChecker] Add support to constructors
2019-11-28 14:43:23 +01:00
Mathias Baumann
5b8ff78176
Implement virtual keyword
2019-11-14 11:49:39 +01:00
Leonardo Alt
fc945880d1
[SMTChecker] Fix override tests
2019-11-07 11:49:32 +01:00
Leonardo Alt
10e70b8603
[SMTChecker] Support inheritance and resolve overrides
2019-11-06 11:00:06 +01:00
Leonardo Alt
dd4e938265
[SMTChecker] Fix ICE in inherited state var
2019-05-02 10:03:12 +02:00