solidity/libsolidity/formal
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
ArraySlicePredicate.h
BMC.cpp [SMTChecker] Added support for precise modeling of external calls to this. 2020-11-13 11:49:09 +01:00
BMC.h
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
EncodingContext.h
ModelChecker.cpp
ModelChecker.h
Predicate.cpp
Predicate.h
PredicateInstance.cpp
PredicateInstance.h
PredicateSort.cpp
PredicateSort.h
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
SSAVariable.h
SymbolicState.cpp
SymbolicState.h
SymbolicTypes.cpp
SymbolicTypes.h
SymbolicVariables.cpp
SymbolicVariables.h
VariableUsage.cpp
VariableUsage.h