Leonardo Alt
|
a612daa783
|
Add msgvalue to cex
|
2021-01-21 19:05:44 +01:00 |
|
Leonardo Alt
|
007d39871b
|
[SMTChecker] Synthesize untrusted functions called externally
|
2021-01-15 11:56:26 +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 |
|
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 |
|
Martin Blicha
|
745466b71f
|
updates to the tests
|
2020-12-28 14:32:53 +01:00 |
|
Leonardo Alt
|
50be39fc21
|
Add and update tests
|
2020-12-17 14:42:49 +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
|
71f835b71b
|
[SMTChecker] Fixed internal error when increment/decrement is applied on a result of push().
|
2020-12-14 22:52:44 +01:00 |
|
Alex Beregszaszi
|
edbdff8619
|
Update tests
|
2020-12-14 19:32:31 +00: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 |
|
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
|
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
|
d56a7bb89e
|
Merge pull request #10489 from ethereum/develop
Merge develop into breaking.
|
2020-12-03 18:11:12 +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 |
|
Djordje Mijovic
|
26c43cfc66
|
[SMTChecker] Fix SMT logic error when doing compound assignment with string literlas.
|
2020-11-24 19:14:15 +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 |
|
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 |
|
Mathias Baumann
|
559b27aaad
|
Natspec: Fix internal error when different return name was inherited
|
2020-11-17 11:56:32 +01:00 |
|
hrkrshnn
|
29e23efc93
|
Tests/Docs after "stricter explicit conversion from Literals to Integers"
|
2020-11-03 14:31:44 +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 |
|
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 |
|
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 |
|
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
|
88f783bb1e
|
Remove more tests because current Spacer crashes
|
2020-10-13 19:27:49 +01:00 |
|
Leonardo Alt
|
47b268d509
|
Update tests
|
2020-10-13 17:49:04 +01:00 |
|