cerc-io/solidity
11
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 fixed point inc/dec

Browse Source
This commit is contained in:
Leonardo Alt
2020-05-28 10:56:06 +02:00
parent ee8307ceed
commit cb1cbbc1f1
4 changed files with 12 additions and 5 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SMTEncoder.cpp
+2 -5
View File
@@ -463,9 +463,6 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
createExpr(_op);
if (_op.annotation().type->category() == Type::Category::FixedPoint)
return;
switch (_op.getOperator())
{
case Token::Not: // !
@@ -477,8 +474,8 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
case Token::Inc: // ++ (pre- or postfix)
case Token::Dec: // -- (pre- or postfix)
{
solAssert(smt::isInteger(_op.annotation().type->category()), "");
auto cat = _op.annotation().type->category();
solAssert(smt::isInteger(cat) || smt::isFixedPoint(cat), "");
solAssert(_op.subExpression().annotation().willBeWrittenTo, "");
if (auto identifier = dynamic_cast<Identifier const*>(&_op.subExpression()))
{