Re: Ensuring postconditions in the face of exceptions

[Alex Mentis <asmentis@gmail.com>]

On Mar 14, 10:21 am, Ludovic Brenta <ludo...@ludovic-brenta.org>
wrote:
> 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.

Well, I'm not sure I'm suggesting you raise extra exceptions, just
handle them in the calling subprogram instead of the called
subprogram.  You're already re-raising the exception with the called
subprogram exception handler:

> >> exception
> >>    when others =>
> >>       Dirty := True; -- warnings here
> >>       raise;

You don't have to create a user-defined exception.  Consider the
following code:

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;

-- This handler isn't necessary, but I put it here to help illustrate
-- the changes I'm recommending.
exception
   when others =>
      raise;
end Refresh;

*****

procedure Calls_Refresh is

   Obj : T;
   Calling_Scope_Dirty : Boolean;

begin

   -- potentially other code here

   Dirty_Handler_Block :
   begin

      Refresh(Obj, Calling_Scope_Dirty);

   exception
      when others =>
         Calling_Scope_Dirty : True;
         -- potentially other handler code here

   end Dirty_Handler_Block;

   -- potentially other code here

end Calls_Refresh;