[m-rev.] for review: change termination analysis error reporting

[Julien Fischer]

On Thu, 8 Jan 2004, Fergus Henderson wrote:

> On 08-Jan-2004, Julien Fischer <juliensf at students.cs.mu.OZ.AU> wrote:
> >
> > Modify the termination analysis so that when `--check-termination'
> > is enabled and if there are no direct reasons (in the sense defined in
> > term_errors.m) for the non-termination of a procedure then the indirect
> > reasons are reported. (Currently indirect reasons will only be reported
> > if `--verbose-check-termination' is enabled.)
> >
> > This should reduce occurrences of the termination analysis reporting
> > that termination cannot be proven for unknown reasons(s).
> >
> > compiler/termination.m:
> > 	Alter the reporting of error messages, so that if there are no
> > 	direct cause of non-termination we report the indirect ones.
>
> Do you need to update the expected output for the test cases
> in tests/termination?
>

No, the tests in tests/term check the contents of the .trans_opt files - they
will still be the same after this change.

> If so, please do so; if not, please add a test case to test this change.
>

I've added the following test case in tests/warnings.  (An addition to
the log message and the diff follow).

tests/warnings/Mercury.options:
tests/warnings/Mmakefile:
tests/warnings/term_indirect_warning.m:
tests/warnings/term_indirect_warning.exp:
	Add a test case for this.

Index: Mercury.options
===================================================================
RCS file: /home/mercury1/repository/tests/warnings/Mercury.options,v
retrieving revision 1.8
diff -u -r1.8 Mercury.options
--- Mercury.options	24 Jul 2003 07:59:46 -0000	1.8
+++ Mercury.options	8 Jan 2004 08:00:20 -0000
@@ -34,9 +34,10 @@
 MCFLAGS-infinite_recursion	= --excess-assign --common-struct

 MCFLAGS-warn_stubs		= --allow-stubs --warn-unused-args
-
-	# Conflicting termination pragmas won't show up unless we
-	# perform termination analysis.
+
+	# For tests that involve the termination analysis we need
+	# to make sure that it is enabled otherwise the tests will fail.
 MCFLAGS-pragma_term_conflict = --enable-termination
+MCFLAGS-term_indirect_warning = --check-termination

 MCFLAGS-warn_dead_procs 	= --warn-dead-procs --infer-all
Index: Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/warnings/Mmakefile,v
retrieving revision 1.32
diff -u -r1.32 Mmakefile
--- Mmakefile	23 Jul 2003 03:38:17 -0000	1.32
+++ Mmakefile	8 Jan 2004 07:54:16 -0000
@@ -7,6 +7,7 @@
 COMPILE_PROGS=	\
 	arg_order_rearrangment \
 	pragma_term_conflict \
+	term_indirect_warning \
 	warn_dead_procs

 ERRORCHECK_PROGS= \
Index: term_indirect_warning.exp
===================================================================
RCS file: term_indirect_warning.exp
diff -N term_indirect_warning.exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ term_indirect_warning.exp	8 Jan 2004 07:54:44 -0000
@@ -0,0 +1,4 @@
+term_indirect_warning.m:015: Termination of
+term_indirect_warning.m:015:   predicate `term_indirect_warning.foo/3' mode 0
+term_indirect_warning.m:015:   not proven for the following reason:
+term_indirect_warning.m:020: It contains a higher order call.
Index: term_indirect_warning.m
===================================================================
RCS file: term_indirect_warning.m
diff -N term_indirect_warning.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ term_indirect_warning.m	8 Jan 2004 07:58:01 -0000
@@ -0,0 +1,18 @@
+% Tests that the termination analyser gives a reason for reporting
+% non-termination when `--check-termination' is enabled rather than
+% just reporting that it couldn't prove termination for unknown reasons.
+
+:- module term_indirect_warning.
+
+:- interface.
+
+:- type nat ---> zero ; s(nat).
+
+:- pred foo(pred(nat), nat, nat).
+:- mode foo(pred(in) is det, in, out) is det.
+
+:- implementation.
+
+foo(P, X, s(s(X))) :- P(X).
+
+:- end_module term_indirect_warning.
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------