Commit Graph

79 Commits

Author SHA1 Message Date
Leonardo Alt
10e70b8603 [SMTChecker] Support inheritance and resolve overrides 2019-11-06 11:00:06 +01:00
chriseth
46ac16d25c Merge remote-tracking branch 'origin/develop' into develop_060 2019-11-04 19:09:11 +01:00
Leonardo Alt
8a42e3f87a [SMTChecker] Support assignments to m-d arrays and mappings 2019-10-28 17:27:39 +01:00
Leonardo
ca714a2d3d
Merge pull request #7485 from ethereum/develop
Merge develop into develop_060
2019-09-26 15:43:12 +02:00
Leonardo Alt
83ef34f41d [SMTChecker] Fix SMT name for function identifiers 2019-09-24 11:23:10 +02:00
chriseth
5b3efee93b
Merge pull request #7442 from ethereum/develop
Merge develop into develop_060
2019-09-17 12:16:27 +02:00
Leonardo Alt
e1c238e25f [SMTChecker] Add loop support 2019-09-13 12:40:53 +02:00
Daniel Kirchner
4782c800ec Initial introduction of array slices with partial implementation for dynamic calldata arrays. 2019-09-13 10:57:53 +02:00
Leonardo Alt
214e5c6369 [SMTChecker] Fix index access type type error 2019-08-27 16:39:19 +02:00
Leonardo
cbac3a4208
Merge pull request #7107 from ethereum/smt_chc_constructor_interface
[SMTChecker] Add CHC constructor/interface/error blocks
2019-08-12 15:06:08 +02:00
Leonardo Alt
bef6228810 [SMTChecker] Create CHC constructor/interface/error blocks 2019-08-12 12:34:57 +02:00
Leonardo Alt
360f868836 [SMTChecker] Fix literal string type mismatch 2019-08-10 21:51:46 +02:00
Leonardo Alt
7b22496b1f [SMTChecker] Fix ICE when inlining functions that use state vars and are in a different source 2019-08-09 17:50:52 +02:00
Leonardo Alt
369f8cd97f [SMTChecker] CHC create function return variables 2019-08-05 12:36:51 +02:00
Leonardo
11632966c9
Merge pull request #7171 from ethereum/smt_fix_compound_bitwise
[SMTChecker] Fix ICE compound bitwise op inside branch
2019-08-05 12:15:01 +02:00
Leonardo Alt
d5fb8cf58a [SMTChecker] Fix ICE compound bitwise op inside branch 2019-08-02 20:02:39 +02:00
Leonardo Alt
7b5863e583 Do not erase knowledge about storage pointers when another pointer is assigned 2019-08-02 13:09:06 +02:00
Leonardo Alt
44d7c6976a Erase pointer knowledge properly inside loops 2019-07-30 12:47:50 +02:00
Leonardo Alt
847f574e22 [SMTChecker] Fix ICE when inlining function with tuple expression 2019-07-26 16:29:29 +02:00
Leonardo Alt
382df64899 [SMTChecker] Refactor function inlining 2019-07-18 13:56:48 +02:00
Leonardo Alt
934e00d235 [SMTChecker] SymbolicVariables use EncodingContext to declare SMT vars 2019-07-03 16:05:56 +02:00
chriseth
817852c650
Merge pull request #7030 from ethereum/smt_move_solver
[SMTChecker] Move solver from SMTEncoder to BMC
2019-07-02 14:08:55 +02:00
chriseth
e542e46163
Merge pull request #7022 from ethereum/smt_create_expr
[SMTChecker] Always create symbolic expression
2019-07-02 14:07:24 +02:00
chriseth
ca10b59b25
Merge pull request #7020 from ethereum/smt_fix_callstack_message
[SMTChecker] Fix wrong assertion in callstack message
2019-07-02 13:47:49 +02:00
Leonardo Alt
b0818bd002 [SMTChecker] Move solver pointer from SMTEncoder to BMC 2019-07-02 12:06:52 +02:00
Leonardo Alt
fb3c85633b Always create symbolic expression 2019-07-01 16:25:33 +02:00
Leonardo Alt
75663dc91e [SMTChecker] Fix require with message 2019-07-01 16:17:06 +02:00
Leonardo Alt
6606a13ed2 [SMTChecker] Remove unsound assertion (too strong) 2019-07-01 16:16:39 +02:00
Leonardo Alt
3cb4ed83c1 [SMTChecker] Split SMTChecker into SMTEncoder and BMC 2019-07-01 15:05:03 +02:00