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

Merge pull request #6100 from ethereum/smt_dynamic_cast_types

Browse Source 
[SMTChecker] Replace dynamic_cast by category check
This commit is contained in:
chriseth 2019-02-26 13:28:48 +01:00 committed by GitHub
commit 80417e3d8c
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 5 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
libsolidity/formal/SMTChecker.cpp
View File

@ -414,7 +414,7 @@ void SMTChecker::endVisit(UnaryOperation const& _op)
case Token::Sub: // - case Token::Sub: // -
{ {
defineExpr(_op, 0 - expr(_op.subExpression())); defineExpr(_op, 0 - expr(_op.subExpression()));
if (dynamic_cast<IntegerType const*>(_op.annotation().type.get())) if (_op.annotation().type->category() == Type::Category::Integer)
addOverflowTarget( addOverflowTarget(
OverflowTarget::Type::All, OverflowTarget::Type::All,
_op.annotation().type, _op.annotation().type,
@ -625,10 +625,8 @@ void SMTChecker::endVisit(Identifier const& _identifier)
{ {
// Will be translated as part of the node that requested the lvalue. // Will be translated as part of the node that requested the lvalue.
} }
else if (dynamic_cast<FunctionType const*>(_identifier.annotation().type.get())) else if (_identifier.annotation().type->category() == Type::Category::Function)
{
visitFunctionIdentifier(_identifier); visitFunctionIdentifier(_identifier);
}
else if (isSupportedType(_identifier.annotation().type->category())) else if (isSupportedType(_identifier.annotation().type->category()))
{ {
if (VariableDeclaration const* decl = dynamic_cast<VariableDeclaration const*>(_identifier.annotation().referencedDeclaration)) if (VariableDeclaration const* decl = dynamic_cast<VariableDeclaration const*>(_identifier.annotation().referencedDeclaration))
@ -1006,11 +1004,11 @@ void SMTChecker::assignment(VariableDeclaration const& _variable, Expression con
void SMTChecker::assignment(VariableDeclaration const& _variable, smt::Expression const& _value, SourceLocation const& _location) void SMTChecker::assignment(VariableDeclaration const& _variable, smt::Expression const& _value, SourceLocation const& _location)
{ {
TypePointer type = _variable.type(); TypePointer type = _variable.type();
if (dynamic_cast<IntegerType const*>(type.get())) if (type->category() == Type::Category::Integer)
addOverflowTarget(OverflowTarget::Type::All, type, _value, _location); addOverflowTarget(OverflowTarget::Type::All, type, _value, _location);
else if (dynamic_cast<AddressType const*>(type.get())) else if (type->category() == Type::Category::Address)
addOverflowTarget(OverflowTarget::Type::All, make_shared<IntegerType>(160), _value, _location); addOverflowTarget(OverflowTarget::Type::All, make_shared<IntegerType>(160), _value, _location);
else if (dynamic_cast<MappingType const*>(type.get())) else if (type->category() == Type::Category::Mapping)
arrayAssignment(); arrayAssignment();
m_interface->addAssertion(newValue(_variable) == _value); m_interface->addAssertion(newValue(_variable) == _value);
} }