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

Do not throw on string literals

Browse Source
This commit is contained in:
Leonardo Alt 2019-02-20 16:42:15 +01:00
parent cb6c2b33f8
commit 467c34999f
1 changed files with 16 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
libsolidity/formal/SMTChecker.cpp
View File

@ -698,17 +698,26 @@ void SMTChecker::endVisit(Literal const& _literal)
solAssert(_literal.annotation().type, "Expected type for AST node"); solAssert(_literal.annotation().type, "Expected type for AST node");
Type const& type = *_literal.annotation().type; Type const& type = *_literal.annotation().type;
if (isNumber(type.category())) if (isNumber(type.category()))
defineExpr(_literal, smt::Expression(type.literalValue(&_literal))); defineExpr(_literal, smt::Expression(type.literalValue(&_literal)));
else if (isBool(type.category())) else if (isBool(type.category()))
defineExpr(_literal, smt::Expression(_literal.token() == Token::TrueLiteral ? true : false)); defineExpr(_literal, smt::Expression(_literal.token() == Token::TrueLiteral ? true : false));
else else
{
if (type.category() == Type::Category::StringLiteral)
{
auto stringType = make_shared<ArrayType>(DataLocation::Memory, true);
auto stringLit = dynamic_cast<StringLiteralType const*>(_literal.annotation().type.get());
solAssert(stringLit, "");
auto result = newSymbolicVariable(*stringType, stringLit->richIdentifier(), *m_interface);
m_expressions.emplace(&_literal, result.second);
}
m_errorReporter.warning( m_errorReporter.warning(
_literal.location(), _literal.location(),
"Assertion checker does not yet support the type of this literal (" + "Assertion checker does not yet support the type of this literal (" +
_literal.annotation().type->toString() + _literal.annotation().type->toString() +
")." ")."
); );
}
} }
void SMTChecker::endVisit(Return const& _return) void SMTChecker::endVisit(Return const& _return)
@ -812,6 +821,12 @@ void SMTChecker::arrayIndexAssignment(Assignment const& _assignment)
expr(_assignment.rightHandSide()) expr(_assignment.rightHandSide())
); );
m_interface->addAssertion(newValue(varDecl) == store); 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 const*>(&indexAccess.baseExpression())) else if (dynamic_cast<IndexAccess const*>(&indexAccess.baseExpression()))
m_errorReporter.warning( m_errorReporter.warning(