cerc-io/solidity
16
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 expression creation problems.

Browse Source
This commit is contained in:
chriseth 2017-10-05 19:39:29 +02:00
parent 00e252a39f
commit a256983320
1 changed files with 30 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

49
libsolidity/formal/SMTChecker.cpp
View File

@ -207,7 +207,10 @@ void SMTChecker::endVisit(Assignment const& _assignment)
{ {
Declaration const* decl = identifier->annotation().referencedDeclaration; Declaration const* decl = identifier->annotation().referencedDeclaration;
if (knownVariable(*decl)) if (knownVariable(*decl))
{
assignment(*decl, _assignment.rightHandSide(), _assignment.location()); assignment(*decl, _assignment.rightHandSide(), _assignment.location());
defineExpr(_assignment, expr(_assignment.rightHandSide()));
}
else else
m_errorReporter.warning( m_errorReporter.warning(
_assignment.location(), _assignment.location(),
@ -778,31 +781,39 @@ smt::Expression SMTChecker::maxValue(IntegerType const& _t)
smt::Expression SMTChecker::expr(Expression const& _e) smt::Expression SMTChecker::expr(Expression const& _e)
{ {
solAssert(m_expressions.count(&_e), ""); if (!m_expressions.count(&_e))
{
m_errorReporter.warning(_e.location(), "Internal error: Expression undefined for SMT solver." );
createExpr(_e);
}
return m_expressions.at(&_e); return m_expressions.at(&_e);
} }
void SMTChecker::createExpr(Expression const& _e) void SMTChecker::createExpr(Expression const& _e)
{ {
solAssert(!m_expressions.count(&_e), ""); if (m_expressions.count(&_e))
solAssert(_e.annotation().type, ""); m_errorReporter.warning(_e.location(), "Internal error: Expression created twice in SMT solver." );
switch (_e.annotation().type->category()) else
{ {
case Type::Category::RationalNumber: solAssert(_e.annotation().type, "");
{ switch (_e.annotation().type->category())
if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(_e.annotation().type.get())) {
solAssert(!rational->isFractional(), ""); case Type::Category::RationalNumber:
m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); {
break; if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(_e.annotation().type.get()))
} solAssert(!rational->isFractional(), "");
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::Integer:
m_expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e))); m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
break; break;
default: case Type::Category::Bool:
solAssert(false, "Type not implemented."); m_expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e)));
break;
default:
solAssert(false, "Type not implemented.");
}
} }
} }