chriseth
561280a5cc
Merge remote-tracking branch 'origin/develop' into breaking
2020-12-14 11:33:40 +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
Alex Beregszaszi
bd641a5206
Enable more C++ compiler warnings
2020-12-10 21:03:58 +00:00
Daniel Kirchner
c400c61fc3
Fix incorrect behaviour on clang 6.
2020-12-10 17:20:30 +01:00
chriseth
d0551b67d7
Merge remote-tracking branch 'origin/develop' into breaking
2020-12-10 17:07:56 +01:00
Daniel Kirchner
7308abc084
Allow loading Z3 dynamically at runtime.
2020-12-10 16:47:47 +01:00
chriseth
482bda6887
Merge remote-tracking branch 'origin/develop' into breaking
2020-12-10 12:15:52 +01:00
Leonardo Alt
3c142e0e94
Move CHC counterexamples to primary location
2020-12-09 19:55:18 +01:00
Leonardo Alt
a961a76263
Do not run SMTChecker when file level functions/constants are present.
2020-12-09 12:18:55 +01:00
chriseth
806453aca9
Merge remote-tracking branch 'origin/develop' into breaking
2020-12-08 21:00:09 +01:00
chriseth
b045195c1e
Merge remote-tracking branch 'origin/develop' into breaking
2020-12-08 17:42:31 +01:00
Martin Blicha
eb356735f6
[SMTChecker] Adding support for reporting values of structs in CEX in CHC engine.
2020-12-08 16:40:28 +01:00
Martin Blicha
0ebab439be
removing assert that is not always true
2020-12-08 12:27:59 +01:00
Martin Blicha
ff0c794674
[SMTChecker] Fixing conversion from StringLiteral to FixedBytes
2020-12-07 19:30:51 +01:00
Leonardo Alt
b7ac207391
[SMTChecker] Support return in CHC
2020-12-07 18:17:33 +01:00
chriseth
bff7254d9e
Fix merge conflict.
2020-12-07 13:30:09 +01:00
chriseth
329b8f2a60
Merge remote-tracking branch 'origin/develop' into breaking
2020-12-07 13:04:14 +01:00
Leonardo Alt
7490ffbe13
Use nonlinear clauses instead of inlining for base constructors
2020-12-04 13:25:56 +01:00
chriseth
d56a7bb89e
Merge pull request #10489 from ethereum/develop
...
Merge develop into breaking.
2020-12-03 18:11:12 +01:00
Leonardo
088b694f0b
Merge pull request #10207 from ethereum/smt_tests_asserts
...
[SMTChecker] Add uncovered test and replace uncovered tests by asserts
2020-12-03 08:59:48 +01:00
Martin Blicha
2ee633f404
[SMTChecker] Added support for public getters through this.
2020-12-02 16:06:48 +01:00
chriseth
6de7eaba95
Merge remote-tracking branch 'origin/develop' into breaking
2020-12-01 10:50:13 +01:00
Leonardo Alt
fa561dbd0e
Add uncovered test and replace uncovered tests by asserts
2020-11-30 18:46:47 +01:00
Martin Blicha
cd06d68cbe
[SMTChecker] Keeping better track of path condition through branches with return statement in the BMC engine.
2020-11-30 11:47:49 +01:00
chriseth
18de8a56c9
Merge remote-tracking branch 'origin/develop' into breaking
2020-11-26 11:48:53 +01:00
Djordje Mijovic
26c43cfc66
[SMTChecker] Fix SMT logic error when doing compound assignment with string literlas.
2020-11-24 19:14:15 +01:00
chriseth
253889cbf1
Merge remote-tracking branch 'origin/develop' into breaking
2020-11-24 16:22:03 +01:00
Leonardo Alt
68cfa0a901
Fix spelling in SMTChecker comment
2020-11-23 19:40:29 +01:00
chriseth
a0a02f2307
Merge remote-tracking branch 'origin/develop' into breaking
2020-11-23 19:28:08 +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
Martin Blicha
80d743426f
[SMTChecker] Added support for struct constructor.
2020-11-23 13:45:17 +01:00
Leonardo
61069ec77d
Merge pull request #10355 from blishko/smtchecker-refactoring
...
[SMTChecker] Small refactoring of assignments to provide a common low-level point for model checking engines to hook into.
2020-11-20 14:31:32 -01:00
Leonardo Alt
e4339b0526
[SMTChecker] Support named arguments in function calls
2020-11-20 11:52:26 -01:00
Martin Blicha
fbcb572d69
[SMTChecker] Small refactoring of assignments to provide a common low-level point for model checker engines to hook into.
2020-11-19 22:03:08 +01:00
chriseth
e8a278eefa
Merge remote-tracking branch 'origin/develop' into breaking
2020-11-17 18:51:57 +01:00
Martin Blicha
07427c798c
[SMTChecker] Adding a dummy frame to the call stack for the implicit constructor
2020-11-16 22:46:17 +01:00
Martin Blicha
5ca7a24896
[SMTChecker] Added support for precise modeling of external calls to this.
...
Modeling external calls to this, since we can trust these calls.
fixed problem with transaction data not being restored after trusted external call
update to the tests
additional tests
changelog entry
added tests for external getters of this
2020-11-13 11:49:09 +01:00
chriseth
14ed67ac4b
Merge remote-tracking branch 'origin/develop' into breaking
2020-11-11 20:33:40 +01:00
Alex Beregszaszi
2f899bbffa
[SMTChecker] Avoid implicit conversion
2020-11-11 16:29:03 +00:00
chriseth
da92fe548e
Merge remote-tracking branch 'origin/develop' into breaking
2020-11-10 13:48:32 +01:00
Leonardo
25b2a38d8b
Merge pull request #10202 from ethereum/smt_fix_modifiers_branches
...
[SMTChecker] Fix CHC false positives when using branches inside modifiers
2020-11-09 16:42:30 +00:00
chriseth
04195439b7
Merge remote-tracking branch 'origin/develop' into HEAD
2020-11-09 14:28:05 +01:00
Leonardo Alt
00858c0ccf
Isoltets SMTChecker option and BMC specific tests
2020-11-06 15:03:38 +00:00
Leonardo Alt
89dce24f24
Force SMT variable creation order
2020-11-06 11:51:01 +00:00
Leonardo Alt
646be53f2f
Sort variables and expressions by AST id
2020-11-06 11:50:43 +00:00
Leonardo Alt
1dbd8f8d67
Fix CHC false positives when using branches inside modifiers
2020-11-04 21:47:07 +00:00
Leonardo
62535c2fd4
Merge pull request #10181 from ethereum/smt_user_timeout
...
[SMTChecker] User timeout option
2020-11-04 10:55:28 +00:00
Leonardo Alt
daf859c15b
[SMTChecker] report SMTEncoder warnings also via CHC
2020-11-03 16:06:17 +00:00
chriseth
5ffee049fa
Merge remote-tracking branch 'origin/develop' into breaking
2020-11-03 14:05:14 +01:00
Leonardo Alt
d03ddeb0fa
[SMTChecker] User timeout option
2020-11-03 10:46:11 +00:00
