| 1682 | } |
| 1683 | |
| 1684 | Predicate const* CHC::createSummaryBlock(FunctionDefinition const& _function, ContractDefinition const& _contract, PredicateType _type) |
| 1685 | { |
| 1686 | return createSymbolicBlock( |
| 1687 | functionSort(_function, &_contract, state()), |
| 1688 | "summary_" + uniquePrefix() + "_" + predicateName(&_function, &_contract), |
| 1689 | _type, |
| 1690 | &_function, |
| 1691 | &_contract |
| 1692 | ); |
| 1693 | } |
| 1694 | |
| 1695 | Predicate const* CHC::createConstructorBlock(ContractDefinition const& _contract, std::string const& _prefix) |
| 1696 | { |
nothing calls this directly
no test coverage detected