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
59 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
Alexander Arlt c5673278a7 Remove EWASM backend. 2023-05-11 10:56:55 -05: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
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 cba3d18f66 adjust for osx nondeterminism 2022-05-04 19:04:54 +02:00
Leo Alt 4fd7de36f1 update smt tests z3 4.8.16 2022-05-03 14:23:27 +02: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 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 16bc15acac Fix false negative on storage array references returned by internal functions 2021-08-28 09:30:53 +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 20e23171da Update tests to z3 4.8.12 2021-07-16 14:43:52 +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
Martin Blicha 330fb8f4d0 [SMTChecker] Assignment refactoring 2021-03-31 13:36:50 +02:00
Leonardo Alt ba97d6ac4e Add local vars to cex 2021-03-30 17:55:21 +02:00
Leonardo Alt dbd067d6db Report out of bounds index access 2021-03-30 10:28:48 +02:00
Martin Blicha 98446782e2 [SMTChecker] Fix compound assignment to push 2021-03-24 14:54:13 +01:00
Martin Blicha deb90d84a6 [SMTChecker] added missing type constraints for Address 2021-01-27 20:39:24 +01:00
Leonardo Alt 007d39871b [SMTChecker] Synthesize untrusted functions called externally 2021-01-15 11:56:26 +01:00
Martin Blicha 5e13744423 [SMTChecker] Fixed pushing string literal to bytes array 2021-01-13 16:30:50 +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
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
Leonardo Alt 50be39fc21 Add and update tests 2020-12-17 14:42:49 +01:00
Leonardo Alt 59428b8f76 Fix SMTChecker tests on breaking 2020-12-15 19:49:57 +01:00
Martin Blicha 27402781c4 [SMTChecker] Fixed crash on push to bytes on lhs of an assignment 2020-12-14 17:40:45 +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
chriseth 79669ecd48 Use new abicoder pragma. 2020-11-24 14:57:45 +01:00
Leonardo Alt e38d0db683 [SMTChecker] Fix internal error when array.push() is used as LHS of assignment 2020-11-02 13:32:53 +00:00
Martin Blicha c1a57ffbfe [SMTChecker] More precise creation of verification targets. 2020-10-30 19:11:28 +01:00
Leonardo Alt 88f783bb1e Remove more tests because current Spacer crashes 2020-10-13 19:27:49 +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 afcd44e77c Update current tests 2020-09-03 15:19:03 +02:00
Leonardo Alt 8c05db88c0 [SMTChecker] Fix soundness of array pop 2020-08-31 12:11:33 +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 6bb6783d39 Merge remote-tracking branch 'origin/develop' into breaking 2020-07-22 15:26:44 +02:00