Merge pull request #9051 from ethereum/smt_fix_callstack

[SMTChecker] Fix ICE in inlining function calls while short circuiting
This commit is contained in:
chriseth 2020-05-28 15:48:50 +02:00 committed by GitHub
commit 79f4a2b476
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 8 additions and 2 deletions

View File

@ -26,6 +26,7 @@ Bugfixes:
* Scanner: Fix bug when two empty NatSpec comments lead to scanning past EOL.
* Code Generator: Trigger proper unimplemented errors on certain array copy operations.
* SMTChecker: Fix internal error when applying arithmetic operators to fixed point variables.
* SMTChecker: Fix internal error when short circuiting Boolean expressions with function calls in state variable initialization.
### 0.6.8 (2020-05-14)

View File

@ -1791,7 +1791,6 @@ Expression const* SMTEncoder::leftmostBase(IndexAccess const& _indexAccess)
set<VariableDeclaration const*> SMTEncoder::touchedVariables(ASTNode const& _node)
{
solAssert(!m_callStack.empty(), "");
vector<CallableDeclaration const*> callStack;
for (auto const& call: m_callStack)
callStack.push_back(call.first);

View File

@ -33,7 +33,8 @@ set<VariableDeclaration const*> VariableUsage::touchedVariables(ASTNode const& _
m_touchedVariables.clear();
m_callStack.clear();
m_callStack += _outerCallstack;
m_lastCall = m_callStack.back();
if (!m_callStack.empty())
m_lastCall = m_callStack.back();
_node.accept(*this);
return m_touchedVariables;
}

View File

@ -0,0 +1,5 @@
pragma experimental SMTChecker;
contract c {
bool b = (f() == 0) && (f() == 0);
function f() internal returns (uint) {}
}