Martin Blicha
|
18214d1ccc
|
[SMTChecker] Reset checked/unchecked flag to the default value when inlining function in BMC
|
2021-01-15 15:36:26 +01:00 |
|
Leonardo Alt
|
007d39871b
|
[SMTChecker] Synthesize untrusted functions called externally
|
2021-01-15 11:56:26 +01:00 |
|
Martin Blicha
|
504e4c22b2
|
[SMTChecker] Fix in abi handling - tuple expression of size 1 has the type of the member and not TupleType
|
2021-01-14 14:53:56 +01:00 |
|
Martin Blicha
|
b4d2a71eec
|
[SMTChecker] Fix in abi handling - fixed missing type conversion
|
2021-01-14 14:53:44 +01:00 |
|
Martin Blicha
|
32a923c7ef
|
[SMTChecker] Fix in abi handling - abstracting expressions of type Function inside ABI functions when translating to SMT
|
2021-01-14 14:53:22 +01:00 |
|
Martin Blicha
|
5e13744423
|
[SMTChecker] Fixed pushing string literal to bytes array
|
2021-01-13 16:30:50 +01:00 |
|
Martin Blicha
|
7c6340fe4f
|
[SMTChecker] Refactoring expression to tuple assignment
|
2021-01-12 17:15:14 +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 |
|
Martin Blicha
|
ff76c989ac
|
addressing review comments
|
2021-01-11 14:19:06 +01:00 |
|
Martin Blicha
|
dd43ce1578
|
fixing try/catch encoding for BMC, refactoring
|
2021-01-11 13:36:03 +01:00 |
|
Martin Blicha
|
55589a9eec
|
[SMTChecker] Basic support for try-catch in BMC
|
2021-01-11 13:36:02 +01:00 |
|
Martin Blicha
|
0f3924186e
|
[SMTChecker] Support try-catch in CHC engine
|
2021-01-11 13:36:02 +01:00 |
|
Leonardo Alt
|
11f56861c3
|
Refactor cex loop
|
2021-01-07 23:13:02 +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
|
be0a0f4d90
|
[SMTChecker] Added constraints for block properties
|
2020-12-29 22:17:44 +01:00 |
|
Leonardo Alt
|
9482e7de23
|
[SMTChecker] Fix calls to virtual/overriden functions
|
2020-12-29 11:25:20 +01:00 |
|
Martin Blicha
|
bb0003f5ea
|
removed extra parameter from PredicateInstance::nondetInterface
|
2020-12-28 19:48:48 +01:00 |
|
Martin Blicha
|
f76ff35225
|
[SMTChecker] Detect errors caused by reentrancy
|
2020-12-28 14:32:53 +01:00 |
|
Martin Blicha
|
d90b9da4f0
|
[SMTChecker] Refactoring
|
2020-12-22 13:10:48 +01:00 |
|
Martin Blicha
|
87ef0e16f5
|
[SMTChecker] Fix virtual modifier called statically
|
2020-12-21 13:52:28 +01:00 |
|
Leonardo Alt
|
034d1ab90f
|
[SMTChecker] Replace constants by their value in-place
|
2020-12-18 14:22:28 +01:00 |
|
Martin Blicha
|
7078e8f8f8
|
[SMTChecker] Fix analysis of overriding modifiers
|
2020-12-17 17:05:54 +01:00 |
|
Leonardo Alt
|
2cbf33ca1c
|
SMTChecker support ABI functions as UFs
|
2020-12-17 14:03:17 +01:00 |
|
Leonardo Alt
|
f5c96ea6da
|
Fix constant evaluation build
|
2020-12-16 17:59:00 +01:00 |
|
chriseth
|
3a23df6717
|
Merge remote-tracking branch 'origin/develop' into breaking
|
2020-12-16 16:56:45 +01:00 |
|
Leonardo Alt
|
80e85b772b
|
[SMTChecker] Apply const eval to arithmetic binary expressions
|
2020-12-16 14:58:00 +01:00 |
|
chriseth
|
ffaf40950a
|
Merge pull request #10605 from ethereum/develop
Merge develop into breaking.
|
2020-12-15 14:01:01 +01:00 |
|
Martin Blicha
|
e2c27b8ea4
|
[SMTChecker] Fix internal error on constructor of a recursive struct
|
2020-12-15 09:53:52 +01:00 |
|
Martin Blicha
|
71f835b71b
|
[SMTChecker] Fixed internal error when increment/decrement is applied on a result of push().
|
2020-12-14 22:52:44 +01:00 |
|
Martin Blicha
|
103fa3b7eb
|
[SMTChecker] Fix internal error on abstract modifier
|
2020-12-14 18:23:25 +01:00 |
|
Martin Blicha
|
27402781c4
|
[SMTChecker] Fixed crash on push to bytes on lhs of an assignment
|
2020-12-14 17:40:45 +01:00 |
|
Martin Blicha
|
0be325dc0d
|
[SMTChecker] Fix handling of function calls where the function identifier is nested in a tuple.
|
2020-12-14 16:19:24 +01:00 |
|
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 |
|