CbC/CbC_gcc: gcc/ada/libgnat/a-cofove.ads comparison

comparison gcc/ada/libgnat/a-cofove.ads @ 145:1830386684a0

gcc-9.2.0

author	anatofuz
date	Thu, 13 Feb 2020 11:34:05 +0900
parents	84e7813d76e9
children

comparison

equal deleted inserted replaced

-:84e7813d76e9
+:1830386684a0
 --                                                                          --
 --         A D A . C O N T A I N E R S . F O R M A L _ V E C T O R S        --
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2004-2018, Free Software Foundation, Inc.         --
+--          Copyright (C) 2004-2019, Free Software Foundation, Inc.         --
 --                                                                          --
 -- This specification is derived from the Ada Reference Manual for use with --
 -- GNAT. The copyright notice above, and the license provisions that follow --
 -- apply solely to the  contents of the part following the private keyword. --
 --                                                                          --
 with Ada.Containers.Functional_Vectors;
 generic
 type Index_Type is range <>;
 type Element_Type is private;
+with function "=" (Left, Right : Element_Type) return Boolean is <>;
-Bounded : Boolean := True;
---  If True, the containers are bounded; the initial capacity is the maximum
---  size, and heap allocation will be avoided. If False, the containers can
---  grow via heap allocation.
 package Ada.Containers.Formal_Vectors with
 SPARK_Mode
 is
 pragma Annotate (CodePeer, Skip_Analysis);
 --  Maximal capacity of any vector. It is the minimum of the size of the
 --  index range and the last possible Count_Type.
 subtype Capacity_Range is Count_Type range 0 .. Last_Count;
-type Vector (Capacity : Capacity_Range) is limited private with
+type Vector (Capacity : Capacity_Range) is private with
-Default_Initial_Condition => Is_Empty (Vector);
+Default_Initial_Condition => Is_Empty (Vector),
---  In the bounded case, Capacity is the capacity of the container, which
+Iterable => (First       => Iter_First,
---  never changes. In the unbounded case, Capacity is the initial capacity
+Has_Element => Iter_Has_Element,
---  of the container, and operations such as Reserve_Capacity and Append can
+Next        => Iter_Next,
---  increase the capacity. The capacity never shrinks, except in the case of
+Element     => Element);
---  Clear.
---
---  Note that all objects of type Vector are constrained, including in the
---  unbounded case; you can't assign from one object to another if the
---  Capacity is different.
 function Length (Container : Vector) return Capacity_Range with
 Global => null,
 Post   => Length'Result <= Capacity (Container);
 --  limited which allows usage of 'Old and 'Loop_Entry attributes.
 Ghost,
 Global => null,
 Post   => M.Length (Model'Result) = Length (Container);
+pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Model);
 function Element
 (S : M.Sequence;
 I : Index_Type) return Element_Type renames M.Get;
 --  To improve readability of contracts, we rename the function used to
 Item      => New_Item);
 function Capacity (Container : Vector) return Capacity_Range with
 Global => null,
 Post   =>
