cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity
18,450 Commits 348 Branches 121 Tags 100 MiB
141277dadf
Commit Graph

301 Commits

Author SHA1 Message Date
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
Leonardo Alt
10162016ae [SMTChecker] Fix internal error on try/catch 2020-06-02 16:51:53 +02:00
Leonardo
97cb091ada
Merge pull request #9068 from ethereum/smt_fix_state_var_init_call 
[SMTChecker] Relax assertion about callstack
 2020-06-02 15:53:14 +02:00
Leonardo Alt
ede39fc2da [SMTChecker] Relax assertion about callstack 2020-06-02 12:50:51 +02:00
Leonardo Alt
2128ff9f13 Fix ICE on push for member access 2020-05-29 19:13:27 +02:00
Leonardo Alt
e5d25692a5 [SMTChecker] Fix BMC targets with FP 2020-05-29 18:13:13 +02:00
chriseth
0b216f5771
Merge pull request #9050 from ethereum/smt_fix_nonvalue_asgn 
[SMTChecker] Fix ICE on index access assignment inside single branches
 2020-05-28 16:25:46 +02:00
Leonardo
1051cea91c
Merge pull request #9052 from ethereum/smt_add_test_delete_m_d_array 
[SMTChecker] Add test that deletes arrays
 2020-05-28 16:14:55 +02:00
Leonardo Alt
9b0146be42 Add test 2020-05-28 15:56:47 +02:00
Leonardo Alt
ec766958ea Add test 2020-05-28 13:14:21 +02:00
Leonardo Alt
13f32268da [SMTChecker] Add test that shows that deleting arrays takes the index into account 2020-05-28 13:08:16 +02:00
Leonardo Alt
9e9f0c52e1 [SMTChecker] Support to bitwise 2020-05-27 20:59:00 +02:00
chriseth
69a028b49c Merge remote-tracking branch 'origin/develop' into breaking 2020-05-26 10:11:23 +02:00
Leonardo Alt
0fda5fe077 [SMTChecker] Add test that has an unused mapping 2020-05-25 10:24:48 +02:00