Commit Graph

314 Commits

Author SHA1 Message Date
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
Leonardo Alt
ad1798b000 [SMTChecker] Fix ICE on fixed bytes access 2020-07-28 17:59:42 +02:00
Leonardo Alt
a6df232fa3 Fix SMT tests 2020-07-28 11:24:25 +02:00
chriseth
9605b85c21
Merge pull request #9352 from ethereum/smt_cex
[SMTChecker] CHC counterexamples
2020-07-27 19:21:04 +02:00
Leonardo Alt
b207222af7 Fix extra parens 2020-07-27 17:14:59 +02:00
Leonardo Alt
de4ae301c4 [SMTChecker] Fix ICE when tuples have extra effectless parens 2020-07-27 13:03:27 +02:00
Leonardo Alt
95484d9969 Fix tests after rebase 2020-07-23 18:49:03 +02:00
Leonardo Alt
d70ebbb62d Remove problematic test 2020-07-23 18:49:03 +02:00
Leonardo Alt
5bb4e73693 Review 1 2020-07-23 18:49:03 +02:00
Leonardo Alt
003c9b9a5b Update tests 2020-07-23 18:49:03 +02:00
Leonardo Alt
9d2a0947e9 Fix 1-tuple chain 2020-07-23 13:46:41 +02:00
chriseth
6bb6783d39 Merge remote-tracking branch 'origin/develop' into breaking 2020-07-22 15:26:44 +02:00
chriseth
9be5ed1220 Merge remote-tracking branch 'origin/develop' into breaking 2020-07-21 11:35:28 +02:00
Leonardo Alt
2c93278719 Fix push().push() 2020-07-20 17:17:35 +02:00
Leonardo Alt
2e1067a05a Set type properly for event parameters 2020-07-17 11:17:27 +02:00
Leonardo Alt
672633af0a [SMTChecker] Fix ICE on compound assignment to array index 2020-07-16 17:44:10 +02:00
chriseth
f945163909
Merge pull request #9432 from ethereum/develop
Merge develop into breaking.
2020-07-16 17:14:45 +02:00
Leonardo Alt
46653b2d43 Fix ICE when bitwise operator on fixed bytes 2020-07-15 19:32:15 +02:00
chriseth
9743390a53 Update tests. 2020-07-07 12:16:18 +02:00
chriseth
ab68406006 Merge remote-tracking branch 'origin/develop' into breaking 2020-07-06 15:25:25 +02:00
Leonardo Alt
5517e817d5 Do not trust code of external functions 2020-07-01 18:20:46 +02:00
Leonardo Alt
5160f89c1b [SMTChecker] Support to external calls to unknown code 2020-07-01 18:20:33 +02:00
chriseth
d67734df6f Fix error IDs. 2020-06-22 18:56:32 +02:00
chriseth
1441b97131 Merge remote-tracking branch 'origin/develop' into breaking 2020-06-22 18:40:20 +02:00
a3d4
e04cedafc5 Added error codes to SyntaxTest expectations (updated tests) 2020-06-22 16:51:47 +02:00
chriseth
8155ad2187 Merge remote-tracking branch 'origin/develop' into breaking 2020-06-15 17:11:41 +02:00
Leonardo Alt
3c4e286390 [SMTChecker] Replace wrap mod by slack vars 2020-06-12 14:57:21 +02:00
chriseth
6b3171c38b Merge remote-tracking branch 'origin/develop' into breaking 2020-06-10 11:30:50 +02:00
Leonardo Alt
f49e2424b2 [SMTChecker] Erase knowledge when array variable is pushed 2020-06-08 10:23:06 +02:00
Leonardo
d243f5baac
Merge pull request #9045 from ethereum/smt_fix_tuple
[SMTChecker] Fix internal error in tuples of tuples.
2020-06-05 14:21:32 +02:00
Leonardo
731e6466a0
Merge pull request #9067 from ethereum/smt_fix_fp_again
[SMTChecker] Fix BMC targets with FP
2020-06-05 12:39:28 +02:00
Leonardo Alt
87ceb72b82 [SMTChecker] Fix internal error in tuples of tuples. 2020-06-05 12:20:47 +02:00
chriseth
c8b9d24eba
Merge pull request #9106 from ethereum/develop
Merge develop into breaking.
2020-06-03 13:51:28 +02:00