9.18 Options that control program analyses

--enable-termination

--enable-term

Enable termination analysis, which analyses each mode of each predicate or function to see whether it terminates. The terminates, does_not_terminate, and check_termination pragmas have an effect only when termination analysis is enabled.

Note that both ‘--intermodule-optimization’ and ‘--transitive-intermodule-optimization’ greatly improve the accuracy of the analysis.

--check-termination

--check-term

--chk-term

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

In many cases where the compiler is unable to prove termination, the problem is either a lack of information about the termination properties of other predicates, or the use of language constructs (such as higher order calls) which are beyond the capabilities of the analyser. In these cases, the compiler does not emit a warning of non-termination, as it is likely to be spurious.

--verbose-check-termination

--verb-check-term

--verb-chk-term

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

--termination-single-argument-analysis N

--term-single-arg N

When performing termination analysis, try analyzing recursion on single arguments in strongly connected components of the call graph that have up to the given number of procedures. Setting this limit to zero disables single argument analysis.

--termination-norm {simple, total, num-data-elems}

--term-norm {simple, total, num-data-elems}

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.

--termination-error-limit N

--term-err-limit N

Print at most this number of reasons for any single termination error (default: 3).

--termination-path-limit N

--term-path-limit N

Perform termination analysis only on predicates with at most this many paths (default: 256).

--analyse-exceptions

Enable exception analysis. which tries to identify procedures that will not throw an exception. Some optimizations can make use of this information.

--analyse-trail-usage

Enable trail usage analysis, which tries to identify procedures that will not modify the trail. The compiler can use this information to reduce the overhead of trailing.

--analyse-mm-tabling

Identify those goals that do not call procedures that are evaluated using minimal model tabling. The compiler can use this information to reduce the overhead of minimal model tabling.