[m-rev.] for review: improve termination analysis of standard library

Julien Fischer juliensf at students.cs.mu.OZ.AU
Fri Oct 17 16:17:56 AEST 2003


Estimated hours taken: 0.5
Branches: main

Perform termination analysis with single argument analysis enabled
when building several modules in the standard library.
This increases the number of predicates whose termination can be
inferred and should make the termination analyser a little
more accurate when analysing programs that use the standard library.  In
cases where termination cannot be proven this change is still useful because
it may reduce the number of causes of non-termination reported.

The modules in question are bag, io, list, stack and tree234.
The amount of extra time required for the analysis is negligible.

library/Mercury.options:
	Use single argument analysis when using the termination analyser
	to analyse bag, io, list, stack and tree234.


Index: Mercury.options
===================================================================
RCS file: /home/mercury1/repository/mercury/library/Mercury.options,v
retrieving revision 1.1
diff -u -r1.1 Mercury.options
--- Mercury.options	22 Jun 2002 19:16:03 -0000	1.1
+++ Mercury.options	17 Oct 2003 05:45:58 -0000
@@ -25,3 +25,12 @@
 MGNUCFLAGS-io =	--no-ansi

 MCFLAGS-mer_std = --no-warn-nothing-exported
+
+# Several predicates in the modules below cannot be proven to terminate
+# using the normal termination analysis algorithm *but* can be shown
+# to terminate using single argument analysis.
+MCFLAGS-bag += --term-single-arg 2
+MCFLAGs-io += --term-single-arg 2
+MCFLAGS-list += --term-single-arg 2
+MCFLAGS-stack += --term-single-arg 2
+MCFLAGS-tree234 += --term-single-arg 2

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



More information about the reviews mailing list