| 90 | } |
| 91 | |
| 92 | SortPointer functionBodySort(FunctionDefinition const& _function, ContractDefinition const* _contract, SymbolicState& _state) |
| 93 | { |
| 94 | auto fSort = std::dynamic_pointer_cast<FunctionSort>(functionSort(_function, _contract, _state)); |
| 95 | solAssert(fSort, ""); |
| 96 | |
| 97 | auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); }; |
| 98 | return std::make_shared<FunctionSort>( |
| 99 | fSort->domain + applyMap(SMTEncoder::localVariablesIncludingModifiers(_function, _contract), smtSort), |
| 100 | SortProvider::boolSort |
| 101 | ); |
| 102 | } |
| 103 | |
| 104 | SortPointer arity0FunctionSort() |
| 105 | { |
no test coverage detected