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-term

--enable-termination

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.

--chk-term

--check-term

--check-termination

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.

--verb-chk-term

--verb-check-term

--verbose-check-termination

Enable termination analysis, and emit warnings for all predicates or functions that cannot be proved to terminate.

--term-single-arg limit

--termination-single-argument-analysis limit

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.

--termination-norm norm

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.

--term-err-limit limit

--termination-error-limit limit

Print at most n reasons for any single termination error.

--term-path-limit limit

--termination-path-limit limit

Perform termination analysis only on predicates with at most n paths.