Commit Graph
234 Commits
Author SHA1 Message Date
chriseth e08f521b7e Merge pull request #6764 from ethereum/smt_fix_tuple_ice
[SMTChecker] Fix ICE in unsupported function calls with multi return values
2019-05-20 15:18:11 +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 5493a41842 [SMTChecker] Move global variables and functions to encoding context 2019-05-16 18:11:31 +02:00
Leonardo Alt 4e430ba0ae [SMTChecker] Move expression handling to EncodingContext 2019-05-14 15:56:43 +02:00
Leonardo Alt ebbe03cad6 [SMTChecker] Move variable handling to EncodingContext 2019-05-13 16:59:28 +02:00
chriseth 01dd9ba2ae Merge pull request #6717 from ethereum/smt_namespace
Move SMT specific code into smt namespace
2019-05-13 12:45:34 +02:00
chriseth e5d46767f1 Merge pull request #6722 from ethereum/smt_fix_variable_usage
[SMTChecker] Fix VariableUsage for IndexAccess
2019-05-13 10:17:26 +02:00
Leonardo Alt fac383a233 Move SMT specific code into smt namespace 2019-05-10 20:03:11 +02:00
chriseth cc40e65a4b Merge pull request #6712 from ethereum/smt_unique_ptr
[SMTChecker] Use unique_ptr instead of shared_ptr where applicable
2019-05-10 12:53:53 +02:00
Leonardo Alt 3ea5c112d3 [SMTChecker] Fix VariableUsage for IndexAccess 2019-05-10 11:28:10 +02:00
Leonardo Alt 8d65fd18fc [SMTChecker] Style changes 2019-05-09 19:15:43 +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 c8a017ccd6 [SMTChecker] Use unique_ptr instead of shared_ptr where applicable. 2019-05-09 16:34:22 +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 9893cae27a [SMTChecker] Make mergeVariables deterministic 2019-05-08 20:46:01 +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 66655b87b0 [SMTChecker] Fix ICE in fixed point operations 2019-05-02 10:59:23 +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 e4989369d0 Refactor cast from identifier ref decl to var decl 2019-04-30 11:08:36 +02:00
Leonardo Alt 762f79f84d Refactor assignment handling 2019-04-30 11:08:36 +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
chriseth fce19bde58 Merge pull request #6545 from ethereum/smt_contracts
[SMTChecker] Support contract type
2019-04-18 13:01:18 +02:00
Leonardo Alt ecd89393ee [SMTChecker] Support contract type 2019-04-17 16:30:11 +02:00
Leonardo Alt 03d18f1b98 [SMTChecker] Add note about not inlining external function calls 2019-04-17 16:14:07 +02:00
Christian Parpart 721bf367a3 [libsolidity] TypeProvider: eliminate redundant "Type" suffix in provider function signatures. 2019-04-17 14:42:07 +02:00
Christian Parpart 862b65d6e3 [libsolidity] remove ReferenceType::copyForLocationIfReference (use TypeProvider instead) 2019-04-17 13:25:03 +02:00
Christian Parpart 58a45f2cb6 [libsolidity] TypeProvider: adds explicit uint256() accessor and removes default params in integerType(...). 2019-04-16 18:28:40 +02:00
Christian Parpart bf43eebea9 libsolidity: Introducing TypeProvider API, for clear type system ownership. 2019-04-16 18:26:45 +02:00
Leonardo Alt 07fac9e381 [SMTChecker] Allow SymbolicVariable from smt::Sort 2019-04-15 14:52:46 +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 a7e826a224 [SMTChecker] Implement short circuit 2019-03-28 16:08:30 +01:00
Leonardo Alt 15269067b5 Support arithmetic compound assignment operators 2019-03-28 15:27:52 +01:00
Leonardo Alt ecbf36f271 Refactor computing symbolic arithmetic operation 2019-03-28 15:27:36 +01:00