@@ -72,14 +72,10 @@ package Aspects is
Aspect_Address,
Aspect_Aggregate,
Aspect_Alignment,
- Aspect_Always_Terminates, -- GNAT
Aspect_Annotate, -- GNAT
- Aspect_Async_Readers, -- GNAT
- Aspect_Async_Writers, -- GNAT
Aspect_Attach_Handler,
Aspect_Bit_Order,
Aspect_Component_Size,
- Aspect_Constant_After_Elaboration, -- GNAT
Aspect_Constant_Indexing,
Aspect_Contract_Cases, -- GNAT
Aspect_Convention,
@@ -95,13 +91,9 @@ package Aspects is
Aspect_Dimension_System, -- GNAT
Aspect_Dispatching_Domain,
Aspect_Dynamic_Predicate,
- Aspect_Effective_Reads, -- GNAT
- Aspect_Effective_Writes, -- GNAT
Aspect_Exceptional_Cases, -- GNAT
- Aspect_Extensions_Visible, -- GNAT
Aspect_External_Name,
Aspect_External_Tag,
- Aspect_Ghost, -- GNAT
Aspect_Ghost_Predicate, -- GNAT
Aspect_Global, -- GNAT
Aspect_GNAT_Annotate, -- GNAT
@@ -121,7 +113,6 @@ package Aspects is
Aspect_Max_Entry_Queue_Depth, -- GNAT
Aspect_Max_Entry_Queue_Length,
Aspect_Max_Queue_Length, -- GNAT
- Aspect_No_Caching, -- GNAT
Aspect_No_Controlled_Parts,
Aspect_No_Task_Parts, -- GNAT
Aspect_Object_Size, -- GNAT
@@ -146,7 +137,6 @@ package Aspects is
Aspect_Relaxed_Initialization, -- GNAT
Aspect_Scalar_Storage_Order, -- GNAT
Aspect_Secondary_Stack_Size, -- GNAT
- Aspect_Side_Effects, -- GNAT
Aspect_Simple_Storage_Pool, -- GNAT
Aspect_Size,
Aspect_Small,
@@ -168,7 +158,6 @@ package Aspects is
Aspect_User_Aspect, -- GNAT
Aspect_Value_Size, -- GNAT
Aspect_Variable_Indexing,
- Aspect_Volatile_Function, -- GNAT
Aspect_Warnings, -- GNAT
Aspect_Write,
@@ -190,17 +179,25 @@ package Aspects is
-- the aspect value is inherited from the parent, in which case, we do
-- not allow False if we inherit a True value from the parent.
+ Aspect_Always_Terminates, -- GNAT
Aspect_Asynchronous,
+ Aspect_Async_Readers, -- GNAT
+ Aspect_Async_Writers, -- GNAT
Aspect_Atomic,
Aspect_Atomic_Components,
+ Aspect_Constant_After_Elaboration, -- GNAT
Aspect_Disable_Controlled, -- GNAT
Aspect_Discard_Names,
Aspect_CUDA_Device, -- GNAT
Aspect_CUDA_Global, -- GNAT
+ Aspect_Effective_Reads, -- GNAT
+ Aspect_Effective_Writes, -- GNAT
Aspect_Exclusive_Functions,
Aspect_Export,
+ Aspect_Extensions_Visible, -- GNAT
Aspect_Favor_Top_Level, -- GNAT
Aspect_Full_Access_Only,
+ Aspect_Ghost, -- GNAT
Aspect_Independent,
Aspect_Independent_Components,
Aspect_Import,
@@ -208,6 +205,7 @@ package Aspects is
Aspect_Inline_Always, -- GNAT
Aspect_Interrupt_Handler,
Aspect_Lock_Free, -- GNAT
+ Aspect_No_Caching, -- GNAT
Aspect_No_Inline, -- GNAT
Aspect_No_Return,
Aspect_No_Tagged_Streams, -- GNAT
@@ -217,6 +215,7 @@ package Aspects is
Aspect_Pure_Function, -- GNAT
Aspect_Remote_Access_Type, -- GNAT
Aspect_Shared, -- GNAT (equivalent to Atomic)
+ Aspect_Side_Effects, -- GNAT
Aspect_Simple_Storage_Pool_Type, -- GNAT
Aspect_Static,
Aspect_Suppress_Debug_Info, -- GNAT
@@ -230,6 +229,7 @@ package Aspects is
Aspect_Volatile,
Aspect_Volatile_Components,
Aspect_Volatile_Full_Access, -- GNAT
+ Aspect_Volatile_Function, -- GNAT
Aspect_Yield);
subtype Aspect_Id_Exclude_No_Aspect is
@@ -353,9 +353,13 @@ package Aspects is
-- enabling the aspect. If the parameter is present it must be a static
-- expression of type Standard.Boolean. If the value is True, then the
-- aspect is enabled. If it is False, the aspect is disabled.
+ --
+ -- The Always_Terminates fits in this category even though it accepts an
+ -- optional boolean parameter which is non-static, because we want it to
+ -- be usable with pragma User_Defined_Aspect.
subtype Boolean_Aspects is
- Aspect_Id range Aspect_Asynchronous .. Aspect_Id'Last;
+ Aspect_Id range Aspect_Always_Terminates .. Aspect_Id'Last;
subtype Pre_Post_Aspects is
Aspect_Id range Aspect_Post .. Aspect_Precondition;
@@ -376,14 +380,10 @@ package Aspects is
Aspect_Address => Expression,
Aspect_Aggregate => Expression,
Aspect_Alignment => Expression,
- Aspect_Always_Terminates => Optional_Expression,
Aspect_Annotate => Expression,
- Aspect_Async_Readers => Optional_Expression,
- Aspect_Async_Writers => Optional_Expression,
Aspect_Attach_Handler => Expression,
Aspect_Bit_Order => Expression,
Aspect_Component_Size => Expression,
- Aspect_Constant_After_Elaboration => Optional_Expression,
Aspect_Constant_Indexing => Name,
Aspect_Contract_Cases => Expression,
Aspect_Convention => Name,
@@ -399,13 +399,9 @@ package Aspects is
Aspect_Dimension_System => Expression,
Aspect_Dispatching_Domain => Expression,
Aspect_Dynamic_Predicate => Expression,
- Aspect_Effective_Reads => Optional_Expression,
- Aspect_Effective_Writes => Optional_Expression,
Aspect_Exceptional_Cases => Expression,
- Aspect_Extensions_Visible => Optional_Expression,
Aspect_External_Name => Expression,
Aspect_External_Tag => Expression,
- Aspect_Ghost => Optional_Expression,
Aspect_Ghost_Predicate => Expression,
Aspect_Global => Expression,
Aspect_GNAT_Annotate => Expression,
@@ -425,7 +421,6 @@ package Aspects is
Aspect_Max_Entry_Queue_Depth => Expression,
Aspect_Max_Entry_Queue_Length => Expression,
Aspect_Max_Queue_Length => Expression,
- Aspect_No_Caching => Optional_Expression,
Aspect_No_Controlled_Parts => Optional_Expression,
Aspect_No_Task_Parts => Optional_Expression,
Aspect_Object_Size => Expression,
@@ -450,7 +445,6 @@ package Aspects is
Aspect_Relaxed_Initialization => Optional_Expression,
Aspect_Scalar_Storage_Order => Expression,
Aspect_Secondary_Stack_Size => Expression,
- Aspect_Side_Effects => Optional_Expression,
Aspect_Simple_Storage_Pool => Name,
Aspect_Size => Expression,
Aspect_Small => Expression,
@@ -472,7 +466,6 @@ package Aspects is
Aspect_User_Aspect => Expression,
Aspect_Value_Size => Expression,
Aspect_Variable_Indexing => Name,
- Aspect_Volatile_Function => Optional_Expression,
Aspect_Warnings => Name,
Aspect_Write => Name,
@@ -3548,52 +3548,6 @@ package body Sem_Ch13 is
goto Continue;
end Abstract_State;
- -- Aspect Async_Readers is never delayed because it is
- -- equivalent to a source pragma which appears after the
- -- related object declaration.
-
- when Aspect_Async_Readers =>
- Aitem := Make_Aitem_Pragma
- (Pragma_Argument_Associations => New_List (
- Make_Pragma_Argument_Association (Loc,
- Expression => Relocate_Node (Expr))),
- Pragma_Name => Name_Async_Readers);
-
- Decorate (Aspect, Aitem);
- Insert_Pragma (Aitem);
- goto Continue;
-
- -- Aspect Async_Writers is never delayed because it is
- -- equivalent to a source pragma which appears after the
- -- related object declaration.
-
- when Aspect_Async_Writers =>
- Aitem := Make_Aitem_Pragma
- (Pragma_Argument_Associations => New_List (
- Make_Pragma_Argument_Association (Loc,
- Expression => Relocate_Node (Expr))),
- Pragma_Name => Name_Async_Writers);
-
- Decorate (Aspect, Aitem);
- Insert_Pragma (Aitem);
- goto Continue;
-
- -- Aspect Constant_After_Elaboration is never delayed because
- -- it is equivalent to a source pragma which appears after the
- -- related object declaration.
-
- when Aspect_Constant_After_Elaboration =>
- Aitem := Make_Aitem_Pragma
- (Pragma_Argument_Associations => New_List (
- Make_Pragma_Argument_Association (Loc,
- Expression => Relocate_Node (Expr))),
- Pragma_Name =>
- Name_Constant_After_Elaboration);
-
- Decorate (Aspect, Aitem);
- Insert_Pragma (Aitem);
- goto Continue;
-
-- Aspect Default_Internal_Condition is never delayed because
-- it is equivalent to a source pragma which appears after the
-- related private type. To deal with forward references, the
@@ -3654,67 +3608,6 @@ package body Sem_Ch13 is
Insert_Pragma (Aitem);
goto Continue;
- -- Aspect Effective_Reads is never delayed because it is
- -- equivalent to a source pragma which appears after the
- -- related object declaration.
-
- when Aspect_Effective_Reads =>
- Aitem := Make_Aitem_Pragma
- (Pragma_Argument_Associations => New_List (
- Make_Pragma_Argument_Association (Loc,
- Expression => Relocate_Node (Expr))),
- Pragma_Name => Name_Effective_Reads);
-
- Decorate (Aspect, Aitem);
- Insert_Pragma (Aitem);
- goto Continue;
-
- -- Aspect Effective_Writes is never delayed because it is
- -- equivalent to a source pragma which appears after the
- -- related object declaration.
-
- when Aspect_Effective_Writes =>
- Aitem := Make_Aitem_Pragma
- (Pragma_Argument_Associations => New_List (
- Make_Pragma_Argument_Association (Loc,
- Expression => Relocate_Node (Expr))),
- Pragma_Name => Name_Effective_Writes);
-
- Decorate (Aspect, Aitem);
- Insert_Pragma (Aitem);
- goto Continue;
-
- -- Aspect Extensions_Visible is never delayed because it is
- -- equivalent to a source pragma which appears after the
- -- related subprogram.
-
- when Aspect_Extensions_Visible =>
- Aitem := Make_Aitem_Pragma
- (Pragma_Argument_Associations => New_List (
- Make_Pragma_Argument_Association (Loc,
- Expression => Relocate_Node (Expr))),
- Pragma_Name => Name_Extensions_Visible);
-
- Decorate (Aspect, Aitem);
- Insert_Pragma (Aitem);
- goto Continue;
-
- -- Aspect Ghost is never delayed because it is equivalent to a
- -- source pragma which appears at the top of [generic] package
- -- declarations or after an object, a [generic] subprogram, or
- -- a type declaration.
-
- when Aspect_Ghost =>
- Aitem := Make_Aitem_Pragma
- (Pragma_Argument_Associations => New_List (
- Make_Pragma_Argument_Association (Loc,
- Expression => Relocate_Node (Expr))),
- Pragma_Name => Name_Ghost);
-
- Decorate (Aspect, Aitem);
- Insert_Pragma (Aitem);
- goto Continue;
-
-- Global
-- Aspect Global is never delayed because it is equivalent to
@@ -3870,21 +3763,6 @@ package body Sem_Ch13 is
Insert_Pragma (Aitem);
goto Continue;
- -- Aspect No_Caching is never delayed because it is equivalent
- -- to a source pragma which appears after the related object
- -- declaration.
-
- when Aspect_No_Caching =>
- Aitem := Make_Aitem_Pragma
- (Pragma_Argument_Associations => New_List (
- Make_Pragma_Argument_Association (Loc,
- Expression => Relocate_Node (Expr))),
- Pragma_Name => Name_No_Caching);
-
- Decorate (Aspect, Aitem);
- Insert_Pragma (Aitem);
- goto Continue;
-
-- No_Controlled_Parts, No_Task_Parts
when Aspect_No_Controlled_Parts | Aspect_No_Task_Parts =>
@@ -3955,21 +3833,6 @@ package body Sem_Ch13 is
goto Continue;
- -- Aspect Side_Effects is never delayed because it is
- -- equivalent to a source pragma which appears after
- -- the related subprogram.
-
- when Aspect_Side_Effects =>
- Aitem := Make_Aitem_Pragma
- (Pragma_Argument_Associations => New_List (
- Make_Pragma_Argument_Association (Loc,
- Expression => Relocate_Node (Expr))),
- Pragma_Name => Name_Side_Effects);
-
- Decorate (Aspect, Aitem);
- Insert_Pragma (Aitem);
- goto Continue;
-
-- SPARK_Mode
when Aspect_SPARK_Mode =>
@@ -4135,23 +3998,6 @@ package body Sem_Ch13 is
Analyze_User_Aspect_Aspect_Specification (Aspect);
goto Continue;
- -- Volatile_Function
-
- -- Aspect Volatile_Function is never delayed because it is
- -- equivalent to a source pragma which appears after the
- -- related subprogram.
-
- when Aspect_Volatile_Function =>
- Aitem := Make_Aitem_Pragma
- (Pragma_Argument_Associations => New_List (
- Make_Pragma_Argument_Association (Loc,
- Expression => Relocate_Node (Expr))),
- Pragma_Name => Name_Volatile_Function);
-
- Decorate (Aspect, Aitem);
- Insert_Pragma (Aitem);
- goto Continue;
-
-- Case 2e: Annotate aspect
when Aspect_Annotate | Aspect_GNAT_Annotate =>
@@ -4542,19 +4388,6 @@ package body Sem_Ch13 is
Insert_Pragma (Aitem);
goto Continue;
- -- Always_Terminates
-
- when Aspect_Always_Terminates =>
- Aitem := Make_Aitem_Pragma
- (Pragma_Argument_Associations => New_List (
- Make_Pragma_Argument_Association (Loc,
- Expression => Relocate_Node (Expr))),
- Pragma_Name => Name_Always_Terminates);
-
- Decorate (Aspect, Aitem);
- Insert_Pragma (Aitem);
- goto Continue;
-
-- Exceptional_Cases
when Aspect_Exceptional_Cases =>
@@ -4659,6 +4492,31 @@ package body Sem_Ch13 is
elsif A_Id = Aspect_Yield then
Analyze_Aspect_Yield;
goto Continue;
+
+ -- Handle Boolean aspects equivalent to source pragmas which
+ -- appears after the related object declaration.
+
+ elsif A_Id in Aspect_Always_Terminates
+ | Aspect_Async_Readers
+ | Aspect_Async_Writers
+ | Aspect_Constant_After_Elaboration
+ | Aspect_Effective_Reads
+ | Aspect_Effective_Writes
+ | Aspect_Extensions_Visible
+ | Aspect_Ghost
+ | Aspect_No_Caching
+ | Aspect_Side_Effects
+ | Aspect_Volatile_Function
+ then
+ Aitem :=
+ Make_Aitem_Pragma
+ (Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Relocate_Node (Expr))),
+ Pragma_Name => Nam);
+ Decorate (Aspect, Aitem);
+ Insert_Pragma (Aitem);
+ goto Continue;
end if;
-- Library unit aspects require special handling in the case
@@ -11545,21 +11403,13 @@ package body Sem_Ch13 is
-- Here is the list of aspects that don't require delay analysis
when Aspect_Abstract_State
- | Aspect_Always_Terminates
| Aspect_Annotate
- | Aspect_Async_Readers
- | Aspect_Async_Writers
- | Aspect_Constant_After_Elaboration
| Aspect_Contract_Cases
| Aspect_Default_Initial_Condition
| Aspect_Depends
| Aspect_Dimension
| Aspect_Dimension_System
| Aspect_Exceptional_Cases
- | Aspect_Effective_Reads
- | Aspect_Effective_Writes
- | Aspect_Extensions_Visible
- | Aspect_Ghost
| Aspect_Global
| Aspect_GNAT_Annotate
| Aspect_Implicit_Dereference
@@ -11568,7 +11418,6 @@ package body Sem_Ch13 is
| Aspect_Max_Entry_Queue_Depth
| Aspect_Max_Entry_Queue_Length
| Aspect_Max_Queue_Length
- | Aspect_No_Caching
| Aspect_No_Controlled_Parts
| Aspect_No_Task_Parts
| Aspect_Obsolescent
@@ -11577,7 +11426,6 @@ package body Sem_Ch13 is
| Aspect_Postcondition
| Aspect_Pre
| Aspect_Precondition
- | Aspect_Side_Effects
| Aspect_Refined_Depends
| Aspect_Refined_Global
| Aspect_Refined_Post
@@ -11590,7 +11438,6 @@ package body Sem_Ch13 is
| Aspect_Unimplemented
| Aspect_Unsuppress
| Aspect_User_Aspect
- | Aspect_Volatile_Function
=>
raise Program_Error;
From: Piotr Trojanek <trojanek@adacore.com> The implementation of User_Aspect_Definition uses subtype Boolean_Aspects to decide which existing aspects can be used to define old aspects. This subtype didn't include many of the SPARK aspects, notably the Always_Terminates. gcc/ada/ * aspects.ads (Aspect_Id, Boolean_Aspect): Change categorization of Boolean-valued SPARK aspects. * sem_ch13.adb (Analyze_Aspect_Specification): Adapt CASE statements to new classification of Boolean-valued SPARK aspects. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/aspects.ads | 39 ++++----- gcc/ada/sem_ch13.adb | 203 ++++++------------------------------------- 2 files changed, 41 insertions(+), 201 deletions(-)