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

Fix issue with pop on storage array.

Browse Source
This commit is contained in:
Alexander Arlt
2021-02-23 14:26:55 +01:00
committed by chriseth
parent 3dcba53595
commit ae6996efc1
9 changed files with 73 additions and 56 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SMTEncoder.cpp
+1 -4
View File
@@ -718,7 +718,6 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
break;
}
case FunctionType::Kind::ArrayPush:
case FunctionType::Kind::ByteArrayPush:
arrayPush(_funCall);
break;
case FunctionType::Kind::ArrayPop:
@@ -1656,8 +1655,6 @@ void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression
else if (auto const* funCall = dynamic_cast<FunctionCall const*>(expr))
{
FunctionType const& funType = dynamic_cast<FunctionType const&>(*funCall->expression().annotation().type);
// Push cannot occur on an expression that is itself a ByteArrayPush, i.e., bytes.push().push() is not possible.
solAssert(funType.kind() != FunctionType::Kind::ByteArrayPush, "");
if (funType.kind() == FunctionType::Kind::ArrayPush)
{
auto memberAccess = dynamic_cast<MemberAccess const*>(&funCall->expression());
@@ -2649,7 +2646,7 @@ MemberAccess const* SMTEncoder::isEmptyPush(Expression const& _expr) const
)
{
auto const& funType = dynamic_cast<FunctionType const&>(*funCall->expression().annotation().type);
if (funType.kind() == FunctionType::Kind::ArrayPush || funType.kind() == FunctionType::Kind::ByteArrayPush)
if (funType.kind() == FunctionType::Kind::ArrayPush)
return &dynamic_cast<MemberAccess const&>(funCall->expression());
}
return nullptr;