Method externalFunctionCall

libsolidity/formal/CHC.cpp:981–1068

}

void CHC::externalFunctionCall(FunctionCall const& _funCall)
{
	/// In external function calls we do not add a "predicate call"
	/// because we do not trust their function body anyway,
	/// so we just add the nondet_interface predicate.

	solAssert(m_currentContract, "");

	auto [callExpr, callOptions] = functionCallExpression(_funCall);
	FunctionType const& funType = dynamic_cast<FunctionType const&>(*callExpr->annotation().type);

	auto kind = funType.kind();
	solAssert(
		kind == FunctionType::Kind::External ||
		kind == FunctionType::Kind::BareCall ||
		kind == FunctionType::Kind::BareStaticCall,
		""
	);


	// Only consider high level external calls in trusted mode.
	if (
		kind == FunctionType::Kind::External &&
		(encodeExternalCallsAsTrusted() || isExternalCallToThis(callExpr))
	)
	{
		externalFunctionCallToTrustedCode(_funCall);
		return;
	}

	// Low level calls are still encoded nondeterministically.

	auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
	if (function)
		for (auto var: function->returnParameters())
			m_context.variable(*var)->increaseIndex();

	// If we see a low level call in trusted mode,
	// we need to havoc the global state.
	if (
		kind == FunctionType::Kind::BareCall &&
		encodeExternalCallsAsTrusted()
	)
		state().newStorage();

	// No reentrancy from constructor calls.
	if (!m_currentFunction || m_currentFunction->isConstructor())
		return;

	if (Expression const* value = valueOption(callOptions))
		decreaseBalanceFromOptionsValue(*value);

	auto preCallState = std::vector<smtutil::Expression>{state().state()} + currentStateVariables();

	if (!usesStaticCall(_funCall))
	{
		state().newState();
		for (auto const* var: m_stateVariables)