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
Martin Blicha
ff76c989ac
addressing review comments
2021-01-11 14:19:06 +01:00
Martin Blicha
3d7188ac7b
update to the tests
2021-01-11 13:36:03 +01:00
Martin Blicha
dd43ce1578
fixing try/catch encoding for BMC, refactoring
2021-01-11 13:36:03 +01:00
Martin Blicha
064e9a5de6
Changelog entry
2021-01-11 13:36:03 +01:00
Martin Blicha
09de54b5eb
tests
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
Martin Blicha
be0a0f4d90
[SMTChecker] Added constraints for block properties
2020-12-29 22:17:44 +01:00
Martin Blicha
41d31fe4d4
updates to the tests
2020-12-28 20:05:52 +01:00
Martin Blicha
bb0003f5ea
removed extra parameter from PredicateInstance::nondetInterface
2020-12-28 19:48:48 +01:00
Martin Blicha
58731056a3
Changelog entry
2020-12-28 16:50:04 +01:00
Martin Blicha
77dff222e9
disabling some tests because of nondeterminism in Spacer
2020-12-28 16:24:44 +01:00
Martin Blicha
745466b71f
updates to the tests
2020-12-28 14:32:53 +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
Martin Blicha
7078e8f8f8
[SMTChecker] Fix analysis of overriding modifiers
2020-12-17 17:05:54 +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
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
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
eb356735f6
[SMTChecker] Adding support for reporting values of structs in CEX in CHC engine.
2020-12-08 16:40:28 +01:00
Martin Blicha
12aa654bad
added test
2020-12-08 13:05:16 +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
Martin Blicha
2ee633f404
[SMTChecker] Added support for public getters through this.
2020-12-02 16:06:48 +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
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
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
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
Martin Blicha
c1a57ffbfe
[SMTChecker] More precise creation of verification targets.
2020-10-30 19:11:28 +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
Martin Blicha
f0d81601db
[SMTChecker] Adding division by zero checks in the CHC engine
2020-10-21 14:48:33 +02:00
Martin Blicha
1511f59a7e
Warning 1218 'CHC: Error trying to invoke SMT solver' no longer happens in the tests
2020-10-16 16:17:32 +02: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
Martin Blicha