cerc-io/solidity
10
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

Review comments

Browse Source
This commit is contained in:
Leonardo Alt 2018-06-06 12:11:58 +02:00
parent 678a769cd7
commit 48652c88af
2 changed files with 8 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
libsolidity/formal/SMTChecker.cpp
View File

@ -98,7 +98,7 @@ void SMTChecker::endVisit(FunctionDefinition const&)
// TOOD we could check for "reachability", i.e. satisfiability here. // TOOD we could check for "reachability", i.e. satisfiability here.
// We only handle local variables, so we clear at the beginning of the function. // We only handle local variables, so we clear at the beginning of the function.
// If we add storage variables, those should be cleared differently. // If we add storage variables, those should be cleared differently.
clearLocalVariables(); removeLocalVariables();
m_currentFunction = nullptr; m_currentFunction = nullptr;
} }
@ -729,9 +729,8 @@ void SMTChecker::resetStateVariables()
{ {
for (auto const& variable: m_variables) for (auto const& variable: m_variables)
{ {
VariableDeclaration const* _decl = dynamic_cast<VariableDeclaration const*>(variable.first); VariableDeclaration const& _decl = dynamic_cast<VariableDeclaration const&>(*variable.first);
solAssert(_decl, ""); if (_decl.isStateVariable())
if (_decl->isStateVariable())
{ {
newValue(*variable.first); newValue(*variable.first);
setUnknownValue(*variable.first); setUnknownValue(*variable.first);
@ -895,13 +894,12 @@ void SMTChecker::addPathImpliedExpression(smt::Expression const& _e)
m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), _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(); ) for (auto it = m_variables.begin(); it != m_variables.end(); )
{ {
VariableDeclaration const* _decl = dynamic_cast<VariableDeclaration const*>(it->first); VariableDeclaration const& _decl = dynamic_cast<VariableDeclaration const&>(*it->first);
solAssert(_decl, ""); if (_decl.isLocalVariable())
if (_decl->isLocalVariable())
it = m_variables.erase(it); it = m_variables.erase(it);
else else
++it; ++it;

4
libsolidity/formal/SMTChecker.h
View File

@ -161,8 +161,8 @@ private:
/// Add to the solver: the given expression implied by the current path conditions /// Add to the solver: the given expression implied by the current path conditions
void addPathImpliedExpression(smt::Expression const& _e); void addPathImpliedExpression(smt::Expression const& _e);
/// Clears the local variables of a function. /// Removes the local variables of a function.
void clearLocalVariables(); void removeLocalVariables();
std::shared_ptr<smt::SolverInterface> m_interface; std::shared_ptr<smt::SolverInterface> m_interface;
std::shared_ptr<VariableUsage> m_variableUsage; std::shared_ptr<VariableUsage> m_variableUsage;