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,519 Commits 348 Branches 121 Tags
f8e6f4a4eb06c2a82a744f66910f13a376e519ff
Commit Graph
506 Commits
Author SHA1 Message Date
Leonardo Alt 68cfa0a901 Fix spelling in SMTChecker comment 2020-11-23 19:40:29 +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
Martin Blicha 80d743426f [SMTChecker] Added support for struct constructor. 2020-11-23 13:45:17 +01:00
Leonardo 61069ec77d Merge pull request #10355 from blishko/smtchecker-refactoring 
[SMTChecker] Small refactoring of assignments to provide a common low-level point for model checking engines to hook into.
 2020-11-20 14:31:32 -01:00
Leonardo Alt e4339b0526 [SMTChecker] Support named arguments in function calls 2020-11-20 11:52:26 -01:00
Martin Blicha fbcb572d69 [SMTChecker] Small refactoring of assignments to provide a common low-level point for model checker engines to hook into. 2020-11-19 22:03:08 +01:00
Martin Blicha 07427c798c [SMTChecker] Adding a dummy frame to the call stack for the implicit constructor 2020-11-16 22:46:17 +01:00
Martin Blicha 5ca7a24896 [SMTChecker] Added support for precise modeling of external calls to this. 
Modeling external calls to this, since we can trust these calls.

fixed problem with transaction data not being restored after trusted external call

update to the tests

additional tests

changelog entry

added tests for external getters of this
 2020-11-13 11:49:09 +01:00
Alex Beregszaszi 2f899bbffa [SMTChecker] Avoid implicit conversion 2020-11-11 16:29:03 +00:00
Leonardo 25b2a38d8b Merge pull request #10202 from ethereum/smt_fix_modifiers_branches 
[SMTChecker] Fix CHC false positives when using branches inside modifiers
 2020-11-09 16:42:30 +00:00
Leonardo Alt 00858c0ccf Isoltets SMTChecker option and BMC specific tests 2020-11-06 15:03:38 +00:00
Leonardo Alt 89dce24f24 Force SMT variable creation order 2020-11-06 11:51:01 +00:00
Leonardo Alt 646be53f2f Sort variables and expressions by AST id 2020-11-06 11:50:43 +00:00
Leonardo Alt 1dbd8f8d67 Fix CHC false positives when using branches inside modifiers 2020-11-04 21:47:07 +00:00
Leonardo 62535c2fd4 Merge pull request #10181 from ethereum/smt_user_timeout 
[SMTChecker] User timeout option
 2020-11-04 10:55:28 +00:00
Leonardo Alt daf859c15b [SMTChecker] report SMTEncoder warnings also via CHC 2020-11-03 16:06:17 +00:00
Leonardo Alt d03ddeb0fa [SMTChecker] User timeout option 2020-11-03 10:46:11 +00: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
Leonardo Alt 94e2506132 Fix inherited state vars for BMC 2020-11-02 11:42:39 +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 f2f84a7f97 Format array cex 2020-10-27 16:32:43 +00:00
Leonardo Alt 446e46fe06 Use Expression instead of plain strings for counterexamples 2020-10-27 12:04:51 +00: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
Martin Blicha ade3b9951c [SMTChecker] Added support for selector when expression's value is known at compile time 2020-10-22 14:18:52 +02: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
Leonardo a097f9f124 Merge pull request #10025 from ethereum/smt_crypto_functions 
[SMTChecker] Support crypto functions in CHC
 2020-10-16 16:40:29 +01:00
Leonardo 8d7bdcaba7 Merge pull request #10036 from ethereum/smt_cli_option 
Add CLI option to choose model checker engine
 2020-10-16 16:37:33 +01:00
Martin Blicha 78c8fbc7ce [SMTChecker] encoding division and modulo operations using slack variables 2020-10-16 16:06:31 +02:00
Leonardo Alt 4e49135318 Add CLI option to choose model checker engine 2020-10-16 15:01:47 +01:00
Leonardo Alt 54f76e081a [SMTChecker] Support crypto functions in CHC 2020-10-16 14:57:13 +01:00
Leonardo Alt 440e5b3935 [SMTChecker] Fix counterexample state reporting 2020-10-13 22:18:43 +01:00
Leonardo Alt aec456021d Add tx constraints to CHC 2020-10-13 17:49:04 +01:00
Leonardo Alt a2cdde1191 Add tx data to symbolic state 2020-10-13 17:49:04 +01:00
Leonardo Alt 1e568d7dc6 [SMTChecker] Fix implicit constructor summary predicate 2020-10-13 09:38:58 +01:00
Djordje Mijovic e23d8f5593 [SMTChecker] Supporting inline arrays. 2020-10-12 16:59:14 +02:00
Leonardo Alt 18cf01c187 Add this and state to CHC 2020-10-12 11:11:52 +01:00
Leonardo Alt a86f656704 Refactor state as tuple 2020-10-12 11:11:52 +01: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 352cce5fc8 [SMTChecker] Support addmod and mulmod. 2020-09-29 12:45:19 +02:00
Leonardo Alt fa7c9a0dc6 Simplify internal function calls 2020-09-28 15:31:15 +02:00
Leonardo Alt 3519b38055 Move predicate functions from CHC to PredicateInstance 2020-09-28 12:43:19 +02:00
Leonardo Alt ac93ee1d08 Move error flag from CHC to SymbolicState 2020-09-28 12:37:57 +02:00