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
20,707 Commits 348 Branches 121 Tags
fuzzYulEVMCodeTransformStep4
Commit Graph
648 Commits
Author SHA1 Message Date
Martin Blicha 27402781c4 [SMTChecker] Fixed crash on push to bytes on lhs of an assignment 2020-12-14 17:40:45 +01:00
Martin Blicha 0be325dc0d [SMTChecker] Fix handling of function calls where the function identifier is nested in a tuple. 2020-12-14 16:19:24 +01:00
chriseth 561280a5cc Merge remote-tracking branch 'origin/develop' into breaking 2020-12-14 11:33:40 +01:00
Martin Blicha 8927015e5a [SMTChecker] Adding unary increment and decrement as under/overflow verification targets for the CHC engine 2020-12-11 17:41:50 +01:00
Alex Beregszaszi bd641a5206 Enable more C++ compiler warnings 2020-12-10 21:03:58 +00:00
Daniel Kirchner c400c61fc3 Fix incorrect behaviour on clang 6. 2020-12-10 17:20:30 +01:00
chriseth d0551b67d7 Merge remote-tracking branch 'origin/develop' into breaking 2020-12-10 17:07:56 +01:00
Daniel Kirchner 7308abc084 Allow loading Z3 dynamically at runtime. 2020-12-10 16:47:47 +01:00
chriseth 482bda6887 Merge remote-tracking branch 'origin/develop' into breaking 2020-12-10 12:15:52 +01:00
Leonardo Alt 3c142e0e94 Move CHC counterexamples to primary location 2020-12-09 19:55:18 +01:00
Leonardo Alt a961a76263 Do not run SMTChecker when file level functions/constants are present. 2020-12-09 12:18:55 +01:00
chriseth 806453aca9 Merge remote-tracking branch 'origin/develop' into breaking 2020-12-08 21:00:09 +01:00
chriseth b045195c1e Merge remote-tracking branch 'origin/develop' into breaking 2020-12-08 17:42:31 +01:00
Martin Blicha eb356735f6 [SMTChecker] Adding support for reporting values of structs in CEX in CHC engine. 2020-12-08 16:40:28 +01:00
Martin Blicha 0ebab439be removing assert that is not always true 2020-12-08 12:27:59 +01:00
Martin Blicha ff0c794674 [SMTChecker] Fixing conversion from StringLiteral to FixedBytes 2020-12-07 19:30:51 +01:00
Leonardo Alt b7ac207391 [SMTChecker] Support return in CHC 2020-12-07 18:17:33 +01:00
chriseth bff7254d9e Fix merge conflict. 2020-12-07 13:30:09 +01:00
chriseth 329b8f2a60 Merge remote-tracking branch 'origin/develop' into breaking 2020-12-07 13:04:14 +01:00
Leonardo Alt 7490ffbe13 Use nonlinear clauses instead of inlining for base constructors 2020-12-04 13:25:56 +01:00
chriseth d56a7bb89e Merge pull request #10489 from ethereum/develop 
Merge develop into breaking.
 2020-12-03 18:11:12 +01:00
Leonardo 088b694f0b Merge pull request #10207 from ethereum/smt_tests_asserts 
[SMTChecker] Add uncovered test and replace uncovered tests by asserts
 2020-12-03 08:59:48 +01:00
Martin Blicha 2ee633f404 [SMTChecker] Added support for public getters through this. 2020-12-02 16:06:48 +01:00
chriseth 6de7eaba95 Merge remote-tracking branch 'origin/develop' into breaking 2020-12-01 10:50:13 +01:00
Leonardo Alt fa561dbd0e Add uncovered test and replace uncovered tests by asserts 2020-11-30 18:46:47 +01:00
Martin Blicha cd06d68cbe [SMTChecker] Keeping better track of path condition through branches with return statement in the BMC engine. 2020-11-30 11:47:49 +01:00
chriseth 18de8a56c9 Merge remote-tracking branch 'origin/develop' into breaking 2020-11-26 11:48:53 +01:00
Djordje Mijovic 26c43cfc66 [SMTChecker] Fix SMT logic error when doing compound assignment with string literlas. 2020-11-24 19:14:15 +01:00
chriseth 253889cbf1 Merge remote-tracking branch 'origin/develop' into breaking 2020-11-24 16:22:03 +01:00
Leonardo Alt 68cfa0a901 Fix spelling in SMTChecker comment 2020-11-23 19:40:29 +01:00
chriseth a0a02f2307 Merge remote-tracking branch 'origin/develop' into breaking 2020-11-23 19:28:08 +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
chriseth e8a278eefa Merge remote-tracking branch 'origin/develop' into breaking 2020-11-17 18:51:57 +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
chriseth 14ed67ac4b Merge remote-tracking branch 'origin/develop' into breaking 2020-11-11 20:33:40 +01:00
Alex Beregszaszi 2f899bbffa [SMTChecker] Avoid implicit conversion 2020-11-11 16:29:03 +00:00
chriseth da92fe548e Merge remote-tracking branch 'origin/develop' into breaking 2020-11-10 13:48:32 +01: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
chriseth 04195439b7 Merge remote-tracking branch 'origin/develop' into HEAD 2020-11-09 14:28:05 +01: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