Method inlineFunctionCall

libsolidity/formal/BMC.cpp:699–732

}

void BMC::inlineFunctionCall(
	FunctionDefinition const* _funDef,
	Expression const& _callStackExpr,
	std::optional<Expression const*> _boundArgumentCall,
	std::vector<Expression const*> const& _arguments
)
{
	solAssert(_funDef, "");

	if (visitedFunction(_funDef))
	{
		auto const& returnParams = _funDef->returnParameters();
		for (auto param: returnParams)
		{
			m_context.newValue(*param);
			m_context.setUnknownValue(*param);
		}
	}
	else
	{
		initializeFunctionCallParameters(*_funDef, symbolicArguments(_funDef->parameters(), _arguments, _boundArgumentCall));

		// The reason why we need to pushCallStack here instead of visit(FunctionDefinition)
		// is that there we don't have `_callStackExpr`.
		pushCallStack({_funDef, &_callStackExpr});
		pushPathCondition(currentPathConditions());
		auto oldChecked = std::exchange(m_checked, true);
		_funDef->accept(*this);
		m_checked = oldChecked;
		popPathCondition();
	}

	createReturnedExpressions(_funDef, _callStackExpr);
}

void BMC::inlineFunctionCall(FunctionCall const& _funCall)
{