Re: Ensuring postconditions in the face of exceptions

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

Ludovic Brenta wrote on comp.lang.ada:
> 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

Sorry, I meant:

procedure Refresh (Object : in out T; Dirty : in out Boolean) 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.