diff options
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 26 | ||||
| -rw-r--r-- | libsolidity/formal/SMTChecker.h | 4 |
2 files changed, 16 insertions, 14 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 6c4662ac..1050621e 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -592,21 +592,17 @@ smt::CheckResult SMTChecker::checkSatisifable() void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function) { for (auto const& variable: _function.localVariables()) - { - createVariable(*variable); - setZeroValue(*variable); - } + if (createVariable(*variable)) + setZeroValue(*variable); + for (auto const& param: _function.parameters()) - { - createVariable(*param); - setUnknownValue(*param); - } + if (createVariable(*param)) + setUnknownValue(*param); + if (_function.returnParameterList()) for (auto const& retParam: _function.returnParameters()) - { - createVariable(*retParam); - setZeroValue(*retParam); - } + if (createVariable(*retParam)) + setZeroValue(*retParam); } 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())) { @@ -628,12 +624,16 @@ void SMTChecker::createVariable(VariableDeclaration const& _varDecl) m_currentSequenceCounter[&_varDecl] = 0; m_nextFreeSequenceCounter[&_varDecl] = 1; m_variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int)); + return true; } else + { m_errorReporter.warning( _varDecl.location(), "Assertion checker does not yet support the type of this variable." ); + return false; + } } string SMTChecker::uniqueSymbol(Declaration const& _decl) diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 54e3b22a..8e07d74d 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -96,7 +96,9 @@ private: void initializeLocalVariables(FunctionDefinition const& _function); 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(Expression const& _expr); |