gnatprove_13.2.1_28fc3583/share/examples/spark/gnatprove_by_example/ug__access6/test.adb

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
with Ada.Unchecked_Deallocation;

procedure Test is
   type Int_Ptr is access Integer;
   type Int_Ptr_Ptr is access Int_Ptr;

   procedure Free is new Ada.Unchecked_Deallocation (Object => Integer, Name => Int_Ptr);

   procedure Free (X : in out Int_Ptr_Ptr) with
     Depends => (X => null,
                 null => X),
     Post => X = null
   is
      procedure Internal_Free is new Ada.Unchecked_Deallocation
        (Object => Int_Ptr, Name => Int_Ptr_Ptr);
   begin
      if X /= null and then X.all /= null then
         Free (X.all);
      end if;
      Internal_Free (X);
   end Free;

   Y : Int_Ptr     := new Integer'(11);
   Z : Int_Ptr_Ptr := new Int_Ptr'(Y);
begin
   Free (Z);
end Test;