Re: Ensuring postconditions in the face of exceptions

[Stephen Leake <stephen_leake@stephe-leake.org>]

Ludovic Brenta <ludovic@ludovic-brenta.org> writes:

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

I don't see the point; Visit is not called if Dirty is not True, so
you don't need to do anything in an exception handler. So I would
rewrite it by deleting the exception handler, and maybe adding a
comment. 

Unless you meant the opposite; if Dirty is supposed to be changed to
False on exception from Visit, then you need to set Dirty in the
handler. But that doesn't seem to make sense, given what Dirty seems
to mean.

It would be clearer to localize the exception handler:

generic
   with procedure Visit (Object : in out T);
procedure Refresh (Object : in out T; Dirty : in out T) is
begin
   if Dirty then
      begin
         Visit (Object);
      exception
      when others =>
         Dirty := True; -- warnings here
         raise;
      end;
      Dirty := False;
   end if;
end Refresh;

but that's minor.

-- 
-- Stephe