From 4528ead53ae6e76cd663aa9aa3e710ca833a2fa3 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Tue, 6 Jan 2015 10:02:05 +0100 Subject: [PATCH] [multiple changes] 2015-01-06 Bob Duff * a-cfinve.adb (Copy): Set the discriminant to the Length when Capacity = 0. * a-cofove.ads (Capacity): Add a postcondition. * a-cfinve.ads (Capacity): Add a postcondition. (Reserve_Capacity): Correct the postcondition in the case where Capacity = 0; that means "Capacity => Length (Container)". * a-cofove.adb (Elems[c]): Add a comment explaining the dangers and how to avoid them. 2015-01-06 Ed Schonberg * sem_ch12.adb: Code clean up. From-SVN: r219225 --- gcc/ada/ChangeLog | 14 ++++++++++++++ gcc/ada/a-cfinve.adb | 25 ++++++++++++++++--------- gcc/ada/a-cfinve.ads | 21 +++++++++++---------- gcc/ada/a-cofove.adb | 3 +++ gcc/ada/a-cofove.ads | 3 ++- gcc/ada/sem_ch12.adb | 4 ++-- 6 files changed, 48 insertions(+), 22 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 6c1780dc52f..b0b4b967eef 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,17 @@ +2015-01-06 Bob Duff + + * a-cfinve.adb (Copy): Set the discriminant to the Length when + Capacity = 0. + * a-cofove.ads (Capacity): Add a postcondition. + * a-cfinve.ads (Capacity): Add a postcondition. + (Reserve_Capacity): Correct the postcondition in the case where + Capacity = 0; that means "Capacity => Length (Container)". + * a-cofove.adb (Elems[c]): Add a comment + explaining the dangers and how to avoid them. + +2015-01-06 Ed Schonberg + + * sem_ch12.adb: Code clean up. 2015-01-06 Arnaud Charlet * gnatvsn.ads: Bump copyright year. diff --git a/gcc/ada/a-cfinve.adb b/gcc/ada/a-cfinve.adb index 6574fcb4364..f088b9ed118 100644 --- a/gcc/ada/a-cfinve.adb +++ b/gcc/ada/a-cfinve.adb @@ -2,8 +2,7 @@ -- -- -- GNAT LIBRARY COMPONENTS -- -- -- --- A D A . C O N T A I N E R S --- . F O R M A L _ I N D E F I N I T E _ V E C T O R S -- +-- ADA.CONTAINERS.FORMAL_INDEFINITE_VECTORS -- -- -- -- B o d y -- -- -- @@ -89,7 +88,8 @@ is function Contains (Container : Vector; - Item : Element_Type) return Boolean is + Item : Element_Type) return Boolean + is (Contains (Container.V, H (Item))); ---------- @@ -98,8 +98,10 @@ is function Copy (Source : Vector; - Capacity : Capacity_Range := 0) return Vector is - (Capacity, V => Copy (Source.V, Capacity)); + Capacity : Capacity_Range := 0) return Vector + is + ((if Capacity = 0 then Length (Source) else Capacity), + V => Copy (Source.V, Capacity)); --------------------- -- Current_To_Last -- @@ -139,7 +141,8 @@ is function Find_Index (Container : Vector; Item : Element_Type; - Index : Index_Type := Index_Type'First) return Extended_Index is + Index : Index_Type := Index_Type'First) return Extended_Index + is (Find_Index (Container.V, H (Item), Index)); ------------------- @@ -200,7 +203,9 @@ is ----------------- function Has_Element - (Container : Vector; Position : Extended_Index) return Boolean is + (Container : Vector; + Position : Extended_Index) return Boolean + is (Has_Element (Container.V, Position)); -------------- @@ -272,7 +277,8 @@ is function Reverse_Find_Index (Container : Vector; Item : Element_Type; - Index : Index_Type := Index_Type'Last) return Extended_Index is + Index : Index_Type := Index_Type'Last) return Extended_Index + is (Reverse_Find_Index (Container.V, H (Item), Index)); ---------- @@ -290,7 +296,8 @@ is function To_Vector (New_Item : Element_Type; - Length : Capacity_Range) return Vector is + Length : Capacity_Range) return Vector + is begin return (Length, To_Vector (H (New_Item), Length)); end To_Vector; diff --git a/gcc/ada/a-cfinve.ads b/gcc/ada/a-cfinve.ads index b78633b4f8c..7559df6e4b5 100644 --- a/gcc/ada/a-cfinve.ads +++ b/gcc/ada/a-cfinve.ads @@ -2,8 +2,7 @@ -- -- -- GNAT LIBRARY COMPONENTS -- -- -- --- A D A . C O N T A I N E R S --- . F O R M A L _ I N D E F I N I T E _ V E C T O R S -- +-- ADA.CONTAINERS.FORMAL_INDEFINITE_VECTORS -- -- -- -- S p e c -- -- -- @@ -41,7 +40,7 @@ generic type Index_Type is range <>; type Element_Type (<>) is private; Max_Size_In_Storage_Elements : Natural := - Element_Type'Max_Size_In_Storage_Elements; + Element_Type'Max_Size_In_Storage_Elements; -- This has the same meaning as in Ada.Containers.Bounded_Holders, with the -- same restrictions. @@ -81,7 +80,8 @@ is Global => null; function Capacity (Container : Vector) return Capacity_Range with - Global => null; + Global => null, + Post => Capacity'Result >= Container.Capacity; procedure Reserve_Capacity (Container : in out Vector; @@ -111,7 +111,7 @@ is Capacity : Capacity_Range := 0) return Vector with Global => null, - Pre => (if Bounded then Length (Source) <= Capacity); + Pre => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity)); function Element (Container : Vector; @@ -133,16 +133,17 @@ is New_Item : Vector) with Global => null, - Pre => (if Bounded then - Length (Container) + Length (New_Item) <= Container.Capacity); + Pre => (if Bounded + then Length (Container) + Length (New_Item) <= + Container.Capacity); procedure Append (Container : in out Vector; New_Item : Element_Type) with Global => null, - Pre => (if Bounded then - Length (Container) < Container.Capacity); + Pre => (if Bounded + then Length (Container) < Container.Capacity); procedure Delete_Last (Container : in out Vector) @@ -243,7 +244,7 @@ private package Def is new Formal_Vectors (Index_Type, Holder, "=", Bounded); use Def; - -- ????Assert that Def subtypes have the same range. + -- ????Assert that Def subtypes have the same range type Vector (Capacity : Capacity_Range) is limited record V : Def.Vector (Capacity); diff --git a/gcc/ada/a-cofove.adb b/gcc/ada/a-cofove.adb index 9cfd1328cf2..ef37cc0226e 100644 --- a/gcc/ada/a-cofove.adb +++ b/gcc/ada/a-cofove.adb @@ -59,6 +59,9 @@ is -- possible bounds. This means that the pointer is a thin pointer. This is -- necessary because 'Unrestricted_Access doesn't work when it produces -- access-to-unconstrained and is returned from a function. + -- + -- Note that this is dangerous: make sure calls to this use an indexed + -- component or slice that is within the bounds 1 .. Length (Container). function Get_Element (Container : Vector; diff --git a/gcc/ada/a-cofove.ads b/gcc/ada/a-cofove.ads index 9e91bc8bae0..3d4c1b37ecd 100644 --- a/gcc/ada/a-cofove.ads +++ b/gcc/ada/a-cofove.ads @@ -84,7 +84,8 @@ is Global => null; function Capacity (Container : Vector) return Capacity_Range with - Global => null; + Global => null, + Post => Capacity'Result >= Container.Capacity; procedure Reserve_Capacity (Container : in out Vector; diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index 6062a88d60f..ab118c62075 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -1804,12 +1804,13 @@ package body Sem_Ch12 is (Defining_Entity (Analyzed_Formal))) and then Ekind (Defining_Entity (Analyzed_Formal)) = E_Function + and then Expander_Active then -- If actual is an entity (function or operator), -- and expander is active, build wrapper for it. -- Note that wrappers play no role within a generic. - if Present (Match) and then Expander_Active then + if Present (Match) then if Nkind (Match) = N_Operator_Symbol then -- If the name is a default, find its visible @@ -1837,7 +1838,6 @@ package body Sem_Ch12 is elsif Box_Present (Formal) and then Nkind (Defining_Entity (Analyzed_Formal)) = N_Defining_Operator_Symbol - and then Expander_Active then Append_To (Assoc, Build_Operator_Wrapper -- 2.30.2