[multiple changes]
2014-11-07 Robert Dewar <dewar@adacore.com> * freeze.adb: Code clean up. 2014-11-07 Yannick Moy <moy@adacore.com> * a-cfdlli.ads, a-cfhama.ads, a-cfhase.ads, a-cfinve.ads, * a-cforma.ads, a-cforse.ads, a-cofove.ads: Mark First_To_Previous, Current_To_Last and Strict_Equal as Ghost. 2014-11-07 Ed Schonberg <schonberg@adacore.com> * sem_ch3.adb: Code clean up. From-SVN: r217225
This commit is contained in:
parent
a98480ddbb
commit
8ad1c2df74
|
@ -1,3 +1,17 @@
|
|||
2014-11-07 Robert Dewar <dewar@adacore.com>
|
||||
|
||||
* freeze.adb: Code clean up.
|
||||
|
||||
2014-11-07 Yannick Moy <moy@adacore.com>
|
||||
|
||||
* a-cfdlli.ads, a-cfhama.ads, a-cfhase.ads, a-cfinve.ads,
|
||||
* a-cforma.ads, a-cforse.ads, a-cofove.ads: Mark First_To_Previous,
|
||||
Current_To_Last and Strict_Equal as Ghost.
|
||||
|
||||
2014-11-07 Ed Schonberg <schonberg@adacore.com>
|
||||
|
||||
* sem_ch3.adb: Code clean up.
|
||||
|
||||
2014-11-07 Hristian Kirtchev <kirtchev@adacore.com>
|
||||
|
||||
* freeze.adb (Freeze_Entity): Issue an error regardless of the
|
||||
|
|
|
@ -6,7 +6,7 @@
|
|||
-- --
|
||||
-- S p e c --
|
||||
-- --
|
||||
-- Copyright (C) 2004-2013, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 2004-2014, 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 --
|
||||
|
@ -311,6 +311,7 @@ package Ada.Containers.Formal_Doubly_Linked_Lists is
|
|||
end Generic_Sorting;
|
||||
|
||||
function Strict_Equal (Left, Right : List) return Boolean with
|
||||
Ghost,
|
||||
Global => null;
|
||||
-- Strict_Equal returns True if the containers are physically equal, i.e.
|
||||
-- they are structurally equal (function "=" returns True) and that they
|
||||
|
@ -318,10 +319,13 @@ package Ada.Containers.Formal_Doubly_Linked_Lists is
|
|||
|
||||
function First_To_Previous (Container : List; Current : Cursor) return List
|
||||
with
|
||||
Ghost,
|
||||
Global => null,
|
||||
Pre => Has_Element (Container, Current) or else Current = No_Element;
|
||||
|
||||
function Current_To_Last (Container : List; Current : Cursor) return List
|
||||
with
|
||||
Ghost,
|
||||
Global => null,
|
||||
Pre => Has_Element (Container, Current) or else Current = No_Element;
|
||||
-- First_To_Previous returns a container containing all elements preceding
|
||||
|
|
|
@ -242,6 +242,7 @@ package Ada.Containers.Formal_Hashed_Maps is
|
|||
Global => null;
|
||||
|
||||
function Strict_Equal (Left, Right : Map) return Boolean with
|
||||
Ghost,
|
||||
Global => null;
|
||||
-- Strict_Equal returns True if the containers are physically equal, i.e.
|
||||
-- they are structurally equal (function "=" returns True) and that they
|
||||
|
@ -249,10 +250,13 @@ package Ada.Containers.Formal_Hashed_Maps is
|
|||
|
||||
function First_To_Previous (Container : Map; Current : Cursor) return Map
|
||||
with
|
||||
Ghost,
|
||||
Global => null,
|
||||
Pre => Has_Element (Container, Current) or else Current = No_Element;
|
||||
|
||||
function Current_To_Last (Container : Map; Current : Cursor) return Map
|
||||
with
|
||||
Ghost,
|
||||
Global => null,
|
||||
Pre => Has_Element (Container, Current) or else Current = No_Element;
|
||||
-- First_To_Previous returns a container containing all elements preceding
|
||||
|
|
|
@ -309,6 +309,7 @@ package Ada.Containers.Formal_Hashed_Sets is
|
|||
end Generic_Keys;
|
||||
|
||||
function Strict_Equal (Left, Right : Set) return Boolean with
|
||||
Ghost,
|
||||
Global => null;
|
||||
-- Strict_Equal returns True if the containers are physically equal, i.e.
|
||||
-- they are structurally equal (function "=" returns True) and that they
|
||||
|
@ -316,10 +317,13 @@ package Ada.Containers.Formal_Hashed_Sets is
|
|||
|
||||
function First_To_Previous (Container : Set; Current : Cursor) return Set
|
||||
with
|
||||
Ghost,
|
||||
Global => null,
|
||||
Pre => Has_Element (Container, Current) or else Current = No_Element;
|
||||
|
||||
function Current_To_Last (Container : Set; Current : Cursor) return Set
|
||||
with
|
||||
Ghost,
|
||||
Global => null,
|
||||
Pre => Has_Element (Container, Current) or else Current = No_Element;
|
||||
-- First_To_Previous returns a container containing all elements preceding
|
||||
|
|
|
@ -209,11 +209,14 @@ package Ada.Containers.Formal_Indefinite_Vectors is
|
|||
(Container : Vector;
|
||||
Current : Index_Type) return Vector
|
||||
with
|
||||
Ghost,
|
||||
Global => null;
|
||||
|
||||
function Current_To_Last
|
||||
(Container : Vector;
|
||||
Current : Index_Type) return Vector
|
||||
with
|
||||
Ghost,
|
||||
Global => null;
|
||||
|
||||
private
|
||||
|
|
|
@ -243,6 +243,7 @@ package Ada.Containers.Formal_Ordered_Maps is
|
|||
Global => null;
|
||||
|
||||
function Strict_Equal (Left, Right : Map) return Boolean with
|
||||
Ghost,
|
||||
Global => null;
|
||||
-- Strict_Equal returns True if the containers are physically equal, i.e.
|
||||
-- they are structurally equal (function "=" returns True) and that they
|
||||
|
@ -250,10 +251,13 @@ package Ada.Containers.Formal_Ordered_Maps is
|
|||
|
||||
function First_To_Previous (Container : Map; Current : Cursor) return Map
|
||||
with
|
||||
Ghost,
|
||||
Global => null,
|
||||
Pre => Has_Element (Container, Current) or else Current = No_Element;
|
||||
|
||||
function Current_To_Last (Container : Map; Current : Cursor) return Map
|
||||
with
|
||||
Ghost,
|
||||
Global => null,
|
||||
Pre => Has_Element (Container, Current) or else Current = No_Element;
|
||||
-- First_To_Previous returns a container containing all elements preceding
|
||||
|
|
|
@ -327,17 +327,21 @@ package Ada.Containers.Formal_Ordered_Sets is
|
|||
end Generic_Keys;
|
||||
|
||||
function Strict_Equal (Left, Right : Set) return Boolean with
|
||||
Global => null;
|
||||
Ghost,
|
||||
Global => null;
|
||||
-- Strict_Equal returns True if the containers are physically equal, i.e.
|
||||
-- they are structurally equal (function "=" returns True) and that they
|
||||
-- have the same set of cursors.
|
||||
|
||||
function First_To_Previous (Container : Set; Current : Cursor) return Set
|
||||
with
|
||||
Ghost,
|
||||
Global => null,
|
||||
Pre => Has_Element (Container, Current) or else Current = No_Element;
|
||||
|
||||
function Current_To_Last (Container : Set; Current : Cursor) return Set
|
||||
with
|
||||
Ghost,
|
||||
Global => null,
|
||||
Pre => Has_Element (Container, Current) or else Current = No_Element;
|
||||
-- First_To_Previous returns a container containing all elements preceding
|
||||
|
|
|
@ -212,11 +212,14 @@ package Ada.Containers.Formal_Vectors is
|
|||
(Container : Vector;
|
||||
Current : Index_Type) return Vector
|
||||
with
|
||||
Ghost,
|
||||
Global => null;
|
||||
|
||||
function Current_To_Last
|
||||
(Container : Vector;
|
||||
Current : Index_Type) return Vector
|
||||
with
|
||||
Ghost,
|
||||
Global => null;
|
||||
-- First_To_Previous returns a container containing all elements preceding
|
||||
-- Current (excluded) in Container. Current_To_Last returns a container
|
||||
|
|
|
@ -2398,24 +2398,6 @@ package body Freeze is
|
|||
Set_Has_Non_Standard_Rep (Base_Type (Arr), True);
|
||||
Set_Is_Bit_Packed_Array (Base_Type (Arr), True);
|
||||
Set_Is_Packed (Base_Type (Arr), True);
|
||||
|
||||
-- Make sure that we have the necessary routines to
|
||||
-- implement the packing, and complain now if not.
|
||||
|
||||
declare
|
||||
CS : constant Int := UI_To_Int (Csiz);
|
||||
RE : constant RE_Id := Get_Id (CS);
|
||||
|
||||
begin
|
||||
if RE /= RE_Null
|
||||
and then not RTE_Available (RE)
|
||||
then
|
||||
Error_Msg_CRT
|
||||
("packing of " & UI_Image (Csiz)
|
||||
& "-bit components",
|
||||
First_Subtype (Etype (Arr)));
|
||||
end if;
|
||||
end;
|
||||
end if;
|
||||
end;
|
||||
end if;
|
||||
|
@ -2668,6 +2650,37 @@ package body Freeze is
|
|||
Create_Packed_Array_Impl_Type (Arr);
|
||||
Freeze_And_Append (Packed_Array_Impl_Type (Arr), N, Result);
|
||||
|
||||
-- Make sure that we have the necessary routines to implement the
|
||||
-- packing, and complain now if not. Note that we only test this
|
||||
-- for constrained array types.
|
||||
|
||||
if Is_Constrained (Arr)
|
||||
and then Is_Bit_Packed_Array (Arr)
|
||||
and then Present (Packed_Array_Impl_Type (Arr))
|
||||
and then Is_Array_Type (Packed_Array_Impl_Type (Arr))
|
||||
then
|
||||
declare
|
||||
CS : constant Uint := Component_Size (Arr);
|
||||
RE : constant RE_Id := Get_Id (UI_To_Int (CS));
|
||||
|
||||
begin
|
||||
if RE /= RE_Null
|
||||
and then not RTE_Available (RE)
|
||||
then
|
||||
Error_Msg_CRT
|
||||
("packing of " & UI_Image (CS) & "-bit components",
|
||||
First_Subtype (Etype (Arr)));
|
||||
|
||||
-- Cancel the packing
|
||||
|
||||
Set_Is_Packed (Base_Type (Arr), False);
|
||||
Set_Is_Bit_Packed_Array (Base_Type (Arr), False);
|
||||
Set_Packed_Array_Impl_Type (Arr, Empty);
|
||||
goto Skip_Packed;
|
||||
end if;
|
||||
end;
|
||||
end if;
|
||||
|
||||
-- Size information of packed array type is copied to the array
|
||||
-- type, since this is really the representation. But do not
|
||||
-- override explicit existing size values. If the ancestor subtype
|
||||
|
@ -2689,6 +2702,8 @@ package body Freeze is
|
|||
end if;
|
||||
end if;
|
||||
|
||||
<<Skip_Packed>>
|
||||
|
||||
-- For non-packed arrays set the alignment of the array to the
|
||||
-- alignment of the component type if it is unknown. Skip this
|
||||
-- in atomic case (atomic arrays may need larger alignments).
|
||||
|
|
|
@ -11697,12 +11697,13 @@ package body Sem_Ch3 is
|
|||
Item := First_Rep_Item (Full);
|
||||
|
||||
-- If no existing rep items on full type, we can just link directly
|
||||
-- to the list of items on the private type. Same if the rep items
|
||||
-- are only those inherited from the base
|
||||
-- to the list of items on the private type, if any exist.. Same if
|
||||
-- the rep items are only those inherited from the base
|
||||
|
||||
if No (Item)
|
||||
or else Nkind (Item) /= N_Aspect_Specification
|
||||
or else Entity (Item) = Full_Base
|
||||
if (No (Item)
|
||||
or else Nkind (Item) /= N_Aspect_Specification
|
||||
or else Entity (Item) = Full_Base)
|
||||
and then Present (First_Rep_Item (Priv))
|
||||
then
|
||||
Set_First_Rep_Item (Full, First_Rep_Item (Priv));
|
||||
|
||||
|
|
Loading…
Reference in New Issue