OpenE2K
/
gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

aspects.ads, [...]: Add aspect Type_Invariant, Precondition, Postcondition. 

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.

From-SVN: r177011
This commit is contained in:
Robert Dewar 2011-08-01 10:44:02 +00:00 committed by Arnaud Charlet
parent bd949ee2a3
commit 857ade1b5a
5 changed files with 135 additions and 35 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
gcc/ada/ChangeLog
View File

@ -1,3 +1,12 @@
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

71
gcc/ada/aspects.adb
View File

@ -72,8 +72,8 @@ package body Aspects is
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 @@ package body Aspects is
(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 @@ package body Aspects is
(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 @@ package body Aspects is
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 --
-------------------------------

65
gcc/ada/aspects.ads
View File

@ -55,7 +55,9 @@ package Aspects is
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 @@ package Aspects is
Aspect_Storage_Size,
Aspect_Stream_Size,
Aspect_Suppress,
Aspect_Type_Invariant,
Aspect_Unsuppress,
Aspect_Value_Size, -- GNAT
Aspect_Warnings,
@ -125,33 +128,36 @@ package Aspects is
-- 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 @@ package Aspects is
-- 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

24
gcc/ada/sem_ch13.adb
View File

@ -753,7 +753,7 @@ package body Sem_Ch13 is
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 @@ package body Sem_Ch13 is
-- 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 @@ package body Sem_Ch13 is
-- 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 @@ package body Sem_Ch13 is
-- 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 @@ package body Sem_Ch13 is
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;

1
gcc/ada/snames.ads-tmpl
View File

@ -141,6 +141,7 @@ package Snames is
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