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

Rename variables in SMT checker.

Browse Source
This commit is contained in:
chriseth 2017-09-28 11:29:04 +02:00 committed by Alex Beregszaszi
parent 846b43479d
commit 1f97c1ea8f
2 changed files with 11 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
libsolidity/formal/SMTChecker.cpp
View File

@ -494,10 +494,10 @@ void SMTChecker::createVariable(VariableDeclaration const& _varDecl, bool _setTo
{ {
solAssert(m_currentSequenceCounter.count(&_varDecl) == 0, ""); solAssert(m_currentSequenceCounter.count(&_varDecl) == 0, "");
solAssert(m_nextFreeSequenceCounter.count(&_varDecl) == 0, ""); solAssert(m_nextFreeSequenceCounter.count(&_varDecl) == 0, "");
solAssert(m_Variables.count(&_varDecl) == 0, ""); solAssert(m_variables.count(&_varDecl) == 0, "");
m_currentSequenceCounter[&_varDecl] = 0; m_currentSequenceCounter[&_varDecl] = 0;
m_nextFreeSequenceCounter[&_varDecl] = 1; m_nextFreeSequenceCounter[&_varDecl] = 1;
m_Variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int)); m_variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int));
setValue(_varDecl, _setToZero); setValue(_varDecl, _setToZero);
} }
else else
@ -566,7 +566,7 @@ smt::Expression SMTChecker::maxValue(IntegerType const& _t)
smt::Expression SMTChecker::expr(Expression const& _e) smt::Expression SMTChecker::expr(Expression const& _e)
{ {
if (!m_Expressions.count(&_e)) if (!m_expressions.count(&_e))
{ {
solAssert(_e.annotation().type, ""); solAssert(_e.annotation().type, "");
switch (_e.annotation().type->category()) switch (_e.annotation().type->category())
@ -575,24 +575,24 @@ smt::Expression SMTChecker::expr(Expression const& _e)
{ {
if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(_e.annotation().type.get())) if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(_e.annotation().type.get()))
solAssert(!rational->isFractional(), ""); solAssert(!rational->isFractional(), "");
m_Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
break; break;
} }
case Type::Category::Integer: case Type::Category::Integer:
m_Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
break; break;
case Type::Category::Bool: case Type::Category::Bool:
m_Expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e))); m_expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e)));
break; break;
default: default:
solAssert(false, "Type not implemented."); solAssert(false, "Type not implemented.");
} }
} }
return m_Expressions.at(&_e); return m_expressions.at(&_e);
} }
smt::Expression SMTChecker::var(Declaration const& _decl) smt::Expression SMTChecker::var(Declaration const& _decl)
{ {
solAssert(m_Variables.count(&_decl), ""); solAssert(m_variables.count(&_decl), "");
return m_Variables.at(&_decl); return m_variables.at(&_decl);
} }

4
libsolidity/formal/SMTChecker.h
View File

@ -103,8 +103,8 @@ private:
std::shared_ptr<smt::SolverInterface> m_interface; std::shared_ptr<smt::SolverInterface> m_interface;
std::map<Declaration const*, int> m_currentSequenceCounter; std::map<Declaration const*, int> m_currentSequenceCounter;
std::map<Declaration const*, int> m_nextFreeSequenceCounter; std::map<Declaration const*, int> m_nextFreeSequenceCounter;
std::map<Expression const*, smt::Expression> m_Expressions; std::map<Expression const*, smt::Expression> m_expressions;
std::map<Declaration const*, smt::Expression> m_Variables; std::map<Declaration const*, smt::Expression> m_variables;
ErrorReporter& m_errorReporter; ErrorReporter& m_errorReporter;
FunctionDefinition const* m_currentFunction = nullptr; FunctionDefinition const* m_currentFunction = nullptr;