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 compound assignment to array index

Browse Source
This commit is contained in:
Leonardo Alt
2020-07-16 17:44:10 +02:00
parent f9753a5101
commit 672633af0a
6 changed files with 53 additions and 8 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SMTEncoder.cpp
+5 -1
View File
@@ -363,8 +363,12 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
Token op = _assignment.assignmentOperator();
if (op != Token::Assign && !compoundOps.count(op))
{
Expression const* identifier = &_assignment.leftHandSide();
if (auto const* indexAccess = dynamic_cast<IndexAccess const*>(identifier))
identifier = leftmostBase(*indexAccess);
// Give it a new index anyway to keep the SSA scheme sound.
if (auto varDecl = identifierToVariable(_assignment.leftHandSide()))
solAssert(identifier, "");
if (auto varDecl = identifierToVariable(*identifier))
m_context.newValue(*varDecl);
m_errorReporter.warning(