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
19,112 Commits 348 Branches 121 Tags
8649df169dce5fb8f7dc814dd532c428ada4be7f
Commit Graph
66 Commits
Author SHA1 Message Date
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
Daniel Kirchner 7308abc084 Allow loading Z3 dynamically at runtime. 2020-12-10 16:47:47 +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 7490ffbe13 Use nonlinear clauses instead of inlining for base constructors 2020-12-04 13:25:56 +01:00
Martin Blicha 2ee633f404 [SMTChecker] Added support for public getters through this. 2020-12-02 16:06:48 +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
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 Alt 00858c0ccf Isoltets SMTChecker option and BMC specific tests 2020-11-06 15:03:38 +00:00
Leonardo Alt d03ddeb0fa [SMTChecker] User timeout option 2020-11-03 10:46:11 +00:00
Martin Blicha f0d81601db [SMTChecker] Adding division by zero checks in the CHC engine 2020-10-21 14:48:33 +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 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 a2cdde1191 Add tx data to symbolic state 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 352cce5fc8 [SMTChecker] Support addmod and mulmod. 2020-09-29 12:45:19 +02:00
Leonardo Alt e6bd18525b [SMTChecker] Add engine prefix to verification target error messages 2020-09-25 19:09:06 +02:00
Leonardo Alt 00f6b303b1 [SMTChecker] Change warning message 2020-09-09 16:14:21 +02:00
Leonardo Alt 7b3cd019d4 Make recursive structs unsupported 2020-09-03 15:19:33 +02:00
Đorđe Mijović 4dd25f7302 Merge pull request #9639 from ethereum/smtConditionalSupport 
[SMTChecker] Supporting conditional operator
 2020-08-21 14:25:47 +02:00
Djordje Mijovic 3f97a1012a [SMTChecker] Supporting conditional operator 2020-08-20 21:39:35 +02:00
chriseth 4dc63875f9 Merge pull request #9113 from ethereum/smt_chc_overflow 
[SMTChecker] Add underflow/overflow target to CHC
 2020-08-20 13:17:00 +02:00
Leonardo Alt 8a06041bbe [SMTChecker] Add underflow/overflow target to CHC 2020-08-14 12:58:27 +02:00
Jason Cobb 888d7037cd Make FunctionCallAnnotation::kind a SetOnce 2020-08-12 11:57:01 -04:00
Leonardo Alt 8df8c6e14f [SMTChecker] Fix ICE in BMC function inlining 2020-08-05 11:47:25 +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
Leonardo Alt 88030c6568 [SMTChecker] Refactor verification targets 2020-07-10 10:28:49 +02:00
Leonardo Alt e5d25692a5 [SMTChecker] Fix BMC targets with FP 2020-05-29 18:13:13 +02:00
Leonardo Alt 45eba27424 Rename namespace 2020-05-20 12:55:18 +02:00
Leonardo Alt 087605ea02 Create libsmtutil 2020-05-20 12:55:18 +02:00
a3d4 7cae074b8a Add error IDs to BMC 2020-05-12 11:39:18 +02:00
a3d4 8f68c04358 Add unique IDs to error reporting calls 2020-05-06 13:53:46 +02:00
Leonardo Alt 83c9e82099 Fix ICE with fixed point 2020-04-22 19:57:00 +02:00
Leonardo Alt 05a85461fe Symbolic state 2020-04-06 12:27:53 +02:00
Leonardo Alt 07368c2e1e Add support to internal function calls 2020-03-11 16:29:07 +01:00
Leonardo Alt 34d64761d9 Extract symbolicArguments function 2020-02-12 11:47:58 -03:00
Leonardo Alt 6451a4d2a0 Move VerificationTarget and add BMCVerificationTarget 2020-02-12 11:47:58 -03:00
Christian Parpart 6b23412fae C++ namespace cleanup (except tests). 2020-01-07 15:51:50 +01:00
Leonardo Alt f4f83690f3 Replace some shared_ptr by unique_ptr or raw pointers 2020-01-06 14:16:49 +01:00
chriseth e061f1e743 Merge remote-tracking branch 'origin/develop' into HEAD 2019-12-05 16:44:26 +01:00
Leonardo Alt 48c3a5c225 [SMTChecker] Create options to choose SMT solver in runtime 2019-12-04 17:31:44 +01:00
chriseth 96d777d7f1 Merge commit 'a7d481fb9' into develop_060 2019-12-03 20:47:30 +01:00
Leonardo Alt a352abe00d [SMTChecker] Add support to constructors 2019-11-28 14:43:23 +01:00
Leonardo Alt ddc478e3e4 Add CallbackKind and use it for the SMT solver 2019-11-21 22:10:21 +00:00
Leonardo Alt 8efacfb545 [SMTChecker] Fix ICE in string literal to fixed bytes implicit conversion 2019-11-13 22:25:18 +01:00
Leonardo Alt 10e70b8603 [SMTChecker] Support inheritance and resolve overrides 2019-11-06 11:00:06 +01:00
Leonardo Alt 4214cd1354 [SMTChecker] Fix ICE when reporting cex concerning state vars from different source files 2019-08-10 20:56:52 +02:00
Leonardo 67c855e93e Merge pull request #7170 from ethereum/smt_fix_other_contract_state_var 
[SMTChecker] Fix ICE when inlining functions from different source
 2019-08-09 19:14:28 +02:00
Leonardo Alt 7b22496b1f [SMTChecker] Fix ICE when inlining functions that use state vars and are in a different source 2019-08-09 17:50:52 +02:00