[m-rev.] for review: add terminates pragmas to throw/1 and error/1

[Julien Fischer]

Estimated hours taken: 1
Branches: main

Add pragma terminates declarations to exception.builtin_throw/1,
exception.throw/1 and require.error/1.

The point of this change is to try and reduce the number of cases of
possible non-termination being reported in the standard library due to
calls to require.error/1 or exception.throw/1.

Ideally we would only need provide a terminates declaration for
builtin_throw/1 but in practice the structure of the module dependency graph
means that error/1 is marked as non-terminating and certain calls to throw/1
are also considered to be non-terminating.

library/exception.m:
	Add pragma terminates declaration for builtin_throw/1 and
	throw/1.
library/require.m:
	Add pragma terminates declaration for error/1.


Index: exception.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/exception.m,v
retrieving revision 1.82
diff -u -r1.82 exception.m
--- exception.m	7 Nov 2003 16:51:34 -0000	1.82
+++ exception.m	13 Nov 2003 04:23:55 -0000
@@ -293,6 +293,12 @@
 :- pragma no_inline(throw/1).
 :- pragma no_inline(rethrow/1).

+% The termination analyzer can infer termination
+% of throw/1 itself but declaring it to be terminating
+% here means that all of the standard library will
+% treat it as terminating as well.
+:- pragma terminates(throw/1).
+
 throw(Exception) :-
 	type_to_univ(Exception, Univ),
 	throw_impl(Univ).
@@ -608,6 +614,7 @@
 % builtin_throw and builtin_catch are implemented below using
 % hand-coded low-level C code.
 %
+:- pragma terminates(builtin_throw/1).
 :- pred builtin_throw(univ).
 :- mode builtin_throw(in) is erroneous.

Index: require.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/require.m,v
retrieving revision 1.30
diff -u -r1.30 require.m
--- require.m	15 Jan 2002 03:03:23 -0000	1.30
+++ require.m	13 Nov 2003 04:24:53 -0000
@@ -93,6 +93,10 @@
 % Hopefully error/1 won't be called often (!), so no point inlining it.
 :- pragma no_inline(error/1).

+% We declare error/1 to be terminating so that all of the standard library
+% will treat it as terminating.
+:- pragma terminates(error/1).
+
 error(Message) :-
 	throw(software_error(Message)).


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