2024-03-29 10:29 AEDT

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000220mercuryBugpublic2011-10-05 15:39
Reportercolanderman 
Assigned To 
PrioritynormalSeverityminorReproducibilityalways
StatusnewResolutionopen 
Product Version 
Target VersionFixed in Version 
Summary0000220: Termination analysis produces spurious "termination constant of infinity" errors
DescriptionFor certain (not all) functions and/or predicates XXX and YYY, where YYY has :- pragma terminates set, termination analysis will report that:

"Termination of predicate XXX not proven for the following reason:
 It calls predicate YYY which has a termination constant of infinity."

and that:

"Termination constant of function YYY set to infinity for the following reason:
 It contains one or more predicates and/or functions imported from another module."

Expected behavior is that :- pragma terminates(YYY) causes the compiler to assume YYY terminates, regardless of its body.

This bug is not exhibited by all such predicates or functions; see attached test case.
Additional Information11.07-beta-2011-09-30
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0000364

colanderman (reporter)

Looking through the compiler source I think I understand why: because the output arguments of a function/predicate are considered as a whole. In the attached example, one output argument (which does decrease) is used, but the other (which is not known to decrease) is not. The compiler does not maintain enough info to distinguish the two, so it necessarily infers the worst case (infinite termination constant).

Perhaps :- pragma terminates() should allow optional setting of the termination constant for a given mode? Or should set it to 0?

Either way this is probably a wishlist item and not a bug per se.

~0000365

colanderman (reporter)

Nevermind. I just found :- pragma termination_info, and --check-term2, which seems to obviate this need entirely. You guys are good at keeping secrets ;)
+Notes

-Issue History
Date Modified Username Field Change
2011-10-05 14:58 colanderman New Issue
2011-10-05 14:58 colanderman File Added: termination.m
2011-10-05 14:59 colanderman File Added: termination.err
2011-10-05 15:17 colanderman Note Added: 0000364
2011-10-05 15:39 colanderman Note Added: 0000365
+Issue History