-Capacity'Result =
+Capacity'Result = Container.Capacity;
-(if Bounded then
-Container.Capacity
-else
-Capacity_Range'Last);
 pragma Annotate (GNATprove, Inline_For_Proof, Capacity);
 procedure Reserve_Capacity
 (Container : in out Vector;
 Capacity  : Capacity_Range)
 with
 Global => null,
-Pre    => (if Bounded then Capacity <= Container.Capacity),
+Pre    => Capacity <= Container.Capacity,
 Post   => Model (Container) = Model (Container)'Old;
 function Is_Empty (Container : Vector) return Boolean with
 Global => null,
 Post   => Is_Empty'Result = (Length (Container) = 0);
 procedure Clear (Container : in out Vector) with
 Global => null,
 Post   => Length (Container) = 0;
---  Note that this reclaims storage in the unbounded case. You need to call
---  this before a container goes out of scope in order to avoid storage
---  leaks. In addition, "X := ..." can leak unless you Clear(X) first.
 procedure Assign (Target : in out Vector; Source : Vector) with
 Global => null,
-Pre    => (if Bounded then Length (Source) <= Target.Capacity),
+Pre    => Length (Source) <= Target.Capacity,
 Post   => Model (Target) = Model (Source);
 function Copy
 (Source   : Vector;
 Capacity : Capacity_Range := 0) return Vector
 with
 Global => null,
-Pre    => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity)),
+Pre    => (Capacity = 0 or Length (Source) <= Capacity),
 Post   =>
 Model (Copy'Result) = Model (Source)
 and (if Capacity = 0 then
 Copy'Result.Capacity = Length (Source)
 else
 Copy'Result.Capacity = Capacity);
 procedure Move (Target : in out Vector; Source : in out Vector)
 with
 Global => null,
-Pre    => (if Bounded then Length (Source) <= Capacity (Target)),
+Pre    => Length (Source) <= Capacity (Target),
 Post   => Model (Target) = Model (Source)'Old and Length (Source) = 0;
 function Element
 (Container : Vector;
 Index     : Index_Type) return Element_Type
 (Model (Target),
 Model (Source)'Old,
 Model (Target)'Old);
 end Generic_Sorting;
+---------------------------
+--  Iteration Primitives --
+---------------------------
+function Iter_First (Container : Vector) return Extended_Index with
+Global => null;
+function Iter_Has_Element
+(Container : Vector;
+Position  : Extended_Index) return Boolean
+with
+Global => null,
+Post   =>
+Iter_Has_Element'Result =
+(Position in Index_Type'First .. Last_Index (Container));
+pragma Annotate (GNATprove, Inline_For_Proof, Iter_Has_Element);
+function Iter_Next
+(Container : Vector;
+Position  : Extended_Index) return Extended_Index
+with
+Global => null,
+Pre    => Iter_Has_Element (Container, Position);
 private
 pragma SPARK_Mode (Off);
 pragma Inline (First_Index);
 pragma Inline (Last_Index);
 subtype Array_Index is Capacity_Range range 1 .. Capacity_Range'Last;
 type Elements_Array is array (Array_Index range <>) of Element_Type;
 function "=" (L, R : Elements_Array) return Boolean is abstract;
-type Elements_Array_Ptr is access all Elements_Array;
+type Vector (Capacity : Capacity_Range) is record
+Last     : Extended_Index := No_Index;
-type Vector (Capacity : Capacity_Range) is limited record
+Elements : Elements_Array (1 .. Capacity);
---  In the bounded case, the elements are stored in Elements. In the
---  unbounded case, the elements are initially stored in Elements, until
---  we run out of room, then we switch to Elements_Ptr.
-Last         : Extended_Index := No_Index;
-Elements_Ptr : Elements_Array_Ptr := null;
-Elements     : aliased Elements_Array (1 .. Capacity);
 end record;
---  The primary reason Vector is limited is that in the unbounded case, once
---  Elements_Ptr is in use, assignment statements won't work. "X := Y;" will
---  cause X and Y to share state; that is, X.Elements_Ptr = Y.Elements_Ptr,
---  so for example "Append (X, ...);" will modify BOTH X and Y. That would
---  allow SPARK to "prove" things that are false. We could fix that by
---  making Vector a controlled type, and override Adjust to make a deep
---  copy, but finalization is not allowed in SPARK.
---
---  Note that (unfortunately) this means that 'Old and 'Loop_Entry are not
---  allowed on Vectors.
 function Empty_Vector return Vector is
 ((Capacity => 0, others => <>));
+function Iter_First (Container : Vector) return Extended_Index is
+(Index_Type'First);
+function Iter_Next
+(Container : Vector;
+Position  : Extended_Index) return Extended_Index
+is
+(if Position = Extended_Index'Last then
+Extended_Index'First
+else
+Extended_Index'Succ (Position));
+function Iter_Has_Element
+(Container : Vector;
+Position  : Extended_Index) return Boolean
+is
+(Position in Index_Type'First .. Container.Last);
 end Ada.Containers.Formal_Vectors;

Mercurial > hg > CbC > CbC_gcc

comparison gcc/ada/libgnat/a-cofove.ads @ 145:1830386684a0