Function constructorCall

libsolidity/formal/PredicateInstance.cpp:72–85

}

smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _context, bool _internal)
{
	auto const& contract = dynamic_cast<ContractDefinition const&>(*_pred.programNode());
	if (auto const* constructor = contract.constructor())
		return _pred(currentFunctionVariablesForCall(*constructor, &contract, _context, _internal));

	auto& state = _context.state();
	std::vector<smtutil::Expression> stateExprs = getStateExpressionsForCall(state, _internal);
	state.newState();
	stateExprs += std::vector<smtutil::Expression>{state.state()};
	stateExprs += currentStateVariables(contract, _context);
	stateExprs += newStateVariables(contract, _context);
	return _pred(stateExprs);
}

smtutil::Expression function(
	Predicate const& _pred,