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.