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

Merge remote-tracking branch 'origin/develop' into breaking

Browse Source
This commit is contained in:
chriseth
2020-12-14 11:33:40 +01:00
parent 8db2cad45c e37e3099aa
commit 561280a5cc
112 changed files with 950 additions and 226 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SMTEncoder.cpp
+14 -2
View File
@@ -512,7 +512,13 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
auto decl = identifierToVariable(*identifier);
solAssert(decl, "");
auto innerValue = currentValue(*decl);
auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1;
auto newValue = arithmeticOperation(
_op.getOperator() == Token::Inc ? Token::Add : Token::Sub,
innerValue,
smtutil::Expression(size_t(1)),
_op.annotation().type,
_op
).first;
defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
assignment(*decl, newValue);
}
@@ -522,7 +528,13 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
)
{
auto innerValue = expr(*subExpr);
auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1;
auto newValue = arithmeticOperation(
_op.getOperator() == Token::Inc ? Token::Add : Token::Sub,
innerValue,
smtutil::Expression(size_t(1)),
_op.annotation().type,
_op
).first;
defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
indexOrMemberAssignment(*subExpr, newValue);
}