Mathias Baumann
e197ebbdd1
Replace TypePointer with Type const*
2021-03-23 11:47:19 +01:00
Leonardo Alt
998346e599
Fix bug in virtual functions called by constructor.
2021-03-12 16:42:28 +01:00
Leonardo Alt
6fd76e830d
Fix CHC cex order
2021-03-11 10:36:40 +01:00
Martin Blicha
4285c2803b
[SMTChecker] Fix ICE on array.pop nested inside 1-tuple
2021-03-09 20:00:51 +01:00
Leonardo
7405dc5b7f
Merge pull request #10836 from ethereum/smt_fix_cex_inheritance
...
Fix inheritance bug in CHC cex
2021-02-03 18:49:25 +01:00
Martin Blicha
d99256aae7
[SMTChecker] refactoring of resetting storage variables
2021-02-03 15:53:58 +01:00
Martin Blicha
f1013427a7
[SMTChecker] refactoring the accessing the encoding state
2021-02-03 15:53:58 +01:00
Leonardo Alt
665ce27c18
Fix inheritance bug in CHC cex
2021-02-02 18:06:32 +01: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
3b23cadbdc
Add CLI and JSON option to select SMTChecker targets
2021-01-20 17:35:37 +01:00
Leonardo Alt
007d39871b
[SMTChecker] Synthesize untrusted functions called externally
2021-01-15 11:56:26 +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
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
78d55e6b4a
[SMTChecker] Support check/unchecked
2020-12-30 12:14:30 +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
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
Daniel Kirchner
c400c61fc3
Fix incorrect behaviour on clang 6.
2020-12-10 17:20:30 +01:00
Daniel Kirchner
7308abc084
Allow loading Z3 dynamically at runtime.
2020-12-10 16:47:47 +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
Leonardo Alt
b7ac207391
[SMTChecker] Support return in CHC
2020-12-07 18:17:33 +01:00
Leonardo Alt
7490ffbe13
Use nonlinear clauses instead of inlining for base constructors
2020-12-04 13:25:56 +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
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
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
Leonardo Alt
d03ddeb0fa
[SMTChecker] User timeout option
2020-11-03 10:46:11 +00:00
Martin Blicha
c1a57ffbfe
[SMTChecker] More precise creation of verification targets.
2020-10-30 19:11:28 +01:00
Leonardo Alt
446e46fe06
Use Expression instead of plain strings for counterexamples
2020-10-27 12:04:51 +00:00
Martin Blicha
f0d81601db
[SMTChecker] Adding division by zero checks in the CHC engine
2020-10-21 14:48:33 +02:00
Leonardo Alt
cf35785328
Add unknown message to all verification targets
2020-10-19 20:54:13 +01:00
Leonardo
a097f9f124
Merge pull request #10025 from ethereum/smt_crypto_functions
...
[SMTChecker] Support crypto functions in CHC
2020-10-16 16:40:29 +01:00
Leonardo Alt
4e49135318
Add CLI option to choose model checker engine
2020-10-16 15:01:47 +01:00
Leonardo Alt
54f76e081a
[SMTChecker] Support crypto functions in CHC
2020-10-16 14:57:13 +01:00
Leonardo Alt
aec456021d
Add tx constraints to CHC
2020-10-13 17:49:04 +01:00
Leonardo Alt
18cf01c187
Add this and state to CHC
2020-10-12 11:11:52 +01:00
Leonardo Alt
c8cc73c80c
Support array slices
2020-10-01 11:52:02 +02:00
Leonardo Alt
352cce5fc8
[SMTChecker] Support addmod and mulmod.
2020-09-29 12:45:19 +02:00
