2011-08-01 Robert Dewar <dewar@adacore.com>
+ * aspects.ads, aspects.adb: Add aspect Type_Invariant, Precondition,
+ Postcondition.
+ (Same_Aspect): New function.
+ * sem_ch13.adb (Analyze_Aspect_Specifications): Add aspect
+ Type_Invariant, Precondition, Postcondition.
+ * snames.ads-tmpl: Add Name_Type_Invariant.
+
+2011-08-01 Robert Dewar <dewar@adacore.com>
+
* freeze.adb (Freeze_Entity): Don't call Check_Aspect_At_Freeze_Point
here.
(Freeze_All_Ent): Fix error in handling inherited aspects.
Asp : Aspect_Id;
end record;
- Aspect_Names : constant array (Integer range <>) of Aspect_Entry := (
- (Name_Ada_2005, Aspect_Ada_2005),
+ Aspect_Names : constant array (Integer range <>) of Aspect_Entry :=
+ ((Name_Ada_2005, Aspect_Ada_2005),
(Name_Ada_2012, Aspect_Ada_2012),
(Name_Address, Aspect_Address),
(Name_Alignment, Aspect_Alignment),
(Name_Pack, Aspect_Pack),
(Name_Persistent_BSS, Aspect_Persistent_BSS),
(Name_Post, Aspect_Post),
+ (Name_Postcondition, Aspect_Postcondition),
(Name_Pre, Aspect_Pre),
+ (Name_Precondition, Aspect_Precondition),
(Name_Predicate, Aspect_Predicate),
(Name_Preelaborable_Initialization, Aspect_Preelaborable_Initialization),
(Name_Pure_Function, Aspect_Pure_Function),
(Name_Stream_Size, Aspect_Stream_Size),
(Name_Suppress, Aspect_Suppress),
(Name_Suppress_Debug_Info, Aspect_Suppress_Debug_Info),
+ (Name_Type_Invariant, Aspect_Type_Invariant),
(Name_Unchecked_Union, Aspect_Unchecked_Union),
(Name_Universal_Aliasing, Aspect_Universal_Aliasing),
(Name_Unmodified, Aspect_Unmodified),
return Has_Aspect_Specifications_Flag (Nkind (N));
end Permits_Aspect_Specifications;
+ -----------------
+ -- Same_Aspect --
+ -----------------
+
+ -- Table used for Same_Aspect, maps aspect to canonical aspect
+
+ Canonical_Aspect : constant array (Aspect_Id) of Aspect_Id := (
+ No_Aspect => No_Aspect,
+ Aspect_Ada_2005 => Aspect_Ada_2005,
+ Aspect_Ada_2012 => Aspect_Ada_2005,
+ Aspect_Address => Aspect_Address,
+ Aspect_Alignment => Aspect_Alignment,
+ Aspect_Atomic => Aspect_Atomic,
+ Aspect_Atomic_Components => Aspect_Atomic_Components,
+ Aspect_Bit_Order => Aspect_Bit_Order,
+ Aspect_Component_Size => Aspect_Component_Size,
+ Aspect_Discard_Names => Aspect_Discard_Names,
+ Aspect_Dynamic_Predicate => Aspect_Predicate,
+ Aspect_External_Tag => Aspect_External_Tag,
+ Aspect_Favor_Top_Level => Aspect_Favor_Top_Level,
+ Aspect_Inline => Aspect_Inline,
+ Aspect_Inline_Always => Aspect_Inline,
+ Aspect_Input => Aspect_Input,
+ Aspect_Invariant => Aspect_Invariant,
+ Aspect_Machine_Radix => Aspect_Machine_Radix,
+ Aspect_No_Return => Aspect_No_Return,
+ Aspect_Object_Size => Aspect_Object_Size,
+ Aspect_Output => Aspect_Output,
+ Aspect_Pack => Aspect_Pack,
+ Aspect_Persistent_BSS => Aspect_Persistent_BSS,
+ Aspect_Post => Aspect_Post,
+ Aspect_Postcondition => Aspect_Post,
+ Aspect_Pre => Aspect_Pre,
+ Aspect_Precondition => Aspect_Pre,
+ Aspect_Predicate => Aspect_Predicate,
+ Aspect_Preelaborable_Initialization => Aspect_Preelaborable_Initialization,
+ Aspect_Pure_Function => Aspect_Pure_Function,
+ Aspect_Read => Aspect_Read,
+ Aspect_Shared => Aspect_Atomic,
+ Aspect_Size => Aspect_Size,
+ Aspect_Static_Predicate => Aspect_Predicate,
+ Aspect_Storage_Pool => Aspect_Storage_Pool,
+ Aspect_Storage_Size => Aspect_Storage_Size,
+ Aspect_Stream_Size => Aspect_Stream_Size,
+ Aspect_Suppress => Aspect_Suppress,
+ Aspect_Suppress_Debug_Info => Aspect_Suppress_Debug_Info,
+ Aspect_Type_Invariant => Aspect_Invariant,
+ Aspect_Unchecked_Union => Aspect_Unchecked_Union,
+ Aspect_Universal_Aliasing => Aspect_Universal_Aliasing,
+ Aspect_Unmodified => Aspect_Unmodified,
+ Aspect_Unreferenced => Aspect_Unreferenced,
+ Aspect_Unreferenced_Objects => Aspect_Unreferenced_Objects,
+ Aspect_Unsuppress => Aspect_Unsuppress,
+ Aspect_Value_Size => Aspect_Value_Size,
+ Aspect_Volatile => Aspect_Volatile,
+ Aspect_Volatile_Components => Aspect_Volatile_Components,
+ Aspect_Warnings => Aspect_Warnings,
+ Aspect_Write => Aspect_Write);
+
+ function Same_Aspect (A1 : Aspect_Id; A2 : Aspect_Id) return Boolean is
+ begin
+ return Canonical_Aspect (A1) = Canonical_Aspect (A2);
+ end Same_Aspect;
+
-------------------------------
-- Set_Aspect_Specifications --
-------------------------------
Aspect_Object_Size, -- GNAT
Aspect_Output,
Aspect_Post,
+ Aspect_Postcondition,
Aspect_Pre,
+ Aspect_Precondition,
Aspect_Predicate, -- GNAT
Aspect_Read,
Aspect_Size,
Aspect_Storage_Size,
Aspect_Stream_Size,
Aspect_Suppress,
+ Aspect_Type_Invariant,
Aspect_Unsuppress,
Aspect_Value_Size, -- GNAT
Aspect_Warnings,
-- The following array indicates what argument type is required
Aspect_Argument : constant array (Aspect_Id) of Aspect_Expression :=
- (No_Aspect => Optional,
- Aspect_Address => Expression,
- Aspect_Alignment => Expression,
- Aspect_Bit_Order => Expression,
- Aspect_Component_Size => Expression,
- Aspect_Dynamic_Predicate => Expression,
- Aspect_External_Tag => Expression,
- Aspect_Input => Name,
- Aspect_Invariant => Expression,
- Aspect_Machine_Radix => Expression,
- Aspect_Object_Size => Expression,
- Aspect_Output => Name,
- Aspect_Post => Expression,
- Aspect_Pre => Expression,
- Aspect_Predicate => Expression,
- Aspect_Read => Name,
- Aspect_Size => Expression,
- Aspect_Static_Predicate => Expression,
- Aspect_Storage_Pool => Name,
- Aspect_Storage_Size => Expression,
- Aspect_Stream_Size => Expression,
- Aspect_Suppress => Name,
- Aspect_Unsuppress => Name,
- Aspect_Value_Size => Expression,
- Aspect_Warnings => Name,
- Aspect_Write => Name,
- Boolean_Aspects => Optional);
+ (No_Aspect => Optional,
+ Aspect_Address => Expression,
+ Aspect_Alignment => Expression,
+ Aspect_Bit_Order => Expression,
+ Aspect_Component_Size => Expression,
+ Aspect_Dynamic_Predicate => Expression,
+ Aspect_External_Tag => Expression,
+ Aspect_Input => Name,
+ Aspect_Invariant => Expression,
+ Aspect_Machine_Radix => Expression,
+ Aspect_Object_Size => Expression,
+ Aspect_Output => Name,
+ Aspect_Post => Expression,
+ Aspect_Postcondition => Expression,
+ Aspect_Pre => Expression,
+ Aspect_Precondition => Expression,
+ Aspect_Predicate => Expression,
+ Aspect_Read => Name,
+ Aspect_Size => Expression,
+ Aspect_Static_Predicate => Expression,
+ Aspect_Storage_Pool => Name,
+ Aspect_Storage_Size => Expression,
+ Aspect_Stream_Size => Expression,
+ Aspect_Suppress => Name,
+ Aspect_Type_Invariant => Expression,
+ Aspect_Unsuppress => Name,
+ Aspect_Value_Size => Expression,
+ Aspect_Warnings => Name,
+ Aspect_Write => Name,
+ Boolean_Aspects => Optional);
function Get_Aspect_Id (Name : Name_Id) return Aspect_Id;
pragma Inline (Get_Aspect_Id);
-- Otherwise the aspects are moved and on return Has_Aspects (To) is True,
-- and Has_Aspects (From) is False.
+ function Same_Aspect (A1 : Aspect_Id; A2 : Aspect_Id) return Boolean;
+ -- Returns True if A1 and A2 are (essentially) the same aspect. This is not
+ -- a simple equality test because e.g. Post and Postcondition are the same.
+ -- This is used for detecting duplicate aspects.
+
procedure Tree_Write;
-- Writes contents of Aspect_Specifications hash table to the tree file
Anod := First (L);
while Anod /= Aspect loop
- if Nam = Chars (Identifier (Anod))
+ if Same_Aspect (A_Id, Get_Aspect_Id (Chars (Identifier (Anod))))
and then Comes_From_Source (Aspect)
then
Error_Msg_Name_1 := Nam;
-- required pragma placement. The processing for the pragmas
-- takes care of the required delay.
- when Aspect_Pre | Aspect_Post => declare
+ when Aspect_Pre |
+ Aspect_Precondition |
+ Aspect_Post |
+ Aspect_Postcondition =>
+ declare
Pname : Name_Id;
begin
- if A_Id = Aspect_Pre then
+ if A_Id = Aspect_Pre or else A_Id = Aspect_Precondition then
Pname := Name_Precondition;
else
Pname := Name_Postcondition;
-- get the required pragma placement. The pragma processing
-- takes care of the required delay.
- when Aspect_Invariant =>
+ when Aspect_Invariant |
+ Aspect_Type_Invariant =>
-- Construct the pragma
-- For Pre/Post cases, insert immediately after the entity
-- declaration, since that is the required pragma placement.
- if A_Id = Aspect_Pre or else A_Id = Aspect_Post then
+ if A_Id = Aspect_Pre or else
+ A_Id = Aspect_Post or else
+ A_Id = Aspect_Precondition or else
+ A_Id = Aspect_Postcondition
+ then
Insert_After (N, Aitem);
-- For all other cases, insert in sequence
when Aspect_Dynamic_Predicate |
Aspect_Invariant |
Aspect_Pre |
+ Aspect_Precondition |
Aspect_Post |
+ Aspect_Postcondition |
Aspect_Predicate |
- Aspect_Static_Predicate =>
+ Aspect_Static_Predicate |
+ Aspect_Type_Invariant =>
T := Standard_Boolean;
end case;
Name_Post : constant Name_Id := N + $;
Name_Pre : constant Name_Id := N + $;
Name_Static_Predicate : constant Name_Id := N + $;
+ Name_Type_Invariant : constant Name_Id := N + $;
-- Some special names used by the expander. Note that the lower case u's
-- at the start of these names get translated to extra underscores. These
OSDN Git Service
