https://gcc.gnu.org/g:8d15d848b90f502bdc3070f5b4e6213721eb2272
commit r15-478-g8d15d848b90f502bdc3070f5b4e6213721eb2272 Author: Piotr Trojanek <troja...@adacore.com> Date: Mon Feb 19 09:46:04 2024 +0100 ada: Fix classification of SPARK Boolean aspects 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. Diff: --- gcc/ada/aspects.ads | 39 ++++------ gcc/ada/sem_ch13.adb | 203 +++++++-------------------------------------------- 2 files changed, 41 insertions(+), 201 deletions(-) diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads index a348b322d29a..eb5ab1a85dd4 100644 --- a/gcc/ada/aspects.ads +++ b/gcc/ada/aspects.ads @@ -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, diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 1ad5c4c0128f..eee2aa09cd5c 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -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;