Re: Ensuring postconditions in the face of exceptions

[Ludovic Brenta <ludovic@ludovic-brenta.org>]

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.