cerc-io/solidity
15
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
9f67d26a1a
solidity/libsolidity/formal
History
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
..
ArraySlicePredicate.cpp Support array slices 2020-10-01 11:52:02 +02:00
ArraySlicePredicate.h Support array slices 2020-10-01 11:52:02 +02:00
BMC.cpp [SMTChecker] Added support for precise modeling of external calls to this. 2020-11-13 11:49:09 +01:00
BMC.h [SMTChecker] User timeout option 2020-11-03 10:46:11 +00:00
CHC.cpp [SMTChecker] Added support for precise modeling of external calls to this. 2020-11-13 11:49:09 +01:00
CHC.h [SMTChecker] Added support for precise modeling of external calls to this. 2020-11-13 11:49:09 +01:00
EncodingContext.cpp [SMTChecker] More precise creation of verification targets. 2020-10-30 19:11:28 +01:00
EncodingContext.h [SMTChecker] Avoid implicit conversion 2020-11-11 16:29:03 +00:00
ModelChecker.cpp [SMTChecker] User timeout option 2020-11-03 10:46:11 +00:00
ModelChecker.h [SMTChecker] User timeout option 2020-11-03 10:46:11 +00:00
Predicate.cpp [SMTChecker] Avoid implicit conversion 2020-11-11 16:29:03 +00:00
Predicate.h Format array cex 2020-10-27 16:32:43 +00:00
PredicateInstance.cpp Fix CHC false positives when using branches inside modifiers 2020-11-04 21:47:07 +00:00
PredicateInstance.h Add this and state to CHC 2020-10-12 11:11:52 +01:00
PredicateSort.cpp Fix CHC false positives when using branches inside modifiers 2020-11-04 21:47:07 +00:00
PredicateSort.h [SMTChecker] Support crypto functions in CHC 2020-10-16 14:57:13 +01:00
SMTEncoder.cpp [SMTChecker] Added support for precise modeling of external calls to this. 2020-11-13 11:49:09 +01:00
SMTEncoder.h [SMTChecker] Added support for precise modeling of external calls to this. 2020-11-13 11:49:09 +01:00
SSAVariable.cpp Add SPDX license identifier if not present already in source file 2020-07-17 20:24:12 +05:30
SSAVariable.h Add SPDX license identifier if not present already in source file 2020-07-17 20:24:12 +05:30
SymbolicState.cpp [SMTChecker] Avoid implicit conversion 2020-11-11 16:29:03 +00:00
SymbolicState.h [SMTChecker] Support crypto functions in CHC 2020-10-16 14:57:13 +01:00
SymbolicTypes.cpp Add tx data to symbolic state 2020-10-13 17:49:04 +01:00
SymbolicTypes.h Add tx data to symbolic state 2020-10-13 17:49:04 +01:00
SymbolicVariables.cpp [SMTChecker] Fix internal error when array.push() is used as LHS of assignment 2020-11-02 13:32:53 +00:00
SymbolicVariables.h [SMTChecker] Fix internal error when array.push() is used as LHS of assignment 2020-11-02 13:32:53 +00:00
VariableUsage.cpp [SMTChecker] Fix ICE in BMC function inlining 2020-08-05 11:47:25 +02:00
VariableUsage.h [SMTChecker] Fix ICE in BMC function inlining 2020-08-05 11:47:25 +02:00