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
17,947 Commits 348 Branches 121 Tags 100 MiB
c0954be254
Commit Graph

243 Commits

Author SHA1 Message Date
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