9.7 Termination analysis options
For detailed explanations, see the “Termination analysis” section
of the “Implementation-dependent extensions” chapter in the Mercury
Language Reference Manual.
- Enable termination analysis. Termination analysis analyses each mode of
each predicate to see whether it terminates. The ‘terminates’,
‘does_not_terminate’ and ‘check_termination’
pragmas have no effect unless termination analysis is enabled. When
using termination, ‘--intermodule-optimization’ should be enabled,
as it greatly improves the accuracy of the analysis.
- Enable termination analysis, and emit warnings for some predicates or
functions that cannot be proved to terminate. In many cases in which the
compiler is unable to prove termination, the problem is either a lack of
information about the termination properties of other predicates, or the
fact that the program used language constructs (such as higher order
calls) which cannot be analysed. In these cases the compiler does
not emit a warning of non-termination, as it is likely to be spurious.
- Enable termination analysis, and emit warnings for all predicates or
functions that cannot be proved to terminate.
- When performing termination analysis, try analyzing
recursion on single arguments in strongly connected
components of the call graph that have up to limit procedures.
Setting this limit to zero disables single argument analysis.
- The norm defines how termination analysis measures the size
of a memory cell. The ‘simple’ norm says that size is always one.
The ‘total’ norm says that it is the number of words in the cell.
The ‘num-data-elems’ norm says that it is the number of words in
the cell that contain something other than pointers to cells of
the same type.
- Print at most n reasons for any single termination error.
- Perform termination analysis only on predicates with at most n paths.