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

[SMTChecker] Fix ICE in fixed point operations

Browse Source
This commit is contained in:
Leonardo Alt 2019-04-30 17:45:28 +02:00
parent 73484ccaf2
commit 66655b87b0
2 changed files with 29 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -10,6 +10,7 @@ Compiler Features:
Bugfixes: Bugfixes:
* SMTChecker: Fix bad cast in base constructor modifier. * SMTChecker: Fix bad cast in base constructor modifier.
* SMTChecker: Fix internal error when visiting state variable inherited from base class. * SMTChecker: Fix internal error when visiting state variable inherited from base class.
* SMTChecker: Fix internal error in fixed point operations.

10
libsolidity/formal/SMTChecker.cpp
View File

@ -1050,6 +1050,10 @@ bool SMTChecker::shortcutRationalNumber(Expression const& _expr)
void SMTChecker::arithmeticOperation(BinaryOperation const& _op) void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
{ {
auto type = _op.annotation().commonType;
solAssert(type, "");
if (type->category() == Type::Category::Integer)
{
switch (_op.getOperator()) switch (_op.getOperator())
{ {
case Token::Add: case Token::Add:
@ -1073,6 +1077,12 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
"Assertion checker does not yet implement this operator." "Assertion checker does not yet implement this operator."
); );
} }
}
else
m_errorReporter.warning(
_op.location(),
"Assertion checker does not yet implement this operator for type " + type->richIdentifier() + "."
);
} }
smt::Expression SMTChecker::arithmeticOperation( smt::Expression SMTChecker::arithmeticOperation(