Merge pull request #4744 from ethereum/smt-magic-variable

SMT: do not crash on referencing MagicVariableDeclaration
This commit is contained in:
Alex Beregszaszi 2018-08-07 21:30:14 +01:00 committed by GitHub
commit 4dc3335cda
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

View File

@ -375,8 +375,14 @@ void SMTChecker::endVisit(Identifier const& _identifier)
}
else if (SSAVariable::isSupportedType(_identifier.annotation().type->category()))
{
VariableDeclaration const& decl = dynamic_cast<VariableDeclaration const&>(*(_identifier.annotation().referencedDeclaration));
defineExpr(_identifier, currentValue(decl));
if (VariableDeclaration const* decl = dynamic_cast<VariableDeclaration const*>(_identifier.annotation().referencedDeclaration))
defineExpr(_identifier, currentValue(*decl));
else
// TODO: handle MagicVariableDeclaration here
m_errorReporter.warning(
_identifier.location(),
"Assertion checker does not yet support the type of this variable."
);
}
else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
{