Commit Graph
16 Commits
Author SHA1 Message Date
chriseth 216e1749f4 Merge remote-tracking branch 'origin/develop' into develop_060 2019-11-14 13:42:46 +01:00
Leonardo Alt e3652627fd [SMTChecker] Fix ICE in CHC when function used as argument 2019-11-13 15:11:30 +01:00
chriseth 2e5a42836c Merge pull request #7681 from ethereum/develop
Merge develop into develop_060
2019-11-11 16:42:03 +01:00
Leonardo Alt 6b10efff8c Add CHCSmtLib2Interface 2019-11-07 11:12:11 +01:00
chriseth 21e65076b3 Merge pull request #7650 from ethereum/develop
Merge develop into develop_060
2019-11-06 21:56:55 +01:00
Leonardo Alt 10e70b8603 [SMTChecker] Support inheritance and resolve overrides 2019-11-06 11:00:06 +01:00
chriseth 4d99bf68f4 Merge pull request #7638 from ethereum/develop
Merge develop into develop_060
2019-11-05 17:33:54 +01:00
Leonardo Alt c5e081dc8c [SMTChecker] Refactor CHC loops and add if blocks 2019-11-05 09:28:59 +01:00
Daniel Kirchner 3321fc56ea Split fallback function and introduce "fallback()" and "receive()" syntax. 2019-11-04 17:17:58 +01:00
Leonardo Alt e1c238e25f [SMTChecker] Add loop support 2019-09-13 12:40:53 +02:00
Leonardo Alt 1a70a46f9b [CHC] Add function blocks and check asserts 2019-08-15 12:25:15 +02:00
Leonardo Alt bef6228810 [SMTChecker] Create CHC constructor/interface/error blocks 2019-08-12 12:34:57 +02:00
Leonardo Alt 4214cd1354 [SMTChecker] Fix ICE when reporting cex concerning state vars from different source files 2019-08-10 20:56:52 +02:00
Leonardo Alt 369f8cd97f [SMTChecker] CHC create function return variables 2019-08-05 12:36:51 +02:00
Leonardo Alt b204f27047 [SMTChecker] EncodingContext config flag to accumulate assertions 2019-07-19 19:31:25 +02:00
Leonardo Alt 03cc124f32 Add CHC skeleton 2019-07-19 11:52:05 +02:00