cerc-io/solidity
16
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
21,300 Commits 348 Branches 121 Tags 100 MiB
408bd5fa62
Commit Graph

76 Commits

Author SHA1 Message Date
Leo Alt
49e7627bd3 Use invariants in CHC 2021-10-26 11:30:30 +02:00
Leo Alt
8e81df1bd3 Do not show redundant unsupported errors in SMTChecker 2021-08-27 16:25:09 +02:00
Leo Alt
61160aa0e7 Add constraints correlating address(this).balance and msg.value 2021-08-25 21:10:08 +02:00
Leo Alt
685d7a8c99 Bundle all unproved targets in a single message and only show all if setting chooses that 2021-08-04 13:54:50 +02:00
Leo Alt
6c8ecfa82c Add option to choose solver 2021-07-27 17:14:21 +02:00
chriseth
e3525b81d0 Supply scanner to model checker. 2021-07-14 15:12:10 +02:00
Leonardo Alt
4b2ccf2f37 Abstract function smtchecker natspec 2021-05-11 15:30:19 +02:00
Leonardo Alt
dd1865873e Choose contracts to be analyzed by the SMTChecker 2021-04-21 10:34:14 +02:00
Leonardo Alt
ba97d6ac4e Add local vars to cex 2021-03-30 17:55:21 +02:00
Leonardo Alt
dbd067d6db Report out of bounds index access 2021-03-30 10:28:48 +02:00
Mathias Baumann
e197ebbdd1 Replace TypePointer with Type const* 2021-03-23 11:47:19 +01:00
Leonardo Alt
998346e599 Fix bug in virtual functions called by constructor. 2021-03-12 16:42:28 +01:00
Leonardo
7405dc5b7f
Merge pull request #10836 from ethereum/smt_fix_cex_inheritance 
Fix inheritance bug in CHC cex
 2021-02-03 18:49:25 +01:00
Martin Blicha
f1013427a7 [SMTChecker] refactoring the accessing the encoding state 2021-02-03 15:53:58 +01:00
Leonardo Alt
665ce27c18 Fix inheritance bug in CHC cex 2021-02-02 18:06:32 +01:00
Leonardo Alt
3b23cadbdc Add CLI and JSON option to select SMTChecker targets 2021-01-20 17:35:37 +01:00
Leonardo Alt
b3c3836388 Output internal calls 2021-01-12 14:57:04 +01:00
Martin Blicha
0f3924186e [SMTChecker] Support try-catch in CHC engine 2021-01-11 13:36:02 +01:00
Leonardo Alt
11f56861c3 Refactor cex loop 2021-01-07 23:13:02 +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
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 Alt
646be53f2f Sort variables and expressions by AST id 2020-11-06 11:50:43 +00:00
Leonardo Alt
d03ddeb0fa [SMTChecker] User timeout option 2020-11-03 10:46:11 +00:00
Martin Blicha
c1a57ffbfe [SMTChecker] More precise creation of verification targets. 2020-10-30 19:11:28 +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
Martin Blicha
f0d81601db [SMTChecker] Adding division by zero checks in the CHC engine 2020-10-21 14:48:33 +02:00
Leonardo Alt
18cf01c187 Add this and state to CHC 2020-10-12 11:11:52 +01: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
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
d87e15e2cd Refactor CHC sorts 2020-09-15 16:45:50 +02:00
Leonardo Alt
23ee011c56 [SMTChecker] Fix imports 2020-09-11 13:34:46 +02:00
Leonardo Alt
a3b6019131 Move post input and post output filtering from CHC to Predicate 2020-09-01 16:10:12 +02:00
Leonardo Alt
2e2e96cc93 Move state model filtering from CHC to Predicate 2020-09-01 16:10:12 +02:00
Leonardo Alt
e3a8c94ace Move formatFunctionCallCounterexample from CHC to Predicate 2020-09-01 16:10:11 +02:00
Leonardo Alt
5bbb20d3cb Move stateVariablesIncludingInheritedAndPrivate from CHC to SMTEncoder 2020-09-01 16:09:57 +02:00
Leonardo Alt
016b9b83a8 Refactor predicates 2020-09-01 16:09:56 +02:00
Leonardo Alt
8a06041bbe [SMTChecker] Add underflow/overflow target to CHC 2020-08-14 12:58:27 +02:00
Leonardo Alt
d5f00842d9 cex2dot debug 2020-07-23 18:49:03 +02:00
Leonardo Alt
5bb4e73693 Review 1 2020-07-23 18:49:03 +02:00
Leonardo Alt
694ec92688 Generate counterexample message based on cex graph 2020-07-23 18:49:03 +02:00
Leonardo Alt
744905525f Convert z3 cex graph into STL 2020-07-23 18:49:03 +02:00
Leonardo Alt
a7a069c74a Refactor constructor exit 2020-07-23 18:49:03 +02:00
Sachin Grover
b7adb2aa42 Add SPDX license identifier if not present already in source file 
Fixes: #9220
 2020-07-17 20:24:12 +05:30
chriseth
b3566ad0d5
Merge pull request #9082 from ethereum/conversionWarnings 
Adding `-Wsign-conversion` flag and fixing errors
 2020-07-13 11:28:09 +02:00
Leonardo Alt
88030c6568 [SMTChecker] Refactor verification targets 2020-07-10 10:28:49 +02:00
Alex Beregszaszi
a0300835eb Change CHC to avoid sign mismatch 2020-07-09 17:22:52 +02:00