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,850 Commits 348 Branches 121 Tags
import-asm-json-updated-2
Commit Graph
32 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
Pawel Gebal f15b826431 Add optional bounds to unroll loops in BMC model checker 2023-06-02 18:32:38 +02:00
Alexander Arlt c5673278a7 Remove EWASM backend. 2023-05-11 10:56:55 -05: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 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 cba3d18f66 adjust for osx nondeterminism 2022-05-04 19:04:54 +02:00
Leo Alt 9f171c0f06 update smtchecker tests for new z3 2022-01-12 15:13:34 +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 0cc9162fb5 Update SMTChecker tests 2021-08-27 16:25:09 +02:00
Leo Alt 85378b1770 Update existing tests 2021-08-25 21:10:08 +02:00
Leo Alt e46abd0ca1 Update tests due to nondeterminism 2021-07-19 15:20:11 +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 2d231f1859 [SMTChecker] Changed SMTEncoder::mergeVariables to work regardless which branch has been visited first 2021-03-30 20:35:44 +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
Leonardo Alt 6fd76e830d Fix CHC cex order 2021-03-11 10:36:40 +01:00
Martin Blicha a49950cdf3 [SMTChecker] Added transaction constraints also for contract deployment 2021-02-01 16:46:34 +01:00
Martin Blicha deb90d84a6 [SMTChecker] added missing type constraints for Address 2021-01-27 20:39:24 +01:00
Leonardo Alt a612daa783 Add msgvalue to cex 2021-01-21 19:05:44 +01:00
Martin Blicha 35d228d9b6 [SMTChecker] Gather local variables also from nested try/catch clauses 2021-01-18 18:30:18 +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
Martin Blicha ff76c989ac addressing review comments 2021-01-11 14:19:06 +01:00
Martin Blicha 3d7188ac7b update to the tests 2021-01-11 13:36:03 +01:00
Martin Blicha 09de54b5eb tests 2021-01-11 13:36:03 +01:00