Ensuring postconditions in the face of exceptions

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

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.