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

Fix problem with non-value-typed variables.

Browse Source
This commit is contained in:
chriseth 2017-10-05 19:31:17 +02:00 committed by Alex Beregszaszi
parent 19d5c42429
commit 8538a25f8d
2 changed files with 16 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
libsolidity/formal/SMTChecker.cpp
View File

@ -592,22 +592,18 @@ smt::CheckResult SMTChecker::checkSatisifable()
void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function) void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function)
{ {
for (auto const& variable: _function.localVariables()) for (auto const& variable: _function.localVariables())
{ if (createVariable(*variable))
createVariable(*variable);
setZeroValue(*variable); setZeroValue(*variable);
}
for (auto const& param: _function.parameters()) for (auto const& param: _function.parameters())
{ if (createVariable(*param))
createVariable(*param);
setUnknownValue(*param); setUnknownValue(*param);
}
if (_function.returnParameterList()) if (_function.returnParameterList())
for (auto const& retParam: _function.returnParameters()) for (auto const& retParam: _function.returnParameters())
{ if (createVariable(*retParam))
createVariable(*retParam);
setZeroValue(*retParam); setZeroValue(*retParam);
} }
}
void SMTChecker::resetVariables(vector<Declaration const*> _variables) void SMTChecker::resetVariables(vector<Declaration const*> _variables)
{ {
@ -618,7 +614,7 @@ void SMTChecker::resetVariables(vector<Declaration const*> _variables)
} }
} }
void SMTChecker::createVariable(VariableDeclaration const& _varDecl) bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
{ {
if (dynamic_cast<IntegerType const*>(_varDecl.type().get())) if (dynamic_cast<IntegerType const*>(_varDecl.type().get()))
{ {
@ -628,12 +624,16 @@ void SMTChecker::createVariable(VariableDeclaration const& _varDecl)
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));
return true;
} }
else else
{
m_errorReporter.warning( m_errorReporter.warning(
_varDecl.location(), _varDecl.location(),
"Assertion checker does not yet support the type of this variable." "Assertion checker does not yet support the type of this variable."
); );
return false;
}
} }
string SMTChecker::uniqueSymbol(Declaration const& _decl) string SMTChecker::uniqueSymbol(Declaration const& _decl)

4
libsolidity/formal/SMTChecker.h
View File

@ -96,7 +96,9 @@ private:
void initializeLocalVariables(FunctionDefinition const& _function); void initializeLocalVariables(FunctionDefinition const& _function);
void resetVariables(std::vector<Declaration const*> _variables); void resetVariables(std::vector<Declaration const*> _variables);
void createVariable(VariableDeclaration const& _varDecl); /// Tries to create an uninitialized variable and returns true on success.
/// This fails if the type is not supported.
bool createVariable(VariableDeclaration const& _varDecl);
static std::string uniqueSymbol(Declaration const& _decl); static std::string uniqueSymbol(Declaration const& _decl);
static std::string uniqueSymbol(Expression const& _expr); static std::string uniqueSymbol(Expression const& _expr);