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

[SMTChecker] Set unknown values for return variables of recursive functions

Browse Source
This commit is contained in:
Leonardo Alt 2019-08-09 15:26:47 +02:00
parent 682a3ece3b
commit 11d8cf588e
1 changed files with 12 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
libsolidity/formal/BMC.cpp
View File

@ -393,12 +393,22 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
solAssert(shouldInlineFunctionCall(_funCall), ""); solAssert(shouldInlineFunctionCall(_funCall), "");
FunctionDefinition const* funDef = functionCallToDefinition(_funCall); FunctionDefinition const* funDef = functionCallToDefinition(_funCall);
solAssert(funDef, ""); solAssert(funDef, "");
if (visitedFunction(funDef)) if (visitedFunction(funDef))
{
auto const& returnParams = funDef->returnParameters();
for (auto param: returnParams)
{
m_context.newValue(*param);
m_context.setUnknownValue(*param);
}
m_errorReporter.warning( m_errorReporter.warning(
_funCall.location(), _funCall.location(),
"Assertion checker does not support recursive function calls.", "Assertion checker does not support recursive function calls.",
SecondarySourceLocation().append("Starting from function:", funDef->location()) SecondarySourceLocation().append("Starting from function:", funDef->location())
); );
}
else else
{ {
vector<smt::Expression> funArgs; vector<smt::Expression> funArgs;
@ -425,9 +435,9 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
if (m_callStack.empty()) if (m_callStack.empty())
initFunction(*funDef); initFunction(*funDef);
funDef->accept(*this); funDef->accept(*this);
createReturnedExpressions(_funCall);
} }
createReturnedExpressions(_funCall);
} }
void BMC::abstractFunctionCall(FunctionCall const& _funCall) void BMC::abstractFunctionCall(FunctionCall const& _funCall)