diff options
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 14 | ||||
| -rw-r--r-- | libsolidity/formal/SMTChecker.h | 4 |
2 files changed, 8 insertions, 10 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index be968173..773fc332 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -98,7 +98,7 @@ void SMTChecker::endVisit(FunctionDefinition const&) // TOOD we could check for "reachability", i.e. satisfiability here. // We only handle local variables, so we clear at the beginning of the function. // If we add storage variables, those should be cleared differently. - clearLocalVariables(); + removeLocalVariables(); m_currentFunction = nullptr; } @@ -729,9 +729,8 @@ void SMTChecker::resetStateVariables() { for (auto const& variable: m_variables) { - VariableDeclaration const* _decl = dynamic_cast<VariableDeclaration const*>(variable.first); - solAssert(_decl, ""); - if (_decl->isStateVariable()) + VariableDeclaration const& _decl = dynamic_cast<VariableDeclaration const&>(*variable.first); + if (_decl.isStateVariable()) { newValue(*variable.first); setUnknownValue(*variable.first); @@ -895,13 +894,12 @@ void SMTChecker::addPathImpliedExpression(smt::Expression const& _e) m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), _e)); } -void SMTChecker::clearLocalVariables() +void SMTChecker::removeLocalVariables() { for (auto it = m_variables.begin(); it != m_variables.end(); ) { - VariableDeclaration const* _decl = dynamic_cast<VariableDeclaration const*>(it->first); - solAssert(_decl, ""); - if (_decl->isLocalVariable()) + VariableDeclaration const& _decl = dynamic_cast<VariableDeclaration const&>(*it->first); + if (_decl.isLocalVariable()) it = m_variables.erase(it); else ++it; diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index b5c5cfd7..b7d0f6a8 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -161,8 +161,8 @@ private: /// Add to the solver: the given expression implied by the current path conditions void addPathImpliedExpression(smt::Expression const& _e); - /// Clears the local variables of a function. - void clearLocalVariables(); + /// Removes the local variables of a function. + void removeLocalVariables(); std::shared_ptr<smt::SolverInterface> m_interface; std::shared_ptr<VariableUsage> m_variableUsage; |