Function functionSort

libsolidity/formal/PredicateSort.cpp:72–90

}

SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition const* _contract, SymbolicState& _state)
{
	auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };
	auto varSorts = _contract ? stateSorts(*_contract) : std::vector<SortPointer>{};
	auto inputSorts = applyMap(_function.parameters(), smtSort);
	auto outputSorts = applyMap(_function.returnParameters(), smtSort);
	return std::make_shared<FunctionSort>(
		std::vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort()} +
			getBuiltInFunctionsSorts(_state) +
			std::vector<SortPointer>{_state.txSort(), _state.stateSort()} +
			varSorts +
			inputSorts +
			std::vector<SortPointer>{_state.stateSort()} +
			varSorts +
			inputSorts +
			outputSorts,
		SortProvider::boolSort
	);
}

SortPointer functionBodySort(FunctionDefinition const& _function, ContractDefinition const* _contract, SymbolicState& _state)
{