diff options
Diffstat (limited to 'libsolidity/formal/SMTChecker.cpp')
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 36 |
1 files changed, 25 insertions, 11 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 38715289..500b610f 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -418,6 +418,10 @@ void SMTChecker::endVisit(FunctionCall const& _funCall) case FunctionType::Kind::Internal: inlineFunctionCall(_funCall); break; + case FunctionType::Kind::External: + resetStateVariables(); + resetStorageReferences(); + break; case FunctionType::Kind::KECCAK256: case FunctionType::Kind::ECRecover: case FunctionType::Kind::SHA256: @@ -1194,25 +1198,35 @@ void SMTChecker::removeLocalVariables() } } +void SMTChecker::resetVariable(VariableDeclaration const& _variable) +{ + newValue(_variable); + setUnknownValue(_variable); +} + void SMTChecker::resetStateVariables() { - for (auto const& variable: m_variables) - { - if (variable.first->isStateVariable()) - { - newValue(*variable.first); - setUnknownValue(*variable.first); - } - } + resetVariables([&](VariableDeclaration const& _variable) { return _variable.isStateVariable(); }); +} + +void SMTChecker::resetStorageReferences() +{ + resetVariables([&](VariableDeclaration const& _variable) { return _variable.hasReferenceOrMappingType(); }); } void SMTChecker::resetVariables(vector<VariableDeclaration const*> _variables) { for (auto const* decl: _variables) + resetVariable(*decl); +} + +void SMTChecker::resetVariables(function<bool(VariableDeclaration const&)> const& _filter) +{ + for_each(begin(m_variables), end(m_variables), [&](auto _variable) { - newValue(*decl); - setUnknownValue(*decl); - } + if (_filter(*_variable.first)) + this->resetVariable(*_variable.first); + }); } void SMTChecker::mergeVariables(vector<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse) |