cerc-io/solidity
15
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

Add better warning on binary operation on non-integer types in SMT Checker

Browse Source
This commit is contained in:
Alex Beregszaszi 2018-07-24 23:23:54 +01:00
parent 278372c13d
commit d30a6de942
1 changed files with 8 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
libsolidity/formal/SMTChecker.cpp
View File

@ -429,7 +429,14 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
case Token::Div: case Token::Div:
{ {
solAssert(_op.annotation().commonType, ""); solAssert(_op.annotation().commonType, "");
solAssert(_op.annotation().commonType->category() == Type::Category::Integer, ""); if (_op.annotation().commonType->category() != Type::Category::Integer)
{
m_errorReporter.warning(
_op.location(),
"Assertion checker does not yet implement this operator on non-integer types."
);
break;
}
auto const& intType = dynamic_cast<IntegerType const&>(*_op.annotation().commonType); auto const& intType = dynamic_cast<IntegerType const&>(*_op.annotation().commonType);
smt::Expression left(expr(_op.leftExpression())); smt::Expression left(expr(_op.leftExpression()));
smt::Expression right(expr(_op.rightExpression())); smt::Expression right(expr(_op.rightExpression()));