Function constructor

libsolidity/formal/PredicateInstance.cpp:61–70

}

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

	auto& state = _context.state();
	std::vector<smtutil::Expression> stateExprs = getStateExpressionsForConstructor(state);
	return _pred(stateExprs + initialStateVariables(contract, _context) + currentStateVariables(contract, _context));
}

smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _context, bool _internal)
{