From 467c34999f168c97256c86921ab8708499c1c00a Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 20 Feb 2019 16:42:15 +0100 Subject: [PATCH] Do not throw on string literals --- libsolidity/formal/SMTChecker.cpp | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 1f6e85356..b282bb4e5 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -698,17 +698,26 @@ void SMTChecker::endVisit(Literal const& _literal) solAssert(_literal.annotation().type, "Expected type for AST node"); Type const& type = *_literal.annotation().type; if (isNumber(type.category())) - defineExpr(_literal, smt::Expression(type.literalValue(&_literal))); else if (isBool(type.category())) defineExpr(_literal, smt::Expression(_literal.token() == Token::TrueLiteral ? true : false)); else + { + if (type.category() == Type::Category::StringLiteral) + { + auto stringType = make_shared(DataLocation::Memory, true); + auto stringLit = dynamic_cast(_literal.annotation().type.get()); + solAssert(stringLit, ""); + auto result = newSymbolicVariable(*stringType, stringLit->richIdentifier(), *m_interface); + m_expressions.emplace(&_literal, result.second); + } m_errorReporter.warning( _literal.location(), "Assertion checker does not yet support the type of this literal (" + _literal.annotation().type->toString() + ")." ); + } } void SMTChecker::endVisit(Return const& _return) @@ -812,6 +821,12 @@ void SMTChecker::arrayIndexAssignment(Assignment const& _assignment) expr(_assignment.rightHandSide()) ); m_interface->addAssertion(newValue(varDecl) == store); + // Update the SMT select value after the assignment, + // necessary for sound models. + defineExpr(indexAccess, smt::Expression::select( + m_variables[&varDecl]->currentValue(), + expr(*indexAccess.indexExpression()) + )); } else if (dynamic_cast(&indexAccess.baseExpression())) m_errorReporter.warning(