[SMTChecker] Relax assertion about callstack

This commit is contained in:
Leonardo Alt 2020-05-29 18:20:15 +02:00
parent 0a71e41501
commit ede39fc2da
2 changed files with 13 additions and 2 deletions

View File

@ -104,8 +104,7 @@ void VariableUsage::checkIdentifier(Identifier const& _identifier)
solAssert(declaration, "");
if (VariableDeclaration const* varDecl = dynamic_cast<VariableDeclaration const*>(declaration))
{
solAssert(m_lastCall, "");
if (!varDecl->isLocalVariable() || varDecl->functionOrModifierDefinition() == m_lastCall)
if (!varDecl->isLocalVariable() || (m_lastCall && varDecl->functionOrModifierDefinition() == m_lastCall))
m_touchedVariables.insert(varDecl);
}
}

View File

@ -0,0 +1,12 @@
pragma experimental SMTChecker;
contract c {
uint x;
function f() internal returns (uint) {
x = x + 1;
}
bool b = (f() > 0) || (f() > 0);
}
// ----
// Warning: (100-105): Overflow (resulting value larger than 2**256 - 1) happens here
// Warning: (100-105): Underflow (resulting value less than 0) happens here
// Warning: (100-105): Overflow (resulting value larger than 2**256 - 1) happens here