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
19,280 Commits 348 Branches 121 Tags 100 MiB
2c92f7641b
Commit Graph

109 Commits

Author SHA1 Message Date
Leonardo Alt
007d39871b [SMTChecker] Synthesize untrusted functions called externally 2021-01-15 11:56:26 +01:00
Martin Blicha
7c6340fe4f [SMTChecker] Refactoring expression to tuple assignment 2021-01-12 17:15:14 +01:00
Leonardo Alt
b3c3836388 Output internal calls 2021-01-12 14:57:04 +01:00
Leonardo Alt
f1ae24abc7 Remove extra line breaks 2021-01-12 14:00:07 +01:00
Martin Blicha
ff76c989ac addressing review comments 2021-01-11 14:19:06 +01:00
Martin Blicha
dd43ce1578 fixing try/catch encoding for BMC, refactoring 2021-01-11 13:36:03 +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
78d55e6b4a [SMTChecker] Support check/unchecked 2020-12-30 12:14:30 +01:00
Leonardo Alt
9482e7de23 [SMTChecker] Fix calls to virtual/overriden functions 2020-12-29 11:25:20 +01:00
Martin Blicha
bb0003f5ea removed extra parameter from PredicateInstance::nondetInterface 2020-12-28 19:48:48 +01:00
Martin Blicha
f76ff35225 [SMTChecker] Detect errors caused by reentrancy 2020-12-28 14:32:53 +01:00
Martin Blicha
d90b9da4f0 [SMTChecker] Refactoring 2020-12-22 13:10:48 +01:00
Martin Blicha
7078e8f8f8 [SMTChecker] Fix analysis of overriding modifiers 2020-12-17 17:05:54 +01:00
Leonardo Alt
2cbf33ca1c SMTChecker support ABI functions as UFs 2020-12-17 14:03:17 +01:00
Daniel Kirchner
c400c61fc3 Fix incorrect behaviour on clang 6. 2020-12-10 17:20:30 +01:00
Daniel Kirchner
7308abc084 Allow loading Z3 dynamically at runtime. 2020-12-10 16:47:47 +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
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
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
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
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
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
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
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
Leonardo Alt
aec456021d Add tx constraints to CHC 2020-10-13 17:49:04 +01: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
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
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
00f6b303b1 [SMTChecker] Change warning message 2020-09-09 16:14:21 +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