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] Fixed internal error when increment/decrement is applied on a result of push().

Browse Source
This commit is contained in:
Martin Blicha
2020-12-14 22:52:44 +01:00
parent 2ca70bd71a
commit 71f835b71b
3 changed files with 42 additions and 14 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SMTEncoder.cpp
+18 -14
View File
@@ -507,18 +507,21 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
{
solAssert(smt::isInteger(*type) || smt::isFixedPoint(*type), "");
solAssert(subExpr->annotation().willBeWrittenTo, "");
auto computeNewValue = [&](auto currentValue) {
return arithmeticOperation(
_op.getOperator() == Token::Inc ? Token::Add : Token::Sub,
currentValue,
smtutil::Expression(size_t(1)),
_op.annotation().type,
_op
).first;
};
if (auto identifier = dynamic_cast<Identifier const*>(subExpr))
{
auto decl = identifierToVariable(*identifier);
solAssert(decl, "");
auto innerValue = currentValue(*decl);
auto newValue = arithmeticOperation(
_op.getOperator() == Token::Inc ? Token::Add : Token::Sub,
innerValue,
smtutil::Expression(size_t(1)),
_op.annotation().type,
_op
).first;
auto newValue = computeNewValue(innerValue);
defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
assignment(*decl, newValue);
}
@@ -528,16 +531,17 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
)
{
auto innerValue = expr(*subExpr);
auto newValue = arithmeticOperation(
_op.getOperator() == Token::Inc ? Token::Add : Token::Sub,
innerValue,
smtutil::Expression(size_t(1)),
_op.annotation().type,
_op
).first;
auto newValue = computeNewValue(innerValue);
defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
indexOrMemberAssignment(*subExpr, newValue);
}
else if (isEmptyPush(*subExpr))
{
auto innerValue = expr(*subExpr);
auto newValue = computeNewValue(innerValue);
defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
arrayPushPopAssign(*subExpr, newValue);
}
else
solAssert(false, "");