cerc-io/solidity
10
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

Merge pull request #7208 from ethereum/smt_recursive_functions_return_vars

Browse Source 
[SMTChecker] Set unknown for return vars of recursive functions
This commit is contained in:
Leonardo 2019-08-09 18:08:40 +02:00 committed by GitHub
commit dcfa70b1a8
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
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)