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
14,415 Commits 348 Branches 121 Tags 100 MiB
a78843baf7
Commit Graph

78 Commits

Author SHA1 Message Date
Leonardo Alt
214e5c6369 [SMTChecker] Fix index access type type error 2019-08-27 16:39:19 +02:00
Leonardo Alt
1a70a46f9b [CHC] Add function blocks and check asserts 2019-08-15 12:25:15 +02:00
Leonardo Alt
360f868836 [SMTChecker] Fix literal string type mismatch 2019-08-10 21:51:46 +02:00
Leonardo Alt
369f8cd97f [SMTChecker] CHC create function return variables 2019-08-05 12:36:51 +02:00
Leonardo
11632966c9
Merge pull request #7171 from ethereum/smt_fix_compound_bitwise 
[SMTChecker] Fix ICE compound bitwise op inside branch
 2019-08-05 12:15:01 +02:00
Leonardo Alt
d5fb8cf58a [SMTChecker] Fix ICE compound bitwise op inside branch 2019-08-02 20:02:39 +02:00
Leonardo Alt
7b5863e583 Do not erase knowledge about storage pointers when another pointer is assigned 2019-08-02 13:09:06 +02:00
Leonardo Alt
44d7c6976a Erase pointer knowledge properly inside loops 2019-07-30 12:47:50 +02:00
Leonardo Alt
847f574e22 [SMTChecker] Fix ICE when inlining function with tuple expression 2019-07-26 16:29:29 +02:00
chriseth
e542e46163
Merge pull request #7022 from ethereum/smt_create_expr 
[SMTChecker] Always create symbolic expression
 2019-07-02 14:07:24 +02:00
chriseth
ca10b59b25
Merge pull request #7020 from ethereum/smt_fix_callstack_message 
[SMTChecker] Fix wrong assertion in callstack message
 2019-07-02 13:47:49 +02:00
Leonardo Alt
fb3c85633b Always create symbolic expression 2019-07-01 16:25:33 +02:00
Leonardo Alt
75663dc91e [SMTChecker] Fix require with message 2019-07-01 16:17:06 +02:00
Leonardo Alt
6606a13ed2 [SMTChecker] Remove unsound assertion (too strong) 2019-07-01 16:16:39 +02:00
Leonardo Alt
3cb4ed83c1 [SMTChecker] Split SMTChecker into SMTEncoder and BMC 2019-07-01 15:05:03 +02:00
Leonardo Alt
a28b84fdc3 [SMTChecker] Add a more general VerificationTarget 2019-06-27 10:31:50 +02:00
Leonardo Alt
48d6729164 [SMTChecker] Remove overflow check for assignments 2019-06-24 17:58:56 +02:00
Leonardo Alt
60a4f03d3d [SMTChecker] Fix ice in unsupported functions with multi return values 2019-05-16 18:23:42 +02:00
Leonardo Alt
3ea5c112d3 [SMTChecker] Fix VariableUsage for IndexAccess 2019-05-10 11:28:10 +02:00
chriseth
89700dbcff
Merge pull request #6665 from ethereum/smt_inline_external_this 
[SMTChecker] Inline external function calls to `this`
 2019-05-09 19:09:08 +02:00
Leonardo Alt
ef32bf185f [SMTChecker] Inline external function calls to this. 2019-05-09 16:53:30 +02:00
Leonardo Alt
6027383ae5 [SMTChecker] Fix call to function at state var init 2019-05-09 16:12:44 +02:00
Leonardo Alt
3d52a6ca68 [SMTChecker] Fix ICE in branch-inline function call-modify local variable 2019-05-09 09:15:11 +02:00
Leonardo Alt
0b046897ae [SMTChecker] Fix unsupported type assignment 2019-05-08 14:28:23 +02:00
Leonardo Alt
3c7540ceb2 [SMTChecker] Support tuples with multiple var decls 2019-05-07 16:57:27 +02:00
Leonardo Alt
2139c20776 [SMTChecker] Support delete 2019-05-06 18:32:10 +02:00
Leonardo
e99efec085
Merge pull request #6652 from ethereum/smt_tuple_function 
[SMTChecker] Support tuples as function calls with multiple return values
 2019-05-06 15:19:24 +02:00
Leonardo Alt
80712f44cb Fix short circuit with assignments 2019-05-06 11:04:43 +02:00
Leonardo Alt
5440a53d4d [SMTChecker] Support tuples as function calls with multiple return values 2019-05-03 06:10:22 +02:00
Leonardo Alt
204dcf1771 [SMTChecker] Support tuple assignments 2019-05-02 12:55:34 +02:00
Leonardo Alt
6c7527ac90 [SMTChecker] Support tuple type declaration 2019-05-02 12:05:21 +02:00
Leonardo Alt
dd4e938265 [SMTChecker] Fix ICE in inherited state var 2019-05-02 10:03:12 +02:00
Leonardo Alt
a6db37ac9c [SMTChecker] Fix bad cast in base constructor modifier. 2019-04-30 18:48:13 +02:00
Leonardo Alt
fc482de695 [SMTChecker] Support address members 2019-04-25 16:24:36 +02:00
Leonardo Alt
dd1afeba52 [SMTChecker] Support this as address 2019-04-18 17:56:52 +02:00
Leonardo Alt
ecd89393ee [SMTChecker] Support contract type 2019-04-17 16:30:11 +02:00
Mathias Baumann
efc8d79d53 Fix wrong location for inline asm blocks 2019-04-15 16:40:07 +02:00
chriseth
bf5792f7ca
Merge pull request #6483 from ethereum/smt_support_mod 
[SMTChecker] Support mod
 2019-04-15 13:42:18 +02:00
chriseth
73ac8f6220
Merge pull request #6421 from ethereum/smt_fix_variable_usage 
[SMTChecker] Refactor VariableUsage
 2019-04-15 13:39:10 +02:00
Leonardo Alt
af9f16e014 [SMTChecker] Support mod 2019-04-12 12:39:25 +02:00
Leonardo Alt
4fe303530a [SMTChecker] Show unsupported warning for asm blocks 2019-04-05 16:41:15 +02:00
Leonardo Alt
79d8a4e13a [SMTChecker] Refactor VariableUsage 2019-04-05 11:38:37 +02:00
Leonardo Alt
aa9b9aa87e [SMTChecker] Support unary inc/dec for array/mapping access 2019-04-02 16:53:19 +02:00
chriseth
84251e5a22
Merge pull request #6405 from ethereum/smt_compound_assignment 
[SMTChecker] Support arithmetic compound assignment operators.
 2019-03-28 18:27:25 +01:00
Leonardo Alt
dadafed022 Short circuit tests 2019-03-28 16:08:30 +01:00
Leonardo Alt
a7e826a224 [SMTChecker] Implement short circuit 2019-03-28 16:08:30 +01:00
Leonardo Alt
c7e5468505 Arithmetic compound assignment operators tests 2019-03-28 15:27:52 +01:00
Leonardo Alt
2764d2f525 Tests that used to give false negatives 2019-03-28 14:32:47 +01:00
Leonardo Alt
2ae778bf0a [SMTChecker] Add buggy short circuit test 2019-03-21 18:47:14 +01:00
Leonardo Alt
9659f40c8d [SMTChecker] Support modifiers 2019-03-20 11:32:20 +01:00