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 ICE on tuple assignment

Browse Source
This commit is contained in:
Leonardo Alt
2020-09-01 08:29:01 +02:00
parent 7ca335adde
commit 5cafbeebec
4 changed files with 27 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SMTEncoder.cpp
+4 -3
View File
@@ -1490,13 +1490,14 @@ void SMTEncoder::tupleAssignment(Expression const& _left, Expression const& _rig
{
auto lTuple = dynamic_cast<TupleExpression const*>(innermostTuple(_left));
solAssert(lTuple, "");
Expression const* right = innermostTuple(_right);
auto const& lComponents = lTuple->components();
// If both sides are tuple expressions, we individually and potentially
// recursively assign each pair of components.
// This is because of potential type conversion.
if (auto rTuple = dynamic_cast<TupleExpression const*>(&_right))
if (auto rTuple = dynamic_cast<TupleExpression const*>(right))
{
auto const& rComponents = rTuple->components();
solAssert(lComponents.size() == rComponents.size(), "");
@@ -1517,13 +1518,13 @@ void SMTEncoder::tupleAssignment(Expression const& _left, Expression const& _rig
}
else
{
auto rType = dynamic_cast<TupleType const*>(_right.annotation().type);
auto rType = dynamic_cast<TupleType const*>(right->annotation().type);
solAssert(rType, "");
auto const& rComponents = rType->components();
solAssert(lComponents.size() == rComponents.size(), "");
auto symbRight = expr(_right);
auto symbRight = expr(*right);
solAssert(symbRight.sort->kind == smtutil::Kind::Tuple, "");
for (unsigned i = 0; i < lComponents.size(); ++i)