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,823 Commits 348 Branches 121 Tags
develop_7
Commit Graph
312 Commits
Author SHA1 Message Date
Leonardo Alt 80e85b772b [SMTChecker] Apply const eval to arithmetic binary expressions 2020-12-16 14:58:00 +01:00
Martin Blicha e2c27b8ea4 [SMTChecker] Fix internal error on constructor of a recursive struct 2020-12-15 09:53:52 +01:00
Martin Blicha 71f835b71b [SMTChecker] Fixed internal error when increment/decrement is applied on a result of push(). 2020-12-14 22:52:44 +01:00
Martin Blicha 103fa3b7eb [SMTChecker] Fix internal error on abstract modifier 2020-12-14 18:23:25 +01:00
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
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
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
Martin Blicha de34fe8aa3 [SMTChecker] Adding test witnessing that SMTChecker no longer crashes when producing CEX with arrays 2020-12-09 09:13:39 +01:00
Martin Blicha 12aa654bad added test 2020-12-08 13:05:16 +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
Leonardo Alt 7490ffbe13 Use nonlinear clauses instead of inlining for base constructors 2020-12-04 13:25:56 +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
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
Djordje Mijovic 26c43cfc66 [SMTChecker] Fix SMT logic error when doing compound assignment with string literlas. 2020-11-24 19:14:15 +01:00
chriseth 79669ecd48 Use new abicoder pragma. 2020-11-24 14:57:45 +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 Alt e4339b0526 [SMTChecker] Support named arguments in function calls 2020-11-20 11:52:26 -01:00
chriseth bb97363abf Merge pull request #9989 from ethereum/issue-9947 
Natspec: Fix internal error when different return name was inherited
 2020-11-17 13:54:03 +01:00
Mathias Baumann 559b27aaad Natspec: Fix internal error when different return name was inherited 2020-11-17 11:56:32 +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
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 1dbd8f8d67 Fix CHC false positives when using branches inside modifiers 2020-11-04 21:47:07 +00:00
Leonardo Alt daf859c15b [SMTChecker] report SMTEncoder warnings also via CHC 2020-11-03 16:06:17 +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 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
Martin Blicha 8c351278ac [SMTChecker] added test to check correct handling of the sign of the modulo operation 2020-10-16 16:17:32 +02:00
Martin Blicha 78c8fbc7ce [SMTChecker] encoding division and modulo operations using slack variables 2020-10-16 16:06:31 +02:00
Leonardo Alt 54f76e081a [SMTChecker] Support crypto functions in CHC 2020-10-16 14:57:13 +01:00
Leonardo Alt 88f783bb1e Remove more tests because current Spacer crashes 2020-10-13 19:27:49 +01:00
Leonardo Alt b9b9c229b4 New tests 2020-10-13 17:49:04 +01:00