-- --
-- S p e c --
-- --
--- Copyright (C) 2010-2013, Free Software Foundation, Inc. --
+-- Copyright (C) 2010-2015, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- and fully analyzed (possibly with expansion) during the semantic
-- analysis of subprogram bodies.
-with Namet; use Namet;
-with Snames; use Snames;
-with Types; use Types;
+with Namet; use Namet;
+with Snames; use Snames;
+with Types; use Types;
package Aspects is
Aspect_Abstract_State, -- GNAT
Aspect_Address,
Aspect_Alignment,
+ Aspect_Annotate, -- GNAT
Aspect_Attach_Handler,
Aspect_Bit_Order,
Aspect_Component_Size,
Aspect_Convention,
Aspect_CPU,
Aspect_Default_Component_Value,
+ Aspect_Default_Initial_Condition, -- GNAT
Aspect_Default_Iterator,
+ Aspect_Default_Storage_Pool,
Aspect_Default_Value,
Aspect_Depends, -- GNAT
Aspect_Dimension, -- GNAT
Aspect_Dimension_System, -- GNAT
Aspect_Dispatching_Domain,
Aspect_Dynamic_Predicate,
+ Aspect_Extensions_Visible, -- GNAT
Aspect_External_Name,
Aspect_External_Tag,
+ Aspect_Ghost, -- GNAT
Aspect_Global, -- GNAT
Aspect_Implicit_Dereference,
Aspect_Initial_Condition, -- GNAT
Aspect_Linker_Section, -- GNAT
Aspect_Machine_Radix,
Aspect_Object_Size, -- GNAT
+ Aspect_Obsolescent, -- GNAT
Aspect_Output,
Aspect_Part_Of, -- GNAT
Aspect_Post,
Aspect_Synchronization,
Aspect_Test_Case, -- GNAT
Aspect_Type_Invariant,
+ Aspect_Unimplemented, -- GNAT
Aspect_Unsuppress,
Aspect_Value_Size, -- GNAT
Aspect_Variable_Indexing,
-- The following aspects correspond to library unit pragmas
Aspect_All_Calls_Remote,
- Aspect_Compiler_Unit, -- GNAT
Aspect_Elaborate_Body,
+ Aspect_No_Elaboration_Code_All, -- GNAT
Aspect_Preelaborate,
Aspect_Pure,
Aspect_Remote_Call_Interface,
Aspect_Inline,
Aspect_Inline_Always, -- GNAT
Aspect_Interrupt_Handler,
+ Aspect_Lock_Free, -- GNAT
Aspect_No_Return,
+ Aspect_No_Tagged_Streams, -- GNAT
Aspect_Pack,
Aspect_Persistent_BSS, -- GNAT
Aspect_Preelaborable_Initialization,
Aspect_Shared, -- GNAT (equivalent to Atomic)
Aspect_Simple_Storage_Pool_Type, -- GNAT
Aspect_Suppress_Debug_Info, -- GNAT
+ Aspect_Suppress_Initialization, -- GNAT
+ Aspect_Thread_Local_Storage, -- GNAT
Aspect_Unchecked_Union,
Aspect_Universal_Aliasing, -- GNAT
Aspect_Unmodified, -- GNAT
Aspect_Unreferenced_Objects, -- GNAT
Aspect_Volatile,
Aspect_Volatile_Components,
-
- -- Aspects that have a static boolean value but don't correspond to
- -- pragmas
-
- Aspect_Lock_Free); -- GNAT
+ Aspect_Volatile_Full_Access); -- GNAT
subtype Aspect_Id_Exclude_No_Aspect is
Aspect_Id range Aspect_Id'Succ (No_Aspect) .. Aspect_Id'Last;
-- The following array indicates aspects that accept 'Class
Class_Aspect_OK : constant array (Aspect_Id) of Boolean :=
- (Aspect_Invariant => True,
+ (Aspect_Input => True,
+ Aspect_Invariant => True,
+ Aspect_Output => True,
Aspect_Pre => True,
Aspect_Predicate => True,
Aspect_Post => True,
+ Aspect_Read => True,
+ Aspect_Write => True,
Aspect_Type_Invariant => True,
others => False);
Implementation_Defined_Aspect : constant array (Aspect_Id) of Boolean :=
(Aspect_Abstract_State => True,
+ Aspect_Annotate => True,
Aspect_Async_Readers => True,
Aspect_Async_Writers => True,
- Aspect_Compiler_Unit => True,
Aspect_Contract_Cases => True,
Aspect_Depends => True,
Aspect_Dimension => True,
Aspect_Dimension_System => True,
Aspect_Effective_Reads => True,
Aspect_Effective_Writes => True,
+ Aspect_Extensions_Visible => True,
Aspect_Favor_Top_Level => True,
+ Aspect_Ghost => True,
Aspect_Global => True,
Aspect_Inline_Always => True,
Aspect_Invariant => True,
Aspect_Simple_Storage_Pool => True,
Aspect_Simple_Storage_Pool_Type => True,
Aspect_Suppress_Debug_Info => True,
+ Aspect_Suppress_Initialization => True,
+ Aspect_Thread_Local_Storage => True,
Aspect_Test_Case => True,
Aspect_Universal_Aliasing => True,
Aspect_Universal_Data => True,
-- the same aspect attached to the same declaration are allowed.
No_Duplicates_Allowed : constant array (Aspect_Id) of Boolean :=
- (Aspect_Test_Case => False,
+ (Aspect_Annotate => False,
+ Aspect_Test_Case => False,
others => True);
-- The following subtype defines aspects corresponding to library unit
-- The following array indicates what argument type is required
Aspect_Argument : constant array (Aspect_Id) of Aspect_Expression :=
- (No_Aspect => Optional_Expression,
- Aspect_Abstract_State => Expression,
- Aspect_Address => Expression,
- Aspect_Alignment => Expression,
- Aspect_Attach_Handler => Expression,
- Aspect_Bit_Order => Expression,
- Aspect_Component_Size => Expression,
- Aspect_Constant_Indexing => Name,
- Aspect_Contract_Cases => Expression,
- Aspect_Convention => Name,
- Aspect_CPU => Expression,
- Aspect_Default_Component_Value => Expression,
- Aspect_Default_Iterator => Name,
- Aspect_Default_Value => Expression,
- Aspect_Depends => Expression,
- Aspect_Dimension => Expression,
- Aspect_Dimension_System => Expression,
- Aspect_Dispatching_Domain => Expression,
- Aspect_Dynamic_Predicate => Expression,
- Aspect_External_Name => Expression,
- Aspect_External_Tag => Expression,
- Aspect_Global => Expression,
- Aspect_Implicit_Dereference => Name,
- Aspect_Initial_Condition => Expression,
- Aspect_Initializes => Expression,
- Aspect_Input => Name,
- Aspect_Interrupt_Priority => Expression,
- Aspect_Invariant => Expression,
- Aspect_Iterable => Expression,
- Aspect_Iterator_Element => Name,
- Aspect_Link_Name => Expression,
- Aspect_Linker_Section => Expression,
- Aspect_Machine_Radix => Expression,
- Aspect_Object_Size => Expression,
- Aspect_Output => Name,
- Aspect_Part_Of => Expression,
- Aspect_Post => Expression,
- Aspect_Postcondition => Expression,
- Aspect_Pre => Expression,
- Aspect_Precondition => Expression,
- Aspect_Predicate => Expression,
- Aspect_Priority => Expression,
- Aspect_Read => Name,
- Aspect_Refined_Depends => Expression,
- Aspect_Refined_Global => Expression,
- Aspect_Refined_Post => Expression,
- Aspect_Refined_State => Expression,
- Aspect_Relative_Deadline => Expression,
- Aspect_Scalar_Storage_Order => Expression,
- Aspect_Simple_Storage_Pool => Name,
- Aspect_Size => Expression,
- Aspect_Small => Expression,
- Aspect_SPARK_Mode => Optional_Name,
- Aspect_Static_Predicate => Expression,
- Aspect_Storage_Pool => Name,
- Aspect_Storage_Size => Expression,
- Aspect_Stream_Size => Expression,
- Aspect_Suppress => Name,
- Aspect_Synchronization => Name,
- Aspect_Test_Case => Expression,
- Aspect_Type_Invariant => Expression,
- Aspect_Unsuppress => Name,
- Aspect_Value_Size => Expression,
- Aspect_Variable_Indexing => Name,
- Aspect_Warnings => Name,
- Aspect_Write => Name,
-
- Boolean_Aspects => Optional_Expression,
- Library_Unit_Aspects => Optional_Expression);
+ (No_Aspect => Optional_Expression,
+ Aspect_Abstract_State => Expression,
+ Aspect_Address => Expression,
+ Aspect_Alignment => Expression,
+ Aspect_Annotate => Expression,
+ Aspect_Attach_Handler => Expression,
+ Aspect_Bit_Order => Expression,
+ Aspect_Component_Size => Expression,
+ Aspect_Constant_Indexing => Name,
+ Aspect_Contract_Cases => Expression,
+ Aspect_Convention => Name,
+ Aspect_CPU => Expression,
+ Aspect_Default_Component_Value => Expression,
+ Aspect_Default_Initial_Condition => Optional_Expression,
+ Aspect_Default_Iterator => Name,
+ Aspect_Default_Storage_Pool => Expression,
+ Aspect_Default_Value => Expression,
+ Aspect_Depends => Expression,
+ Aspect_Dimension => Expression,
+ Aspect_Dimension_System => Expression,
+ Aspect_Dispatching_Domain => Expression,
+ Aspect_Dynamic_Predicate => Expression,
+ Aspect_Extensions_Visible => Optional_Expression,
+ Aspect_External_Name => Expression,
+ Aspect_External_Tag => Expression,
+ Aspect_Ghost => Optional_Expression,
+ Aspect_Global => Expression,
+ Aspect_Implicit_Dereference => Name,
+ Aspect_Initial_Condition => Expression,
+ Aspect_Initializes => Expression,
+ Aspect_Input => Name,
+ Aspect_Interrupt_Priority => Expression,
+ Aspect_Invariant => Expression,
+ Aspect_Iterable => Expression,
+ Aspect_Iterator_Element => Name,
+ Aspect_Link_Name => Expression,
+ Aspect_Linker_Section => Expression,
+ Aspect_Machine_Radix => Expression,
+ Aspect_Object_Size => Expression,
+ Aspect_Obsolescent => Optional_Expression,
+ Aspect_Output => Name,
+ Aspect_Part_Of => Expression,
+ Aspect_Post => Expression,
+ Aspect_Postcondition => Expression,
+ Aspect_Pre => Expression,
+ Aspect_Precondition => Expression,
+ Aspect_Predicate => Expression,
+ Aspect_Priority => Expression,
+ Aspect_Read => Name,
+ Aspect_Refined_Depends => Expression,
+ Aspect_Refined_Global => Expression,
+ Aspect_Refined_Post => Expression,
+ Aspect_Refined_State => Expression,
+ Aspect_Relative_Deadline => Expression,
+ Aspect_Scalar_Storage_Order => Expression,
+ Aspect_Simple_Storage_Pool => Name,
+ Aspect_Size => Expression,
+ Aspect_Small => Expression,
+ Aspect_SPARK_Mode => Optional_Name,
+ Aspect_Static_Predicate => Expression,
+ Aspect_Storage_Pool => Name,
+ Aspect_Storage_Size => Expression,
+ Aspect_Stream_Size => Expression,
+ Aspect_Suppress => Name,
+ Aspect_Synchronization => Name,
+ Aspect_Test_Case => Expression,
+ Aspect_Type_Invariant => Expression,
+ Aspect_Unimplemented => Optional_Expression,
+ Aspect_Unsuppress => Name,
+ Aspect_Value_Size => Expression,
+ Aspect_Variable_Indexing => Name,
+ Aspect_Warnings => Name,
+ Aspect_Write => Name,
+
+ Boolean_Aspects => Optional_Expression,
+ Library_Unit_Aspects => Optional_Expression);
-----------------------------------------
-- Table Linking Names and Aspect_Id's --
Aspect_Address => Name_Address,
Aspect_Alignment => Name_Alignment,
Aspect_All_Calls_Remote => Name_All_Calls_Remote,
+ Aspect_Annotate => Name_Annotate,
Aspect_Async_Readers => Name_Async_Readers,
Aspect_Async_Writers => Name_Async_Writers,
Aspect_Asynchronous => Name_Asynchronous,
Aspect_Atomic_Components => Name_Atomic_Components,
Aspect_Attach_Handler => Name_Attach_Handler,
Aspect_Bit_Order => Name_Bit_Order,
- Aspect_Compiler_Unit => Name_Compiler_Unit,
Aspect_Component_Size => Name_Component_Size,
Aspect_Constant_Indexing => Name_Constant_Indexing,
Aspect_Contract_Cases => Name_Contract_Cases,
Aspect_Convention => Name_Convention,
Aspect_CPU => Name_CPU,
+ Aspect_Default_Component_Value => Name_Default_Component_Value,
+ Aspect_Default_Initial_Condition => Name_Default_Initial_Condition,
Aspect_Default_Iterator => Name_Default_Iterator,
+ Aspect_Default_Storage_Pool => Name_Default_Storage_Pool,
Aspect_Default_Value => Name_Default_Value,
- Aspect_Default_Component_Value => Name_Default_Component_Value,
Aspect_Depends => Name_Depends,
Aspect_Dimension => Name_Dimension,
Aspect_Dimension_System => Name_Dimension_System,
Aspect_Effective_Reads => Name_Effective_Reads,
Aspect_Effective_Writes => Name_Effective_Writes,
Aspect_Elaborate_Body => Name_Elaborate_Body,
+ Aspect_Export => Name_Export,
+ Aspect_Extensions_Visible => Name_Extensions_Visible,
Aspect_External_Name => Name_External_Name,
Aspect_External_Tag => Name_External_Tag,
- Aspect_Export => Name_Export,
Aspect_Favor_Top_Level => Name_Favor_Top_Level,
+ Aspect_Ghost => Name_Ghost,
Aspect_Global => Name_Global,
Aspect_Implicit_Dereference => Name_Implicit_Dereference,
Aspect_Import => Name_Import,
Aspect_Linker_Section => Name_Linker_Section,
Aspect_Lock_Free => Name_Lock_Free,
Aspect_Machine_Radix => Name_Machine_Radix,
+ Aspect_No_Elaboration_Code_All => Name_No_Elaboration_Code_All,
Aspect_No_Return => Name_No_Return,
+ Aspect_No_Tagged_Streams => Name_No_Tagged_Streams,
Aspect_Object_Size => Name_Object_Size,
+ Aspect_Obsolescent => Name_Obsolescent,
Aspect_Output => Name_Output,
Aspect_Pack => Name_Pack,
Aspect_Part_Of => Name_Part_Of,
Aspect_Stream_Size => Name_Stream_Size,
Aspect_Suppress => Name_Suppress,
Aspect_Suppress_Debug_Info => Name_Suppress_Debug_Info,
+ Aspect_Suppress_Initialization => Name_Suppress_Initialization,
+ Aspect_Thread_Local_Storage => Name_Thread_Local_Storage,
Aspect_Synchronization => Name_Synchronization,
Aspect_Test_Case => Name_Test_Case,
Aspect_Type_Invariant => Name_Type_Invariant,
Aspect_Unchecked_Union => Name_Unchecked_Union,
+ Aspect_Unimplemented => Name_Unimplemented,
Aspect_Universal_Aliasing => Name_Universal_Aliasing,
Aspect_Universal_Data => Name_Universal_Data,
Aspect_Unmodified => Name_Unmodified,
Aspect_Variable_Indexing => Name_Variable_Indexing,
Aspect_Volatile => Name_Volatile,
Aspect_Volatile_Components => Name_Volatile_Components,
+ Aspect_Volatile_Full_Access => Name_Volatile_Full_Access,
Aspect_Warnings => Name_Warnings,
Aspect_Write => Name_Write);
-- information from the parent type, which must be frozen at that point
-- (since freezing the derived type first freezes the parent type).
+ -- SPARK 2014 aspects do not follow the general delay mechanism as they
+ -- act as annotations and cannot modify the attributes of their related
+ -- constructs. To handle forward references in such aspects, the compiler
+ -- delays the analysis of their respective pragmas by collecting them in
+ -- N_Contract nodes. The pragmas are then analyzed at the end of the
+ -- declarative region which contains the related construct. For details,
+ -- see routines Analyze_xxx_In_Decl_Part.
+
-- The following shows which aspects are delayed. There are three cases:
type Delay_Type is
(No_Aspect => Always_Delay,
Aspect_Address => Always_Delay,
Aspect_All_Calls_Remote => Always_Delay,
- Aspect_Async_Readers => Always_Delay,
- Aspect_Async_Writers => Always_Delay,
Aspect_Asynchronous => Always_Delay,
Aspect_Attach_Handler => Always_Delay,
- Aspect_Compiler_Unit => Always_Delay,
Aspect_Constant_Indexing => Always_Delay,
- Aspect_Contract_Cases => Always_Delay,
Aspect_CPU => Always_Delay,
Aspect_Default_Iterator => Always_Delay,
+ Aspect_Default_Storage_Pool => Always_Delay,
Aspect_Default_Value => Always_Delay,
Aspect_Default_Component_Value => Always_Delay,
- Aspect_Depends => Always_Delay,
Aspect_Discard_Names => Always_Delay,
Aspect_Dispatching_Domain => Always_Delay,
Aspect_Dynamic_Predicate => Always_Delay,
- Aspect_Effective_Reads => Always_Delay,
- Aspect_Effective_Writes => Always_Delay,
Aspect_Elaborate_Body => Always_Delay,
+ Aspect_Export => Always_Delay,
Aspect_External_Name => Always_Delay,
Aspect_External_Tag => Always_Delay,
- Aspect_Export => Always_Delay,
Aspect_Favor_Top_Level => Always_Delay,
- Aspect_Global => Always_Delay,
Aspect_Implicit_Dereference => Always_Delay,
Aspect_Import => Always_Delay,
Aspect_Independent => Always_Delay,
Aspect_Independent_Components => Always_Delay,
Aspect_Inline => Always_Delay,
Aspect_Inline_Always => Always_Delay,
- Aspect_Initial_Condition => Always_Delay,
- Aspect_Initializes => Always_Delay,
Aspect_Input => Always_Delay,
Aspect_Interrupt_Handler => Always_Delay,
Aspect_Interrupt_Priority => Always_Delay,
Aspect_Pure => Always_Delay,
Aspect_Pure_Function => Always_Delay,
Aspect_Read => Always_Delay,
- Aspect_Refined_Depends => Always_Delay,
- Aspect_Refined_Global => Always_Delay,
- Aspect_Refined_State => Always_Delay,
Aspect_Relative_Deadline => Always_Delay,
Aspect_Remote_Access_Type => Always_Delay,
Aspect_Remote_Call_Interface => Always_Delay,
Aspect_Stream_Size => Always_Delay,
Aspect_Suppress => Always_Delay,
Aspect_Suppress_Debug_Info => Always_Delay,
+ Aspect_Suppress_Initialization => Always_Delay,
+ Aspect_Thread_Local_Storage => Always_Delay,
Aspect_Type_Invariant => Always_Delay,
Aspect_Unchecked_Union => Always_Delay,
Aspect_Universal_Aliasing => Always_Delay,
Aspect_Write => Always_Delay,
Aspect_Abstract_State => Never_Delay,
+ Aspect_Annotate => Never_Delay,
+ Aspect_Async_Readers => Never_Delay,
+ Aspect_Async_Writers => Never_Delay,
+ Aspect_Contract_Cases => Never_Delay,
Aspect_Convention => Never_Delay,
+ Aspect_Default_Initial_Condition => Never_Delay,
+ Aspect_Depends => Never_Delay,
Aspect_Dimension => Never_Delay,
Aspect_Dimension_System => Never_Delay,
+ Aspect_Effective_Reads => Never_Delay,
+ Aspect_Effective_Writes => Never_Delay,
+ Aspect_Extensions_Visible => Never_Delay,
+ Aspect_Ghost => Never_Delay,
+ Aspect_Global => Never_Delay,
+ Aspect_Initial_Condition => Never_Delay,
+ Aspect_Initializes => Never_Delay,
+ Aspect_No_Elaboration_Code_All => Never_Delay,
+ Aspect_No_Tagged_Streams => Never_Delay,
+ Aspect_Obsolescent => Never_Delay,
Aspect_Part_Of => Never_Delay,
+ Aspect_Refined_Depends => Never_Delay,
+ Aspect_Refined_Global => Never_Delay,
Aspect_Refined_Post => Never_Delay,
+ Aspect_Refined_State => Never_Delay,
Aspect_SPARK_Mode => Never_Delay,
Aspect_Synchronization => Never_Delay,
Aspect_Test_Case => Never_Delay,
+ Aspect_Unimplemented => Never_Delay,
Aspect_Warnings => Never_Delay,
Aspect_Alignment => Rep_Aspect,
Aspect_Storage_Size => Rep_Aspect,
Aspect_Value_Size => Rep_Aspect,
Aspect_Volatile => Rep_Aspect,
- Aspect_Volatile_Components => Rep_Aspect);
+ Aspect_Volatile_Components => Rep_Aspect,
+ Aspect_Volatile_Full_Access => Rep_Aspect);
------------------------------------------------
-- Handling of Aspect Specifications on Stubs --