Re: Ensuring postconditions in the face of exceptions

[Niklas Holsti <niklas.holsti@tidorum.invalid>]

Ludovic Brenta 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?

Perhaps change the mode of Dirty to

    Dirty : access T;

and assign

    Dirty.all := True;

Or use a named access type instead of the anonymous access, as you prefer.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .