cerc-io/solidity
11
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,011 Commits 348 Branches 121 Tags
stackLimitEvaderRefactor3
Commit Graph
462 Commits
Author SHA1 Message Date
Leonardo Alt 71144d0d39 [CHCChecker] Add CHCSolverInterface and Z3CHCSolverInterface 2019-07-15 17:31:39 +02:00
Leonardo 75eb67c3e0 Merge pull request #7050 from ethereum/smt_set_solver 
[SMTChecker] EncodingContext's solver needs to be set dynamically
 2019-07-08 15:19:55 +02:00
Leonardo Alt 96b0c4c148 [SMTChecker] New VariableUsage flag to inline functions 2019-07-08 14:40:33 +02:00
Leonardo Alt 01570bbc8c EncodingContext's solver needs to be set dynamically 2019-07-08 14:40:15 +02:00
chriseth 25928767b7 Merge pull request #7058 from ethereum/smt_reset_context 
[SMTChecker] Clear encoding context before engine starts
 2019-07-08 12:36:50 +02:00
Leonardo Alt be663680d4 [SMTChecker] Clear encoding context before engine starts 2019-07-08 11:56:04 +02:00
Leonardo Alt 4aebdcc442 [SMTChecker] Allow FunctionSort to be created via sort and not type 2019-07-04 12:00:24 +02:00
Leonardo Alt 934e00d235 [SMTChecker] SymbolicVariables use EncodingContext to declare SMT vars 2019-07-03 16:05:56 +02:00
chriseth 817852c650 Merge pull request #7030 from ethereum/smt_move_solver 
[SMTChecker] Move solver from SMTEncoder to BMC
 2019-07-02 14:08:55 +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 b0818bd002 [SMTChecker] Move solver pointer from SMTEncoder to BMC 2019-07-02 12:06:52 +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 ed275fd760 [SMTChecker] Collect assertions in EncodingContext 2019-06-24 15:03:00 +02:00
Leonardo Alt 1221eeebf1 [SMTChecker] Report malformed expressions more precisely 2019-06-06 11:54:29 +02:00
Leonardo Alt f281c94b42 [SMTChecker] Test that non-Boolean literals are actually integers 2019-06-05 10:51:05 +02:00
Leonardo 3a3316393e Merge pull request #6897 from ethereum/smt_check_pragma_earlier 
[SMTChecker] Exit early if no pragma
 2019-06-05 10:26:25 +02:00
Leonardo c39ea56f93 Merge pull request #6896 from ethereum/smt_use_portfolio 
[SMTChecker] Use SMTPortfolio directly
 2019-06-05 10:26:05 +02:00
Leonardo 155af48b9d Merge pull request #6895 from ethereum/smt_keep_assertions 
[SMTChecker] Keep a copy of assertions that are added to the solvers
 2019-06-05 10:25:45 +02:00
Leonardo Alt 4de1e20954 [SMTChecker] Exit early if no pragma 2019-06-04 17:12:15 +02:00
Leonardo Alt 91653526bb [SMTChecker] Use SMTPortfolio directly instead of pointer to SolverInterface 2019-06-04 17:10:52 +02:00
Leonardo Alt 31ef421fff [SMTChecker] Keep a copy of assertions that are added to the solvers 2019-06-04 17:09:04 +02:00
Leonardo Alt d9ce9cab99 [SMTChecker] Use smtlib's implies instead of \!a or b 2019-06-04 14:23:44 +02:00
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