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
22,312 Commits 348 Branches 121 Tags
customKnowledgeBase
Commit Graph
690 Commits
Author SHA1 Message Date
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
chriseth 20f39ab6e9 Merge pull request #10097 from ethereum/develop 
Merge develop into breaking.
 2020-10-23 10:30:24 +02:00
chriseth bfc8e26007 Remove low-level log functions. 2020-10-22 17:50:14 +02: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
chriseth 6979952995 Merge remote-tracking branch 'origin/develop' into HEAD 2020-10-19 18:02:50 +02: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
chriseth 979d3062bc Merge pull request #10033 from ethereum/develop 
Merge develop into breaking
 2020-10-14 14:12:20 +02: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
chriseth f6e57a0eec Merge pull request #10023 from ethereum/develop 
Merge develop into breaking.
 2020-10-13 18:18:53 +02:00
Mathias Baumann 006e5f2e1f Allow path syntax for super constructor calls 2020-10-13 14:32:11 +02: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
Leonardo Alt e6bd18525b [SMTChecker] Add engine prefix to verification target error messages 2020-09-25 19:09:06 +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
Đ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 79f550dba9 [SMTChecker] Supporting compound shift operators. 2020-09-23 11:31:37 +02:00
Djordje Mijovic 773e000227 [SMTChecker] Implementing compound bitwise And/Or/Xor operators 2020-09-23 11:31:37 +02:00
Alex Beregszaszi 709d25bd3d [SMTChecker] Support address type conversion with literals 2020-09-22 18:49:11 +01:00
chriseth 6e2d2feb10 Small fixes wrt ReasoningBasedSimplifier. 2020-09-16 18:08:54 +02:00
Alex Beregszaszi c8c17b693b [SMTChecker] Support events and low-level logs 2020-09-16 11:50:39 +02:00
chriseth adccc0608d Merge pull request #9736 from ethereum/yul_smt 
Reasoning based optimizer using integers only
 2020-09-15 18:45:55 +02:00
Leonardo Alt d87e15e2cd Refactor CHC sorts 2020-09-15 16:45:50 +02:00
chriseth f73fb726af Reasoning based optimizer. 2020-09-15 15:57:58 +02:00