cerc-io/solidity
16
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 pull request #9522 from ethereum/smt_fix_tuple_pop

Browse Source 
[SMTChecker] Fix ICE in tuples again
This commit is contained in:
chriseth 2020-07-27 19:03:12 +02:00 committed by GitHub
commit 0a42ac2a5a
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 22 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
libsolidity/formal/SMTEncoder.cpp
View File

@ -1100,7 +1100,11 @@ void SMTEncoder::arrayPop(FunctionCall const& _funCall)
void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression const& _array) void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression const& _array)
{ {
if (auto const* id = dynamic_cast<Identifier const*>(&_expr)) Expression const* expr = &_expr;
if (auto const* tupleExpr = dynamic_cast<TupleExpression const*>(expr))
expr = innermostTuple(*tupleExpr);
if (auto const* id = dynamic_cast<Identifier const*>(expr))
{ {
auto varDecl = identifierToVariable(*id); auto varDecl = identifierToVariable(*id);
solAssert(varDecl, ""); solAssert(varDecl, "");
@ -1108,9 +1112,9 @@ void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression
resetReferences(*varDecl); resetReferences(*varDecl);
m_context.addAssertion(m_context.newValue(*varDecl) == _array); m_context.addAssertion(m_context.newValue(*varDecl) == _array);
} }
else if (auto const* indexAccess = dynamic_cast<IndexAccess const*>(&_expr)) else if (auto const* indexAccess = dynamic_cast<IndexAccess const*>(expr))
arrayIndexAssignment(*indexAccess, _array); arrayIndexAssignment(*indexAccess, _array);
else if (auto const* funCall = dynamic_cast<FunctionCall const*>(&_expr)) else if (auto const* funCall = dynamic_cast<FunctionCall const*>(expr))
{ {
FunctionType const& funType = dynamic_cast<FunctionType const&>(*funCall->expression().annotation().type); FunctionType const& funType = dynamic_cast<FunctionType const&>(*funCall->expression().annotation().type);
if (funType.kind() == FunctionType::Kind::ArrayPush) if (funType.kind() == FunctionType::Kind::ArrayPush)
@ -1132,7 +1136,7 @@ void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression
arrayPushPopAssign(memberAccess->expression(), symbArray->currentValue()); arrayPushPopAssign(memberAccess->expression(), symbArray->currentValue());
} }
} }
else if (dynamic_cast<MemberAccess const*>(&_expr)) else if (dynamic_cast<MemberAccess const*>(expr))
m_errorReporter.warning( m_errorReporter.warning(
9599_error, 9599_error,
_expr.location(), _expr.location(),

7
test/libsolidity/smtCheckerTests/types/tuple_array_pop_1.sol Normal file
View File

@ -0,0 +1,7 @@
pragma experimental SMTChecker;
contract C {
int[] a;
function f() public { (a).pop();}
}
// ----
// Warning 2529: (78-87): Empty array "pop" detected here.

7
test/libsolidity/smtCheckerTests/types/tuple_array_pop_2.sol Normal file
View File

@ -0,0 +1,7 @@
pragma experimental SMTChecker;
contract C {
int[] a;
function f() public { (((((a))))).pop();}
}
// ----
// Warning 2529: (78-95): Empty array "pop" detected here.