From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,c80e6f742e73478f
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,UTF8
Path: 
 g2news2.google.com!news4.google.com!proxad.net!feeder1-2.proxad.net!newsfeed.straub-nv.de!feeder.eternal-september.org!eternal-september.org!.POSTED!not-for-mail
From: Ludovic Brenta <ludovic@ludovic-brenta.org>
Newsgroups: comp.lang.ada
Subject: Re: Ensuring postconditions in the face of exceptions
Date: Sun, 14 Mar 2010 15:21:49 +0100
Organization: A noiseless patient Spider
Message-ID: <87ljdv56gy.fsf@ludovic-brenta.org>
References: 
 <820d96c0-5d67-4b8c-8c5b-811ca4f1127e@g26g2000yqn.googlegroups.com>
	<8990d686-f703-4e9c-91b7-32410289983d@g11g2000yqe.googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 8bit
Injection-Date: Sun, 14 Mar 2010 14:21:49 +0000 (UTC)
Injection-Info: feeder.eternal-september.org;
 posting-host="chCIqppqQaY9j8yrGB/6Pw";
	logging-data="16489"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1/zBhxFqDoHJ7QCpszFuLka"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/23.1 (gnu/linux)
Cancel-Lock: sha1:i0A9KPGInBIEBF045pmOYK/EgKM=
	sha1:1dIo6AUlXKdqETxRoyb4pKzJD9U=
Xref: g2news2.google.com comp.lang.ada:10532
Date: 2010-03-14T15:21:49+01:00
List-Id: <comp.lang.ada>

Alex Mentis writes:
> On Mar 12, 4:13 am, Ludovic Brenta <ludo...@ludovic-brenta.org> wrote:
>> Consider the procedure:
>>
>> type T is private; -- completion elided
>>
>> generic
>>    with procedure Visit (Object : in out T);
>> procedure Refresh (Object : in out T; Dirty : in out T) is
>> begin
>>    if Dirty then
>>       Visit (Object);
>>       Dirty := False;
>>    end if;
>> exception
>>    when others =>
>>       Dirty := True; -- warnings here
>>       raise;
>> end Refresh;
>>
>> GNAT says:
>> warning: assignment to pass-by-copy formal may have no effect
>> warning: "raise" statement may result in abnormal return (RM
>> 6.4.1(17))
>>
>> The reason for the exception handler is to enforce a postcondition
>> that Dirty must be True if Visit raises an exception. However the
>> warnings suggest that the postcondition cannot be enforced this way.
>> How should I rewrite my code?
>>
>> --
>> Ludovic Brenta.
>
> I think trying to "force" the parameter passing mode to a certain mode
> is making this more complicated than necessary.  One of the nice
> things about Ada over other languages is that you generally shouldn't
> have to worry about whether a parameter is copy-by-value or copy-by-
> reference.
>
> In this case, you are trying to use the exception handler to assign a
> value to the local parameter Dirty so that it can get passed back to
> the calling subprogram.  This implies the calling subprogram has a
> parameter in its scope that keeps track of dirtiness, too.  Instead of
> trying to set Dirty to True in Refresh, why not just raise a user-
> defined exception (such as Dirty_Error) and have an exception handler
> in the calling subprogram that catches this exception and sets the
> *calling subprogram's* variable tracking dirtiness to True?

That's an interesting suggestion but we've patched the run-time library
so that it dumps core on every exception; we use exceptions only for
exceptional situations and dumping core freezes the system for 30
seconds to produce a file roughly 300 MiB in size.  So I would rather
not raise exceptions that are do not detect a bug.

-- 
Ludovic Brenta.