From 11d8cf588ede60a5d8a2fcd0edaa8df14e0efd07 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Fri, 9 Aug 2019 15:26:47 +0200 Subject: [PATCH] [SMTChecker] Set unknown values for return variables of recursive functions --- libsolidity/formal/BMC.cpp | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index f1238201e..931be1022 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -393,12 +393,22 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall) solAssert(shouldInlineFunctionCall(_funCall), ""); FunctionDefinition const* funDef = functionCallToDefinition(_funCall); solAssert(funDef, ""); + if (visitedFunction(funDef)) + { + auto const& returnParams = funDef->returnParameters(); + for (auto param: returnParams) + { + m_context.newValue(*param); + m_context.setUnknownValue(*param); + } + m_errorReporter.warning( _funCall.location(), "Assertion checker does not support recursive function calls.", SecondarySourceLocation().append("Starting from function:", funDef->location()) ); + } else { vector funArgs; @@ -425,9 +435,9 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall) if (m_callStack.empty()) initFunction(*funDef); funDef->accept(*this); - - createReturnedExpressions(_funCall); } + + createReturnedExpressions(_funCall); } void BMC::abstractFunctionCall(FunctionCall const& _funCall)