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 SMT logic error when doing compound assignment with string literlas.

Browse Source
This commit is contained in:
Djordje Mijovic
2020-11-24 19:14:15 +01:00
parent 2d235bf7b0
commit 26c43cfc66
5 changed files with 67 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SMTEncoder.cpp
+10 -4
View File
@@ -1927,18 +1927,24 @@ smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment
auto decl = identifierToVariable(_assignment.leftHandSide());
TypePointer commonType = Type::commonType(
_assignment.leftHandSide().annotation().type,
_assignment.rightHandSide().annotation().type
);
solAssert(commonType == _assignment.annotation().type, "");
if (compoundToBitwise.count(op))
return bitwiseOperation(
compoundToBitwise.at(op),
decl ? currentValue(*decl) : expr(_assignment.leftHandSide()),
expr(_assignment.rightHandSide()),
decl ? currentValue(*decl) : expr(_assignment.leftHandSide(), _assignment.annotation().type),
expr(_assignment.rightHandSide(), _assignment.annotation().type),
_assignment.annotation().type
);
auto values = arithmeticOperation(
compoundToArithmetic.at(op),
decl ? currentValue(*decl) : expr(_assignment.leftHandSide()),
expr(_assignment.rightHandSide()),
decl ? currentValue(*decl) : expr(_assignment.leftHandSide(), _assignment.annotation().type),
expr(_assignment.rightHandSide(), _assignment.annotation().type),
_assignment.annotation().type,
_assignment
);