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
50 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 678461e828 Fix encoding of side-effects inside if and conditional statements in the BMC engine 2023-05-11 16:44:09 +02:00
Leo Alt 21c0f78650 Report safe properties in BMC and CHC 2023-03-09 14:59:32 +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 4fd7de36f1 update smt tests z3 4.8.16 2022-05-03 14:23:27 +02: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 ff5c842d67 update smtchecker tests 2021-11-24 20:41:22 +01:00
Leo Alt 38b0cf7f9c SMTChecker tests 2021-10-26 11:30:30 +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
Alex Beregszaszi 45c6bbe02b Trivial isoltest updates: directives sorted alphabetically 2021-04-20 17:21:56 +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 25b31111df Merge pull request #11040 from ethereum/smt_fix_virtual_one_more_time 
[SMTChecker] Fix bug in virtual functions called by constructor
 2021-03-17 16:54:36 +01:00
Martin Blicha 2f52affcc2 [SMTChecker] Correctly resolve current scope contract in VariableUsage. 2021-03-15 13:55:14 +01:00
Leonardo Alt 998346e599 Fix bug in virtual functions called by constructor. 2021-03-12 16:42:28 +01:00
Leonardo Alt 6fd76e830d Fix CHC cex order 2021-03-11 10:36:40 +01:00
Leonardo Alt 007d39871b [SMTChecker] Synthesize untrusted functions called externally 2021-01-15 11:56:26 +01:00
Leonardo Alt b3c3836388 Output internal calls 2021-01-12 14:57:04 +01:00
Leonardo Alt f1ae24abc7 Remove extra line breaks 2021-01-12 14:00:07 +01:00
Martin Blicha 09de54b5eb tests 2021-01-11 13:36:03 +01:00
Leonardo Alt b02722ebda Add contract name to called function in cex 2021-01-04 10:03:16 +01:00
Martin Blicha be0a0f4d90 [SMTChecker] Added constraints for block properties 2020-12-29 22:17:44 +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
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 3c142e0e94 Move CHC counterexamples to primary location 2020-12-09 19:55:18 +01:00
Leonardo Alt b7ac207391 [SMTChecker] Support return in CHC 2020-12-07 18:17:33 +01:00
Leonardo Alt 1dbd8f8d67 Fix CHC false positives when using branches inside modifiers 2020-11-04 21:47:07 +00:00
Leonardo Alt daf859c15b [SMTChecker] report SMTEncoder warnings also via CHC 2020-11-03 16:06:17 +00:00
Mathias Baumann 32b4f18023 Print warning for unnamed return parameters and no return statement 2020-10-13 13:11:29 +02:00
Leonardo Alt e6bd18525b [SMTChecker] Add engine prefix to verification target error messages 2020-09-25 19:09:06 +02:00
Leonardo Alt f4ee4cd479 Update tests 2020-09-22 20:51:28 +02:00
Alex Beregszaszi 783d66c1a4 [SMTChecker] Support revert() 2020-09-15 11:46:33 +01:00
Alex Beregszaszi 8f36408ef9 Add test case for revert() in SMTChecker 2020-09-15 11:46:16 +01: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 003c9b9a5b Update tests 2020-07-23 18:49:03 +02:00
a3d4 e04cedafc5 Added error codes to SyntaxTest expectations (updated tests) 2020-06-22 16:51:47 +02:00
Leonardo Alt 10162016ae [SMTChecker] Fix internal error on try/catch 2020-06-02 16:51:53 +02:00
Leonardo Alt 07368c2e1e Add support to internal function calls 2020-03-11 16:29:07 +01:00
Leonardo Alt 3d52a6ca68 [SMTChecker] Fix ICE in branch-inline function call-modify local variable 2019-05-09 09:15:11 +02:00
Leonardo Alt 80712f44cb Fix short circuit with assignments 2019-05-06 11:04:43 +02:00
Leonardo Alt dadafed022 Short circuit tests 2019-03-28 16:08:30 +01:00
Leonardo Alt a7e826a224 [SMTChecker] Implement short circuit 2019-03-28 16:08:30 +01:00
Leonardo Alt 2ae778bf0a [SMTChecker] Add buggy short circuit test 2019-03-21 18:47:14 +01:00
Leonardo Alt 32fe4768a9 Organize smt tests in subdirectories 2018-11-22 13:33:28 +00:00