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
14,260 Commits 348 Branches 121 Tags
b7d17c578d403024ef632b0abda7091d6060beb7
Commit Graph
277 Commits
Author SHA1 Message Date
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
chriseth 04f298fd0e Merge pull request #7132 from ethereum/smt_acc_solver 
[SMTChecker] EncodingContext config flag to accumulate assertions
 2019-08-01 13:04:37 +02:00
Leonardo Alt 44d7c6976a Erase pointer knowledge properly inside loops 2019-07-30 12:47:50 +02:00
Leonardo 00accd9daa Merge pull request #7141 from ethereum/smt_fix_json 
[SMTChecker] Reset SSA index to 0 instead of increasing in context reset
 2019-07-29 10:20:06 +02:00
Leonardo 0197a200cd Merge pull request #7142 from ethereum/smt_init_numbers 
[SMTChecker] Initialize all number types with 0
 2019-07-29 10:19:17 +02:00
Leonardo Alt 847f574e22 [SMTChecker] Fix ICE when inlining function with tuple expression 2019-07-26 16:29:29 +02:00
Leonardo Alt cd5a5b3686 [SMTChecker] Initialize all number types with 0 2019-07-25 15:15:18 +02:00
Leonardo Alt 6bcbeb1d23 [SMTChecker] Reset SSA index to 0 instead of increasing in context reset 2019-07-25 14:16:34 +02:00
Leonardo 264035f0dd Merge pull request #7120 from ethereum/smt_refactor_inlining 
[SMTChecker] Refactor function inlining
 2019-07-22 14:20:32 +02:00
Leonardo Alt b204f27047 [SMTChecker] EncodingContext config flag to accumulate assertions 2019-07-19 19:31:25 +02:00
Leonardo Alt 03cc124f32 Add CHC skeleton 2019-07-19 11:52:05 +02:00
Leonardo Alt 382df64899 [SMTChecker] Refactor function inlining 2019-07-18 13:56:48 +02:00
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