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,405 Commits 348 Branches 121 Tags
consteval-arith
Commit Graph
286 Commits
Author SHA1 Message Date
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
Leonardo Alt 47b268d509 Update tests 2020-10-13 17:49:04 +01:00
Leonardo Alt aec456021d Add tx constraints to CHC 2020-10-13 17:49:04 +01:00
Mathias Baumann 32b4f18023 Print warning for unnamed return parameters and no return statement 2020-10-13 13:11:29 +02:00
Djordje Mijovic e23d8f5593 [SMTChecker] Supporting inline arrays. 2020-10-12 16:59:14 +02:00
Leonardo Alt 3d2e6252f0 Add/update tests 2020-10-12 11:11:52 +01:00
Leonardo Alt 18cf01c187 Add this and state to CHC 2020-10-12 11:11:52 +01:00
a3d4 f29ebc0847 Fix shadowing/same-name warnings for later declarations 2020-10-08 20:22:04 +02: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
Mathias Baumann 4c02cd2310 Add name for split-test to prevent failure in other places 2020-09-30 16:56:53 +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 e6bd18525b [SMTChecker] Add engine prefix to verification target error messages 2020-09-25 19:09:06 +02:00
Leonardo Alt 0223571987 [SMTChecker] Do not report error when rlimit 2020-09-25 18:43:10 +02:00
Alex Beregszaszi 9f3d5d3e2f [SMTChecker] Implement support for memory allocation 2020-09-25 15:56:24 +01:00
Alex Beregszaszi 9c1b041dcb [SMTChecker] Keep constraints of string literals after assignment 2020-09-25 11:32:48 +01:00
Alex Beregszaszi 5090353a1a [SMTChecker] Keep knowledge about string literals 2020-09-25 11:32:23 +01:00
Leonardo 57e1b2cb92 Merge pull request #9881 from ethereum/smt_fixed_bytes_index_access 
[SMTChecker] Support fixed bytes index access
 2020-09-25 11:32:56 +02:00
Leonardo Alt df8c6d94e3 [SMTChecker] Support fixed bytes index access 2020-09-25 09:59:38 +02:00
Alex Beregszaszi 6edfdff187 [SMTChecker] Do not warn on "abi" as an identifer 
There is an approprate warning for the function call.
 2020-09-24 13:57:42 +01:00
chriseth a9f9b4db27 Merge pull request #9872 from ethereum/smt_remove_tests 
Extract boost smt and remove unused tests
 2020-09-24 13:20:19 +02:00
Leonardo Alt ebb6f61506 [SMTChecker] Decrease rlimit 2020-09-23 19:28:47 +02:00
Leonardo Alt 8eba66daf9 Extract boost smt and remove unused tests 2020-09-23 17:55:55 +02:00
Đorđe Mijović 858b4507e2 Merge pull request #9854 from ethereum/bitwiseSmt 
[SMTChecker] Support compound shifts and bitwise and, or, and xor
 2020-09-23 12:35:48 +02:00
Djordje Mijovic 96bafb9ba3 [SMTChecker] Updating old and adding new tests for compound shift operators. 2020-09-23 11:31:37 +02:00
Djordje Mijovic 0193952106 [SMTChecker] Updating old and adding new tests for compound bitwise xor operator. 2020-09-23 11:31:37 +02:00