chriseth
0dd2f1edbe
Update counter-examples.
2020-12-14 14:21:35 +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
Leonardo Alt
64f81fe82b
Fix SMT tests
2020-12-10 18:54:52 +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
chriseth
b18c76e34b
Merge remote-tracking branch 'origin/develop' into breaking
2020-12-09 15:24:49 +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
chriseth
b045195c1e
Merge remote-tracking branch 'origin/develop' into breaking
2020-12-08 17:42:31 +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
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
hrkrshnn
9e5d7b9910
Test updates after disallowing Integer -> Contract conversion
2020-12-03 17:53:00 +01:00
hrkrshnn
40244c5469
Tests/Docs after stricter explicit conversion.
2020-12-03 16:51:05 +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
hrkrshnn
a834476de6
Tests/Docs after disallowing super, this and _ as declaration names
2020-11-25 11:14:13 +01:00
chriseth
f01cd3f38f
Fix merge conflicts
2020-11-25 08:09:38 +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
chriseth
79669ecd48
Use new abicoder pragma.
2020-11-24 14:57:45 +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 Alt
e4339b0526
[SMTChecker] Support named arguments in function calls
2020-11-20 11:52:26 -01:00
chriseth
e8a278eefa
Merge remote-tracking branch 'origin/develop' into breaking
2020-11-17 18:51:57 +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
hrkrshnn
2348b721bb
Tests after changing type of super to TypeType
2020-11-10 15:38:21 +01: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
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
hrkrshnn
29e23efc93
Tests/Docs after "stricter explicit conversion from Literals to Integers"
2020-11-03 14:31:44 +01:00
chriseth
5ffee049fa
Merge remote-tracking branch 'origin/develop' into breaking
2020-11-03 14:05:14 +01: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
