gnatprove_14.1.1_f6ca6f8c/include/spark/spark-containers-formal-holders.ads

 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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
--
--  Copyright (C) 2022-2024, Free Software Foundation, Inc.
--
--  SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
--

private with Ada.Finalization;

private generic
   type Element_Type (<>) is private;

package SPARK.Containers.Formal.Holders is

   type Element_Type_Access is access Element_Type;

   type Holder_Type is private;

   function Element (Container : Holder_Type) return Element_Type;
   --  Return the element held by Container

   function Element_Access
     (Container : Holder_Type) return not null access Element_Type;
   --  Return the stored access.

   procedure Replace_Element
     (Container : in out Holder_Type;
      Element   : Element_Type);
   --  Replace the Holder's element by Element and do the required

   procedure Move (Target, Source : in out Holder_Type);
   --  Move the content of the source to the target.

   procedure Adjust (Source : in out Holder_Type);
   --  Make a copy of Container in order to avoid sharing

   procedure Finalize (Container : in out Holder_Type);
   --  Finalize the element held by Container if necessary. It is still
   --  possible to use a finalized Holder_Type but the former value is lost.

   function Is_Null (Container : Holder_Type) return Boolean;

private

   type Holder_Type is new Ada.Finalization.Controlled
   with record
      Element : Element_Type_Access;
   end record;

   function Is_Null (Container : Holder_Type) return Boolean is
     (Container.Element = null);
end SPARK.Containers.Formal.Holders;