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
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
Martin Blicha
de34fe8aa3
[SMTChecker] Adding test witnessing that SMTChecker no longer crashes when producing CEX with arrays
2020-12-09 09:13:39 +01:00
Martin Blicha
12aa654bad
added test
2020-12-08 13:05:16 +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
Leonardo Alt
7490ffbe13
Use nonlinear clauses instead of inlining for base constructors
2020-12-04 13:25:56 +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
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
Djordje Mijovic
26c43cfc66
[SMTChecker] Fix SMT logic error when doing compound assignment with string literlas.
2020-11-24 19:14:15 +01:00
chriseth
79669ecd48
Use new abicoder pragma.
2020-11-24 14:57:45 +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 Alt
e4339b0526
[SMTChecker] Support named arguments in function calls
2020-11-20 11:52:26 -01:00
chriseth
bb97363abf
Merge pull request #9989 from ethereum/issue-9947
...
Natspec: Fix internal error when different return name was inherited
2020-11-17 13:54:03 +01:00
Mathias Baumann
559b27aaad
Natspec: Fix internal error when different return name was inherited
2020-11-17 11:56:32 +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
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
00858c0ccf
Isoltets SMTChecker option and BMC specific tests
2020-11-06 15:03:38 +00:00
Leonardo Alt
1dbd8f8d67
Fix CHC false positives when using branches inside modifiers
2020-11-04 21:47:07 +00:00
Leonardo Alt
daf859c15b
[SMTChecker] report SMTEncoder warnings also via CHC
2020-11-03 16:06:17 +00:00
Leonardo Alt
e38d0db683
[SMTChecker] Fix internal error when array.push() is used as LHS of assignment
2020-11-02 13:32:53 +00:00
Leonardo Alt
94e2506132
Fix inherited state vars for BMC
2020-11-02 11:42:39 +00:00
Martin Blicha
c1a57ffbfe
[SMTChecker] More precise creation of verification targets.
2020-10-30 19:11:28 +01:00
Đorđe Mijović
1f50b86aad
Merge pull request #10073 from ethereum/smt_format_array_cex
...
Format array cex
2020-10-28 12:39:19 +01:00
Leonardo Alt
25f75ce547
Remove nondet tests
2020-10-28 11:03:42 +00:00
Leonardo
07c454949f
Merge pull request #10127 from ethereum/fixIceSmtBitwise
...
[SMTChecker] Fix ICE when using >>>
2020-10-28 09:28:18 +00:00
Djordje Mijovic
9cc37c3fa4
[SMTChecker] Fix ICE when using >>>
2020-10-28 09:25:14 +01:00
Leonardo Alt
4755cfe157
Fix assignment to contract member access
2020-10-26 14:39:02 +00:00
Leonardo Alt
d3d77e482c
Fix ICE on conditions with tuples of rationals
2020-10-23 14:47:53 +01:00
Martin Blicha
ade3b9951c
[SMTChecker] Added support for selector when expression's value is known at compile time
2020-10-22 14:18:52 +02:00
Leonardo Alt
b087fa9750
[SMTChecker] Fix ICE implicit conversion string literal -> byte
2020-10-21 22:03:01 +01: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
Martin Blicha
8c351278ac
[SMTChecker] added test to check correct handling of the sign of the modulo operation
2020-10-16 16:17:32 +02:00
Martin Blicha
78c8fbc7ce
[SMTChecker] encoding division and modulo operations using slack variables
2020-10-16 16:06:31 +02:00
Leonardo Alt
54f76e081a
[SMTChecker] Support crypto functions in CHC
2020-10-16 14:57:13 +01:00
Leonardo Alt
88f783bb1e
Remove more tests because current Spacer crashes
2020-10-13 19:27:49 +01:00
Leonardo Alt
b9b9c229b4
New tests
2020-10-13 17:49:04 +01:00
Leonardo Alt
47b268d509
Update tests
2020-10-13 17:49:04 +01:00
Leonardo Alt
aec456021d
Add tx constraints to CHC
2020-10-13 17:49:04 +01:00
Mathias Baumann
32b4f18023
Print warning for unnamed return parameters and no return statement
2020-10-13 13:11:29 +02:00
Djordje Mijovic
e23d8f5593
[SMTChecker] Supporting inline arrays.
2020-10-12 16:59:14 +02:00
Leonardo Alt
3d2e6252f0
Add/update tests
2020-10-12 11:11:52 +01:00
Leonardo Alt
18cf01c187
Add this and state to CHC
2020-10-12 11:11:52 +01:00
