cerc-io/solidity
10
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,548 Commits 348 Branches 121 Tags 100 MiB
ac9b31d623
Commit Graph

77 Commits

Author SHA1 Message Date
Djordje Mijovic
26c43cfc66 [SMTChecker] Fix SMT logic error when doing compound assignment with string literlas. 2020-11-24 19:14:15 +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
Mathias Baumann
559b27aaad Natspec: Fix internal error when different return name was inherited 2020-11-17 11:56:32 +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
Mathias Baumann
32b4f18023 Print warning for unnamed return parameters and no return statement 2020-10-13 13:11:29 +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
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 Alt
df8c6d94e3 [SMTChecker] Support fixed bytes index access 2020-09-25 09:59:38 +02:00
Leonardo Alt
ebb6f61506 [SMTChecker] Decrease rlimit 2020-09-23 19:28:47 +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
28c8e01149 Readd SMTChecker tests 2020-09-14 23:44:13 +02:00
Leonardo Alt
3fea11e1a9 Remove problematic test 2020-09-11 22:02:18 +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 Alt
49d3804de4 [SMTChecker] Fix rational number short circuit 2020-09-01 17:21:13 +02:00
Leonardo Alt
50e0ada77d [SMTChecker] Fix unary operator on lvalue tuple 2020-09-01 08:25:06 +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
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