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
21,212 Commits 348 Branches 121 Tags
separate-control-flow-from-error-reporting-in-CommandLineParser
Commit Graph
29 Commits
Author SHA1 Message Date
Leo Alt 4c2b661eaa [SMTChecker] Report values for block, msg and tx variables in counterexamples 2021-10-05 15:19:10 +02:00
Leo Alt a1bea368cb [SMTChecker] Support constants via modules 2021-09-16 14:35:05 +02:00
Leo Alt d91f75deb8 Fix ICE on unique errors 2021-09-09 16:37:43 +02:00
Leo Alt 0cc9162fb5 Update SMTChecker tests 2021-08-27 16:25:09 +02:00
Leo Alt 8eb28b10cb Add SMTChecker tests with modules 2021-06-01 13:35:10 +02:00
Leo Alt 1642c10f6e Fix ICE in free functions 2021-05-03 10:57: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 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 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
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 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
Martin Blicha 66125b79d6 [SMTChecker] Do not report warning when encountered a Type identifier. The operations are supported now. 2020-11-23 15:41:57 +01:00
Leonardo Alt daf859c15b [SMTChecker] report SMTEncoder warnings also via CHC 2020-11-03 16:06:17 +00:00
Leonardo Alt 94e2506132 Fix inherited state vars for BMC 2020-11-02 11:42:39 +00:00
Martin Blicha c1a57ffbfe [SMTChecker] More precise creation of verification targets. 2020-10-30 19:11:28 +01:00
Leonardo Alt cf35785328 Add unknown message to all verification targets 2020-10-19 20:54:13 +01:00
Mathias Baumann 4c02cd2310 Add name for split-test to prevent failure in other places 2020-09-30 16:56:53 +02:00
Leonardo Alt e6bd18525b [SMTChecker] Add engine prefix to verification target error messages 2020-09-25 19:09:06 +02:00
Leonardo Alt 0223571987 [SMTChecker] Do not report error when rlimit 2020-09-25 18:43:10 +02:00
Leonardo Alt 8eba66daf9 Extract boost smt and remove unused tests 2020-09-23 17:55:55 +02:00
Leonardo Alt 23ee011c56 [SMTChecker] Fix imports 2020-09-11 13:34:46 +02:00