This patch implements the latest version of invariants, in which the
aspect is called Type_Invariant, the old name Invariant is retained
as an implementation-specific aspect. A general mechanism for dealing
with synonyms is also implemented (so that e.g. you cannot specify
both Invariant and Type_Invariant for the same entity). Synonyms
Precondition and Postcondition have been added for Pre and Post
aspects. The names of pragmas are not affected.
The first test shows synonym checking in effect (compiled with
-gnatj60ld7 -gnata12)
1. package sameaspect is
2. type R1 is new Integer with
3. Atomic => True,
4. Shared => True;
|
>>> aspect "shared" for "R1" previously given at
line 3
5.
6. type R2 is private with
7. Invariant => True,
8. Type_Invariant => False;
|
>>> aspect "type_invariant" for "R2" previously
given at line 7
9.
10. private
11. type R2 is new Integer;
12. end sameaspect;
The second test shows the new aspect name Type_Invariant
being properly recognized (compiles clean with above
switches and executes silently).
1. with Ada.Assertions; use Ada.Assertions;
2. procedure typeinvariant is
3. package P is
4. type R is private with
5. Type_Invariant => False;
6. private
7. type R is record
8. X : Integer := 3;
9. end record;
10. end;
11.
12. begin
13. declare
14. V : P.R;
15. begin
16. raise Program_Error;
17. end;
18.
19. exception
20. when Assertion_Error =>
21. null;
22. end;
Tested on x86_64-pc-linux-gnu, committed on trunk
2011-08-01 Robert Dewar <de...@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.
Index: aspects.adb
===================================================================
--- aspects.adb (revision 177009)
+++ aspects.adb (working copy)
@@ -72,8 +72,8 @@
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),
@@ -95,7 +95,9 @@
(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),
@@ -108,6 +110,7 @@
(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),
@@ -217,6 +220,70 @@
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 --
-------------------------------
Index: aspects.ads
===================================================================
--- aspects.ads (revision 177009)
+++ aspects.ads (working copy)
@@ -55,7 +55,9 @@
Aspect_Object_Size, -- GNAT
Aspect_Output,
Aspect_Post,
+ Aspect_Postcondition,
Aspect_Pre,
+ Aspect_Precondition,
Aspect_Predicate, -- GNAT
Aspect_Read,
Aspect_Size,
@@ -64,6 +66,7 @@
Aspect_Storage_Size,
Aspect_Stream_Size,
Aspect_Suppress,
+ Aspect_Type_Invariant,
Aspect_Unsuppress,
Aspect_Value_Size, -- GNAT
Aspect_Warnings,
@@ -125,33 +128,36 @@
-- 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);
@@ -207,6 +213,11 @@
-- 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
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb (revision 177010)
+++ sem_ch13.adb (working copy)
@@ -753,7 +753,7 @@
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;
@@ -932,11 +932,15 @@
-- 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;
@@ -1020,7 +1024,8 @@
-- 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
@@ -1113,7 +1118,11 @@
-- 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
@@ -5131,9 +5140,12 @@
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;
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl (revision 177009)
+++ snames.ads-tmpl (working copy)
@@ -141,6 +141,7 @@
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
