cerc-io/solidity
11
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,848 Commits 348 Branches 121 Tags
new-analysis-crashes
Commit Graph
47 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
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