| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 0000220 | mercury | Bug | public | 2011-10-05 14:58 | 2011-10-05 15:39 | ||||||||
| Reporter | colanderman | ||||||||||||
| Assigned To | |||||||||||||
| Priority | normal | Severity | minor | Reproducibility | always | ||||||||
| Status | new | Resolution | open | ||||||||||
| Product Version | |||||||||||||
| Target Version | Fixed in Version | ||||||||||||
| Summary | 0000220: Termination analysis produces spurious "termination constant of infinity" errors | ||||||||||||
| Description | For 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 Information | 11.07-beta-2011-09-30 | ||||||||||||
| Tags | No tags attached. | ||||||||||||
| Attached Files |
| ||||||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
colanderman (reporter) 2011-10-05 15:17 |
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. |
|
colanderman (reporter) 2011-10-05 15:39 |
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 |