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 |
|
chriseth
|
e93a84ccd4
|
Merge remote-tracking branch 'origin/develop' into HEAD
|
2020-10-28 18:19:31 +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 |
|
hrkrshnn
|
0e30fbbae1
|
Fix failing SMTChecker test on breaking
|
2020-10-26 14:01:40 +01:00 |
|
Leonardo Alt
|
d3d77e482c
|
Fix ICE on conditions with tuples of rationals
|
2020-10-23 14:47:53 +01:00 |
|
chriseth
|
20f39ab6e9
|
Merge pull request #10097 from ethereum/develop
Merge develop into breaking.
|
2020-10-23 10:30:24 +02:00 |
|
chriseth
|
bfc8e26007
|
Remove low-level log functions.
|
2020-10-22 17:50:14 +02: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 |
|
chriseth
|
6979952995
|
Merge remote-tracking branch 'origin/develop' into HEAD
|
2020-10-19 18:02:50 +02: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 |
|
chriseth
|
979d3062bc
|
Merge pull request #10033 from ethereum/develop
Merge develop into breaking
|
2020-10-14 14:12:20 +02: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 |
|
chriseth
|
f6e57a0eec
|
Merge pull request #10023 from ethereum/develop
Merge develop into breaking.
|
2020-10-13 18:18:53 +02:00 |
|
Mathias Baumann
|
006e5f2e1f
|
Allow path syntax for super constructor calls
|
2020-10-13 14:32:11 +02:00 |
|
Mathias Baumann
|
32b4f18023
|
Print warning for unnamed return parameters and no return statement
|
2020-10-13 13:11:29 +02:00 |
|
chriseth
|
0ea4bdafcd
|
Merge pull request #10017 from ethereum/develop
Merge develop into breaking.
|
2020-10-13 12:58:23 +02:00 |
|
Djordje Mijovic
|
e23d8f5593
|
[SMTChecker] Supporting inline arrays.
|
2020-10-12 16:59:14 +02:00 |
|
chriseth
|
8a1bf41ac0
|
Merge pull request #10010 from ethereum/develop
Merge develop into breaking.
|
2020-10-12 15:33:34 +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 |
|
a3d4
|
f29ebc0847
|
Fix shadowing/same-name warnings for later declarations
|
2020-10-08 20:22:04 +02:00 |
|
Harikrishnan Mulackal
|
a309669f75
|
Disallow explicit conversions from negative literals to `address`
|
2020-10-07 16:06:02 +02:00 |
|
Alex Beregszaszi
|
fedbea46cd
|
[SMTChecker] Support type conversions
|
2020-10-02 10:26:02 +02:00 |
|
Leonardo Alt
|
c8cc73c80c
|
Support array slices
|
2020-10-01 11:52:02 +02:00 |
|
Mathias Baumann
|
4c02cd2310
|
Add name for split-test to prevent failure in other places
|
2020-09-30 16:56:53 +02:00 |
|
Leonardo Alt
|
352cce5fc8
|
[SMTChecker] Support addmod and mulmod.
|
2020-09-29 12:45:19 +02:00 |
|
Leonardo Alt
|
fa7c9a0dc6
|
Simplify internal function calls
|
2020-09-28 15:31:15 +02:00 |
|
Leonardo Alt
|
e6bd18525b
|
[SMTChecker] Add engine prefix to verification target error messages
|
2020-09-25 19:09:06 +02:00 |
|
Leonardo Alt
|
0223571987
|
[SMTChecker] Do not report error when rlimit
|
2020-09-25 18:43:10 +02:00 |
|
Alex Beregszaszi
|
9f3d5d3e2f
|
[SMTChecker] Implement support for memory allocation
|
2020-09-25 15:56:24 +01:00 |
|
Alex Beregszaszi
|
9c1b041dcb
|
[SMTChecker] Keep constraints of string literals after assignment
|
2020-09-25 11:32:48 +01:00 |
|
Alex Beregszaszi
|
5090353a1a
|
[SMTChecker] Keep knowledge about string literals
|
2020-09-25 11:32:23 +01:00 |
|
Leonardo
|
57e1b2cb92
|
Merge pull request #9881 from ethereum/smt_fixed_bytes_index_access
[SMTChecker] Support fixed bytes index access
|
2020-09-25 11:32:56 +02:00 |
|
Leonardo Alt
|
df8c6d94e3
|
[SMTChecker] Support fixed bytes index access
|
2020-09-25 09:59:38 +02:00 |
|
Alex Beregszaszi
|
6edfdff187
|
[SMTChecker] Do not warn on "abi" as an identifer
There is an approprate warning for the function call.
|
2020-09-24 13:57:42 +01:00 |
|
chriseth
|
a9f9b4db27
|
Merge pull request #9872 from ethereum/smt_remove_tests
Extract boost smt and remove unused tests
|
2020-09-24 13:20:19 +02:00 |
|
Leonardo Alt
|
ebb6f61506
|
[SMTChecker] Decrease rlimit
|
2020-09-23 19:28:47 +02:00 |
|
Leonardo Alt
|
8eba66daf9
|
Extract boost smt and remove unused tests
|
2020-09-23 17:55:55 +02:00 |
|
Đorđe Mijović
|
858b4507e2
|
Merge pull request #9854 from ethereum/bitwiseSmt
[SMTChecker] Support compound shifts and bitwise and, or, and xor
|
2020-09-23 12:35:48 +02:00 |
|
Djordje Mijovic
|
96bafb9ba3
|
[SMTChecker] Updating old and adding new tests for compound shift operators.
|
2020-09-23 11:31:37 +02:00 |
|
Djordje Mijovic
|
0193952106
|
[SMTChecker] Updating old and adding new tests for compound bitwise xor operator.
|
2020-09-23 11:31:37 +02:00 |
|
Djordje Mijovic
|
e2e0b33ee7
|
[SMTChecker] Updating old and adding new tests for compound bitwise or operator.
|
2020-09-23 11:31:41 +02:00 |
|
Djordje Mijovic
|
69df163dcb
|
[SMTChecker] Updating old and adding new tests for compound bitwise and operator.
|
2020-09-23 11:31:37 +02:00 |
|
Leonardo Alt
|
f4ee4cd479
|
Update tests
|
2020-09-22 20:51:28 +02:00 |
|
Alex Beregszaszi
|
709d25bd3d
|
[SMTChecker] Support address type conversion with literals
|
2020-09-22 18:49:11 +01:00 |
|
Alex Beregszaszi
|
c8c17b693b
|
[SMTChecker] Support events and low-level logs
|
2020-09-16 11:50:39 +02:00 |
|
Alex Beregszaszi
|
783d66c1a4
|
[SMTChecker] Support revert()
|
2020-09-15 11:46:33 +01:00 |
|
Alex Beregszaszi
|
8f36408ef9
|
Add test case for revert() in SMTChecker
|
2020-09-15 11:46:16 +01:00 |
|
Daniel Kirchner
|
e93d74398b
|
Merge pull request #9807 from ethereum/smt_readd_tests
Readd SMTChecker tests
|
2020-09-15 02:57:42 +02:00 |
|
Leonardo Alt
|
28c8e01149
|
Readd SMTChecker tests
|
2020-09-14 23:44:13 +02:00 |
|
Alex Beregszaszi
|
83934254ea
|
[SMTChecker] Support type(I).interfaceId
|
2020-09-14 20:34:52 +01:00 |
|
Leonardo Alt
|
fd6c665548
|
Update SMTChecker tests with z3 4.8.9
|
2020-09-14 19:04:13 +02:00 |
|
Leonardo
|
31b5102aa0
|
Merge pull request #9731 from ethereum/smt_import
[SMTChecker] Fix CHC encoding
|
2020-09-12 00:56:04 +02:00 |
|
Alex Beregszaszi
|
961a199cf5
|
[SMTChecker] Support type(T).min and type(T).max
|
2020-09-11 21:37:51 +01:00 |
|
Leonardo Alt
|
3fea11e1a9
|
Remove problematic test
|
2020-09-11 22:02:18 +02:00 |
|
Leonardo Alt
|
23ee011c56
|
[SMTChecker] Fix imports
|
2020-09-11 13:34:46 +02:00 |
|
Leonardo Alt
|
84c707cd2a
|
Adjust problematic SMTChecker tests
|
2020-09-10 19:32:17 +02:00 |
|
Leonardo Alt
|
40197df104
|
[SMTChecker] Support shifts
|
2020-09-09 19:47:52 +02:00 |
|
Leonardo Alt
|
00f6b303b1
|
[SMTChecker] Change warning message
|
2020-09-09 16:14:21 +02:00 |
|
Leonardo Alt
|
69a7808838
|
Add new tests
|
2020-09-03 15:19:33 +02:00 |
|
Leonardo Alt
|
afcd44e77c
|
Update current tests
|
2020-09-03 15:19:03 +02:00 |
|
Leonardo
|
0d83977d5a
|
Merge pull request #9648 from ethereum/smt_refactor_predicates
[SMTChecker] Refactor CHC predicates
|
2020-09-01 20:38:47 +02:00 |
|
Leonardo Alt
|
49d3804de4
|
[SMTChecker] Fix rational number short circuit
|
2020-09-01 17:21:13 +02:00 |
|
Leonardo Alt
|
e23d96464b
|
Adjust test
|
2020-09-01 16:10:12 +02:00 |
|
Leonardo Alt
|
016b9b83a8
|
Refactor predicates
|
2020-09-01 16:09:56 +02:00 |
|
Leonardo Alt
|
238b8a929e
|
[SMTChecker] Fix ICE on tuples of one element that actually have tuple type
|
2020-09-01 08:31:57 +02:00 |
|
Leonardo Alt
|
5cafbeebec
|
[SMTChecker] Fix ICE on tuple assignment
|
2020-09-01 08:29:01 +02:00 |
|
Leonardo Alt
|
50e0ada77d
|
[SMTChecker] Fix unary operator on lvalue tuple
|
2020-09-01 08:25:06 +02:00 |
|
Leonardo Alt
|
8c05db88c0
|
[SMTChecker] Fix soundness of array pop
|
2020-08-31 12:11:33 +02:00 |
|
Djordje Mijovic
|
11a7763f49
|
[SMTChecker] Support bitwise or, xor and not.
|
2020-08-26 11:06:56 +02:00 |
|
Djordje Mijovic
|
00e765f478
|
Fix tests for conditional operator on latest develop.
|
2020-08-22 07:52:55 +02:00 |
|
Đorđe Mijović
|
4dd25f7302
|
Merge pull request #9639 from ethereum/smtConditionalSupport
[SMTChecker] Supporting conditional operator
|
2020-08-21 14:25:47 +02:00 |
|
Djordje Mijovic
|
3f97a1012a
|
[SMTChecker] Supporting conditional operator
|
2020-08-20 21:39:35 +02:00 |
|
Leonardo Alt
|
5afd1219f5
|
Add test with unused error id
|
2020-08-14 12:58:27 +02:00 |
|
Leonardo Alt
|
0a160b1ba0
|
Update remaining tests
|
2020-08-14 12:58:27 +02:00 |
|
Leonardo Alt
|
80ab56dbc6
|
Update overflow tests
|
2020-08-14 12:58:27 +02:00 |
|
Leonardo Alt
|
8a06041bbe
|
[SMTChecker] Add underflow/overflow target to CHC
|
2020-08-14 12:58:27 +02:00 |
|
Leonardo Alt
|
ec31d971e6
|
[SMTChecker] Fix tuple name for arrays
|
2020-08-07 12:28:10 +02:00 |
|
chriseth
|
3a409c39e4
|
Merge pull request #9518 from ethereum/smt_fix_bmc_function_inlining
[SMTChecker] Fix ICE in BMC function inlining
|
2020-08-06 00:50:04 +02:00 |
|
Leonardo Alt
|
8df8c6e14f
|
[SMTChecker] Fix ICE in BMC function inlining
|
2020-08-05 11:47:25 +02:00 |
|
Leonardo Alt
|
55624d6416
|
Add test from Aon blog post
|
2020-08-04 09:31:48 +02:00 |
|