diff options
author | Piotr Trojanek <trojanek@adacore.com> | 2023-05-02 16:03:18 +0200 |
---|---|---|
committer | Marc Poulhiès <poulhies@adacore.com> | 2023-06-13 09:31:45 +0200 |
commit | dcc601423c21a3902d6dd22d40a9a828ce9658b0 (patch) | |
tree | fd4c08f457c25ee27ea57fe3962b79151ba47b73 | |
parent | 204dba400b42b75271071b05102a5b46fd2a34d0 (diff) | |
download | gcc-dcc601423c21a3902d6dd22d40a9a828ce9658b0.zip gcc-dcc601423c21a3902d6dd22d40a9a828ce9658b0.tar.gz gcc-dcc601423c21a3902d6dd22d40a9a828ce9658b0.tar.bz2 |
ada: Implement new aspect Always_Terminates for SPARK
This patch allows subprograms to be annotated with aspect
Always_Terminates that requires a boolean expression. When this
expression evaluates to True, the subprogram is required to terminate or
raise an exception, but not loop infinitely.
This aspect is only meant to be used by GNATprove and it has no
meaningful run-time semantics: either the annotated subprogram
terminates and then the aspect expression doesn't matter, or the
subprogram loops infinitely and there is nothing we can do. (We could
also evaluate the aspect expression just to detect run-time errors in
the expression itself, but this can be implemented later, after a
backend support for the aspect is added to GNATprove.)
Implementation of this aspect is heavily based on the implementation of
Subprogram_Variant, which in turn is heavily based on the implementation
of Contract_Cases. Since the new aspect is not yet expanded, there is no
corresponding assertion kind that would control the expansion.
gcc/ada/
* aspects.ads (Aspect_Id): Add new aspect.
(Implementation_Defined_Aspect): New aspect is
implementation-defined.
(Aspect_Argument): New aspect has an expression argument.
(Is_Representation_Aspect): New aspect is not a representation
aspect.
(Aspect_Names): Link new aspect identifier with a name.
(Aspect_Delay): New aspect is never delayed.
* contracts.adb (Expand_Subprogram_Contract): Mention new aspect
in comment.
(Add_Contract_Item): Attach pragma corresponding to the new aspect
to contract items.
(Analyze_Entry_Or_Subprogram_Contract): Analyze pragma
corresponding to the new aspect that appears with subprogram spec.
(Analyze_Subprogram_Body_Stub_Contract): Expand pragma
corresponding to the new aspect.
* contracts.ads
(Add_Contract_Item, Analyze_Entry_Or_Subprogram_Contract)
(Analyze_Entry_Or_Subprogram_Body_Contract)
(Analyze_Subprogram_Body_Stub_Contract): Mention new aspect in
comment.
* einfo-utils.adb (Get_Pragma): Return pragma attached to
contract.
* einfo-utils.ads (Get_Pragma): Mention new contract in comment.
* exp_prag.adb (Expand_Pragma_Always_Terminates): Placeholder for
possibly expanding new aspect.
* exp_prag.ads (Expand_Pragma_Always_Terminates): Dedicated
routine for expansion of the new aspect.
* inline.adb (Remove_Aspects_And_Pragmas): Remove aspect from
inlined bodies.
* par-prag.adb (Prag): Postpone checking of the pragma until
analysis.
* sem_ch12.adb: Mention new aspect in explanation of handling
contracts on generic units.
* sem_ch13.adb (Analyze_Aspect_Specifications): Convert new aspect
into a corresponding pragma.
(Check_Aspect_At_Freeze_Point): Don't expect new aspect.
* sem_prag.adb (Analyze_Always_Terminates_In_Decl_Part): Analyze
pragma corresponding to the new aspect.
(Analyze_Pragma): Handle pragma corresponding to the new aspect.
(Is_Non_Significant_Pragma_Reference): Handle references appearing
within new aspect.
* sem_prag.ads (Aspect_Specifying_Pragma): New aspect can be
emulated with a pragma.
(Assertion_Expression_Pragma): New aspect has an assertion
expression.
(Pragma_Significant_To_Subprograms): New aspect is significant to
subprograms.
(Analyze_Always_Terminates_In_Decl_Part): Add spec for routine
that analyses new aspect.
(Find_Related_Declaration_Or_Body): Mention new aspect in comment.
* sem_util.adb (Is_Subprogram_Contract_Annotation): New aspect is
a subprogram contract annotation.
* sem_util.ads (Is_Subprogram_Contract_Annotation): Mention new
aspect in comment.
* sinfo.ads (Is_Generic_Contract_Pragma): New pragma is a generic
contract.
(Contract): Explain attaching new pragma to subprogram contract.
* snames.ads-tmpl (Name_Always_Terminates): New name for the new
contract.
(Pragma_Always_Terminates): New pragma identifier.
-rw-r--r-- | gcc/ada/aspects.ads | 6 | ||||
-rw-r--r-- | gcc/ada/contracts.adb | 29 | ||||
-rw-r--r-- | gcc/ada/contracts.ads | 4 | ||||
-rw-r--r-- | gcc/ada/einfo-utils.adb | 1 | ||||
-rw-r--r-- | gcc/ada/einfo-utils.ads | 1 | ||||
-rw-r--r-- | gcc/ada/exp_prag.adb | 10 | ||||
-rw-r--r-- | gcc/ada/exp_prag.ads | 4 | ||||
-rw-r--r-- | gcc/ada/inline.adb | 4 | ||||
-rw-r--r-- | gcc/ada/par-prag.adb | 1 | ||||
-rw-r--r-- | gcc/ada/sem_ch12.adb | 7 | ||||
-rw-r--r-- | gcc/ada/sem_ch13.adb | 30 | ||||
-rw-r--r-- | gcc/ada/sem_prag.adb | 199 | ||||
-rw-r--r-- | gcc/ada/sem_prag.ads | 15 | ||||
-rw-r--r-- | gcc/ada/sem_util.adb | 3 | ||||
-rw-r--r-- | gcc/ada/sem_util.ads | 1 | ||||
-rw-r--r-- | gcc/ada/sinfo.ads | 2 | ||||
-rw-r--r-- | gcc/ada/snames.ads-tmpl | 2 |
17 files changed, 295 insertions, 24 deletions
diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads index bd8e7c6..19f7c07 100644 --- a/gcc/ada/aspects.ads +++ b/gcc/ada/aspects.ads @@ -72,6 +72,7 @@ package Aspects is Aspect_Address, Aspect_Aggregate, Aspect_Alignment, + Aspect_Always_Terminates, -- GNAT Aspect_Annotate, -- GNAT Aspect_Async_Readers, -- GNAT Aspect_Async_Writers, -- GNAT @@ -261,6 +262,7 @@ package Aspects is Implementation_Defined_Aspect : constant array (Aspect_Id) of Boolean := (Aspect_Abstract_State => True, + Aspect_Always_Terminates => True, Aspect_Annotate => True, Aspect_Async_Readers => True, Aspect_Async_Writers => True, @@ -370,6 +372,7 @@ package Aspects is Aspect_Address => Expression, Aspect_Aggregate => Expression, Aspect_Alignment => Expression, + Aspect_Always_Terminates => Expression, Aspect_Annotate => Expression, Aspect_Async_Readers => Optional_Expression, Aspect_Async_Writers => Optional_Expression, @@ -477,6 +480,7 @@ package Aspects is Aspect_Address => True, Aspect_Aggregate => False, Aspect_Alignment => True, + Aspect_Always_Terminates => False, Aspect_Annotate => False, Aspect_Async_Readers => False, Aspect_Async_Writers => False, @@ -630,6 +634,7 @@ package Aspects is Aspect_Aggregate => Name_Aggregate, Aspect_Alignment => Name_Alignment, Aspect_All_Calls_Remote => Name_All_Calls_Remote, + Aspect_Always_Terminates => Name_Always_Terminates, Aspect_Annotate => Name_Annotate, Aspect_Async_Readers => Name_Async_Readers, Aspect_Async_Writers => Name_Async_Writers, @@ -980,6 +985,7 @@ package Aspects is Aspect_Write => Always_Delay, Aspect_Abstract_State => Never_Delay, + Aspect_Always_Terminates => Never_Delay, Aspect_Annotate => Never_Delay, Aspect_Async_Readers => Never_Delay, Aspect_Async_Writers => Never_Delay, diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index 19073d1..0e87cee 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -109,9 +109,9 @@ package body Contracts is procedure Expand_Subprogram_Contract (Body_Id : Entity_Id); -- Expand the contracts of a subprogram body and its correspoding spec (if -- any). This routine processes all [refined] pre- and postconditions as - -- well as Contract_Cases, Exceptional_Cases, Subprogram_Variant, - -- invariants and predicates. Body_Id denotes the entity of the - -- subprogram body. + -- well as Always_Terminates, Contract_Cases, Exceptional_Cases, + -- Subprogram_Variant, invariants and predicates. Body_Id denotes the + -- entity of the subprogram body. procedure Preanalyze_Condition (Subp : Entity_Id; @@ -225,6 +225,7 @@ package body Contracts is end if; -- Entry or subprogram declarations, the applicable pragmas are: + -- Always_Terminates -- Attach_Handler -- Contract_Cases -- Depends @@ -260,7 +261,8 @@ package body Contracts is then Add_Classification; - elsif Prag_Nam in Name_Contract_Cases + elsif Prag_Nam in Name_Always_Terminates + | Name_Contract_Cases | Name_Exceptional_Cases | Name_Subprogram_Variant | Name_Test_Case @@ -663,10 +665,10 @@ package body Contracts is Gen_Id => Spec_Id); end if; - -- Deal with preconditions, [refined] postconditions, Contract_Cases, - -- Exceptional_Cases, Subprogram_Variant, invariants and predicates - -- associated with body and its spec. Do not expand the contract of - -- subprogram body stubs. + -- Deal with preconditions, [refined] postconditions, Always_Terminates, + -- Contract_Cases, Exceptional_Cases, Subprogram_Variant, invariants and + -- predicates associated with body and its spec. Do not expand the + -- contract of subprogram body stubs. if Nkind (Body_Decl) = N_Subprogram_Body then Expand_Subprogram_Contract (Body_Id); @@ -789,7 +791,10 @@ package body Contracts is while Present (Prag) loop Prag_Nam := Pragma_Name (Prag); - if Prag_Nam = Name_Contract_Cases then + if Prag_Nam = Name_Always_Terminates then + Analyze_Always_Terminates_In_Decl_Part (Prag); + + elsif Prag_Nam = Name_Contract_Cases then -- Do not analyze the contract cases of an entry declaration -- unless annotating the original tree for GNATprove. @@ -1533,6 +1538,7 @@ package body Contracts is Analyze_Entry_Or_Subprogram_Body_Contract (Stub_Id); -- The stub acts as its own spec, the applicable pragmas are: + -- Always_Terminates -- Contract_Cases -- Depends -- Exceptional_Cases @@ -2879,7 +2885,10 @@ package body Contracts is Prag := Contract_Test_Cases (Items); while Present (Prag) loop if Is_Checked (Prag) then - if Pragma_Name (Prag) = Name_Contract_Cases then + if Pragma_Name (Prag) = Name_Always_Terminates then + Expand_Pragma_Always_Terminates (Prag); + + elsif Pragma_Name (Prag) = Name_Contract_Cases then Expand_Pragma_Contract_Cases (CCs => Prag, Subp_Id => Subp_Id, diff --git a/gcc/ada/contracts.ads b/gcc/ada/contracts.ads index d52e1aa..c3dc5d6 100644 --- a/gcc/ada/contracts.ads +++ b/gcc/ada/contracts.ads @@ -37,6 +37,7 @@ package Contracts is -- The following are valid pragmas: -- -- Abstract_State + -- Always_Terminates -- Async_Readers -- Async_Writers -- Attach_Handler @@ -81,6 +82,7 @@ package Contracts is -- subprogram body Body_Id as if they appeared at the end of a declarative -- region. Pragmas in question are: -- + -- Always_Terminates (stand alone subprogram body) -- Contract_Cases (stand alone subprogram body) -- Depends (stand alone subprogram body) -- Exceptional_Cases (stand alone subprogram body) @@ -100,6 +102,7 @@ package Contracts is -- subprogram Subp_Id as if they appeared at the end of a declarative -- region. The pragmas in question are: -- + -- Always_Terminates -- Contract_Cases -- Depends -- Exceptional_Cases @@ -175,6 +178,7 @@ package Contracts is -- stub Stub_Id as if they appeared at the end of a declarative region. The -- pragmas in question are: -- + -- Always_Terminates -- Contract_Cases -- Depends -- Exceptional_Cases diff --git a/gcc/ada/einfo-utils.adb b/gcc/ada/einfo-utils.adb index d1db66f..dad3a65 100644 --- a/gcc/ada/einfo-utils.adb +++ b/gcc/ada/einfo-utils.adb @@ -1017,6 +1017,7 @@ package body Einfo.Utils is -- Contract / subprogram variant / test case pragmas Is_CTC : constant Boolean := + Id = Pragma_Always_Terminates or else Id = Pragma_Contract_Cases or else Id = Pragma_Exceptional_Cases or else Id = Pragma_Subprogram_Variant or else diff --git a/gcc/ada/einfo-utils.ads b/gcc/ada/einfo-utils.ads index e805502..fee771c 100644 --- a/gcc/ada/einfo-utils.ads +++ b/gcc/ada/einfo-utils.ads @@ -439,6 +439,7 @@ package Einfo.Utils is -- node, otherwise Empty is returned. The following contract pragmas that -- appear in N_Contract nodes are also handled by this routine: -- Abstract_State + -- Always_Terminates -- Async_Readers -- Async_Writers -- Attach_Handler diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb index e660196..1cc4653 100644 --- a/gcc/ada/exp_prag.adb +++ b/gcc/ada/exp_prag.adb @@ -269,6 +269,16 @@ package body Exp_Prag is end; end Expand_Pragma_Abort_Defer; + ------------------------------------- + -- Expand_Pragma_Always_Terminates -- + ------------------------------------- + + procedure Expand_Pragma_Always_Terminates (Prag : Node_Id) is + pragma Unreferenced (Prag); + begin + null; + end Expand_Pragma_Always_Terminates; + -------------------------- -- Expand_Pragma_Check -- -------------------------- diff --git a/gcc/ada/exp_prag.ads b/gcc/ada/exp_prag.ads index 9f810da..10ccaf7 100644 --- a/gcc/ada/exp_prag.ads +++ b/gcc/ada/exp_prag.ads @@ -31,6 +31,10 @@ package Exp_Prag is procedure Expand_N_Pragma (N : Node_Id); + procedure Expand_Pragma_Always_Terminates (Prag : Node_Id); + -- This routine only exists for consistency with other pragmas, since + -- Always_Terminates has no meaningful expansion. + procedure Expand_Pragma_Contract_Cases (CCs : Node_Id; Subp_Id : Entity_Id; diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index a4c32e9..edb90a9 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.adb @@ -312,6 +312,7 @@ package body Inline is -- Remove all aspects and/or pragmas that have no meaning in inlined body -- Body_Decl. The analysis of these items is performed on the non-inlined -- body. The items currently removed are: + -- Always_Terminates -- Contract_Cases -- Global -- Depends @@ -5225,7 +5226,8 @@ package body Inline is end if; if Present (Item_Id) - and then Chars (Item_Id) in Name_Contract_Cases + and then Chars (Item_Id) in Name_Always_Terminates + | Name_Contract_Cases | Name_Global | Name_Depends | Name_Exceptional_Cases diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb index ac50c84..b139862 100644 --- a/gcc/ada/par-prag.adb +++ b/gcc/ada/par-prag.adb @@ -1315,6 +1315,7 @@ begin | Pragma_Aggregate_Individually_Assign | Pragma_All_Calls_Remote | Pragma_Allow_Integer_Address + | Pragma_Always_Terminates | Pragma_Annotate | Pragma_Assert | Pragma_Assert_And_Cut diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index a38ab28..f584a9f 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -261,9 +261,10 @@ package body Sem_Ch12 is -- as annotations: -- package subprogram [body] - -- Abstract_State Contract_Cases - -- Initial_Condition Depends - -- Initializes Exceptional_Cases + -- Abstract_State Always_Terminates + -- Initial_Condition Contract_Cases + -- Initializes Depends + -- Exceptional_Cases -- Extensions_Visible -- Global -- package body Post diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 2b8b64a..e771c0d 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -1407,6 +1407,7 @@ package body Sem_Ch13 is Is_Instance : Boolean := False); -- Subsidiary to the analysis of aspects -- Abstract_State + -- Always_Terminates -- Attach_Handler -- Contract_Cases -- Depends @@ -1667,10 +1668,11 @@ package body Sem_Ch13 is -- analyzed right now. -- Note that there is a special handling for Pre, Post, Test_Case, - -- Contract_Cases, Exceptional_Cases and Subprogram_Variant aspects. - -- In these cases, we do not have to worry about delay issues, since the - -- pragmas themselves deal with delay of visibility for the expression - -- analysis. Thus, we just insert the pragma after the node N. + -- Contract_Cases, Always_Terminates, Exceptional_Cases and + -- Subprogram_Variant aspects. In these cases, we do not have to worry + -- about delay issues, since the pragmas themselves deal with delay of + -- visibility for the expression analysis. Thus, we just insert the + -- pragma after the node N. -- Loop through aspects @@ -4297,9 +4299,9 @@ package body Sem_Ch13 is -- Case 4: Aspects requiring special handling - -- Pre/Post/Test_Case/Contract_Cases/Exceptional_Cases and - -- Subprogram_Variant whose corresponding pragmas take care - -- of the delay. + -- Pre/Post/Test_Case/Contract_Cases/Always_Terminates/ + -- Exceptional_Cases and Subprogram_Variant whose corresponding + -- pragmas take care of the delay. -- Pre/Post @@ -4531,6 +4533,19 @@ 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 => @@ -11315,6 +11330,7 @@ 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 diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index abc0e5d..bca4eb5 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -420,6 +420,79 @@ package body Sem_Prag is end if; end Adjust_External_Name_Case; + -------------------------------------------- + -- Analyze_Always_Terminates_In_Decl_Part -- + -------------------------------------------- + + procedure Analyze_Always_Terminates_In_Decl_Part + (N : Node_Id; + Freeze_Id : Entity_Id := Empty) + is + Subp_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N); + Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl); + Expr : constant Node_Id := Expression (Get_Argument (N, Spec_Id)); + + Saved_GM : constant Ghost_Mode_Type := Ghost_Mode; + Saved_IGR : constant Node_Id := Ignored_Ghost_Region; + -- Save the Ghost-related attributes to restore on exit + + Errors : Nat; + Restore_Scope : Boolean := False; + + begin + -- Do not analyze the pragma multiple times + + if Is_Analyzed_Pragma (N) then + return; + end if; + + -- Set the Ghost mode in effect from the pragma. Due to the delayed + -- analysis of the pragma, the Ghost mode at point of declaration and + -- point of analysis may not necessarily be the same. Use the mode in + -- effect at the point of declaration. + + Set_Ghost_Mode (N); + + -- Ensure that the subprogram and its formals are visible when analyzing + -- the expression of the pragma. + + if not In_Open_Scopes (Spec_Id) then + Restore_Scope := True; + + if Is_Generic_Subprogram (Spec_Id) then + Push_Scope (Spec_Id); + Install_Generic_Formals (Spec_Id); + else + Push_Scope (Spec_Id); + Install_Formals (Spec_Id); + end if; + end if; + + Errors := Serious_Errors_Detected; + Preanalyze_Assert_Expression (Expr, Standard_Boolean); + + -- Emit a clarification message when the expression contains at least + -- one undefined reference, possibly due to contract freezing. + + if Errors /= Serious_Errors_Detected + and then Present (Freeze_Id) + and then Has_Undefined_Reference (Expr) + then + Contract_Freeze_Error (Spec_Id, Freeze_Id); + end if; + + if Restore_Scope then + End_Scope; + end if; + + -- Currently it is not possible to inline pre/postconditions on a + -- subprogram subject to pragma Inline_Always. + + Set_Is_Analyzed_Pragma (N); + + Restore_Ghost_Region (Saved_GM, Saved_IGR); + end Analyze_Always_Terminates_In_Decl_Part; + ----------------------------------------- -- Analyze_Contract_Cases_In_Decl_Part -- ----------------------------------------- @@ -13202,6 +13275,131 @@ package body Sem_Prag is Opt.Allow_Integer_Address := True; end if; + ----------------------- + -- Always_Terminates -- + ----------------------- + + -- pragma Always_Terminates (boolean_EXPRESSION); + + -- Characteristics: + + -- * Analysis - The annotation undergoes initial checks to verify + -- the legal placement and context. Secondary checks preanalyze the + -- expressions in: + + -- Analyze_Always_Terminates_Cases_In_Decl_Part + + -- * Expansion - The annotation is expanded during the expansion of + -- the related subprogram [body] contract as performed in: + + -- Expand_Subprogram_Contract + + -- * Template - The annotation utilizes the generic template of the + -- related subprogram [body] when it is: + + -- aspect on subprogram declaration + -- aspect on stand-alone subprogram body + -- pragma on stand-alone subprogram body + + -- The annotation must prepare its own template when it is: + + -- pragma on subprogram declaration + + -- * Globals - Capture of global references must occur after full + -- analysis. + + -- * Instance - The annotation is instantiated automatically when + -- the related generic subprogram [body] is instantiated except for + -- the "pragma on subprogram declaration" case. In that scenario + -- the annotation must instantiate itself. + + when Pragma_Always_Terminates => Always_Terminates : declare + Spec_Id : Entity_Id; + Subp_Decl : Node_Id; + Subp_Spec : Node_Id; + + begin + GNAT_Pragma; + Check_No_Identifiers; + Check_Arg_Count (1); + + -- Ensure the proper placement of the pragma. Exceptional_Cases + -- must be associated with a subprogram declaration or a body that + -- acts as a spec. + + Subp_Decl := + Find_Related_Declaration_Or_Body (N, Do_Checks => True); + + -- Generic subprogram + + if Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then + null; + + -- Body acts as spec + + elsif Nkind (Subp_Decl) = N_Subprogram_Body + and then No (Corresponding_Spec (Subp_Decl)) + then + null; + + -- Body stub acts as spec + + elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub + and then No (Corresponding_Spec_Of_Stub (Subp_Decl)) + then + null; + + -- Subprogram + + elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then + Subp_Spec := Specification (Subp_Decl); + + -- Pragma Always_Terminates is forbidden on null procedures, + -- as this may lead to potential ambiguities in behavior + -- when interface null procedures are involved. Also, it + -- just wouldn't make sense, because null procedures always + -- terminate anyway. + + if Nkind (Subp_Spec) = N_Procedure_Specification + and then Null_Present (Subp_Spec) + then + Error_Msg_N (Fix_Error + ("pragma % cannot apply to null procedure"), N); + return; + end if; + + else + Pragma_Misplaced; + end if; + + Spec_Id := Unique_Defining_Entity (Subp_Decl); + + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Ghost_Pragma (N, Spec_Id); + + -- Chain the pragma on the contract for further processing by + -- Analyze_Always_Terminates_In_Decl_Part. + + Add_Contract_Item (N, Defining_Entity (Subp_Decl)); + + -- Fully analyze the pragma when it appears inside a subprogram + -- body because it cannot benefit from forward references. + + if Nkind (Subp_Decl) in N_Subprogram_Body + | N_Subprogram_Body_Stub + then + -- The legality checks of pragma Always_Terminates are affected + -- by the SPARK mode in effect and the volatility of the + -- context. Analyze all pragmas in a specific order. + + Analyze_If_Present (Pragma_SPARK_Mode); + Analyze_If_Present (Pragma_Volatile_Function); + Analyze_Always_Terminates_In_Decl_Part (N); + end if; + end Always_Terminates; + -------------- -- Annotate -- -------------- @@ -31990,6 +32188,7 @@ package body Sem_Prag is Pragma_Aggregate_Individually_Assign => 0, Pragma_All_Calls_Remote => -1, Pragma_Allow_Integer_Address => -1, + Pragma_Always_Terminates => -1, Pragma_Annotate => 93, Pragma_Assert => -1, Pragma_Assert_And_Cut => -1, diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index 49c1d0b..e8e9856 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.ads @@ -38,6 +38,7 @@ package Sem_Prag is Aspect_Specifying_Pragma : constant array (Pragma_Id) of Boolean := (Pragma_Abstract_State => True, Pragma_All_Calls_Remote => True, + Pragma_Always_Terminates => True, Pragma_Annotate => True, Pragma_Async_Readers => True, Pragma_Async_Writers => True, @@ -133,7 +134,8 @@ package Sem_Prag is -- expression. Assertion_Expression_Pragma : constant array (Pragma_Id) of Boolean := - (Pragma_Assert => True, + (Pragma_Always_Terminates => True, + Pragma_Assert => True, Pragma_Assert_And_Cut => True, Pragma_Assume => True, Pragma_Check => True, @@ -210,7 +212,8 @@ package Sem_Prag is -- of subprogram bodies. Pragma_Significant_To_Subprograms : constant array (Pragma_Id) of Boolean := - (Pragma_Contract_Cases => True, + (Pragma_Always_Terminates => True, + Pragma_Contract_Cases => True, Pragma_Depends => True, Pragma_Exceptional_Cases => True, Pragma_Ghost => True, @@ -241,6 +244,13 @@ package Sem_Prag is procedure Analyze_Pragma (N : Node_Id); -- Analyze procedure for pragma reference node N + procedure Analyze_Always_Terminates_In_Decl_Part + (N : Node_Id; + Freeze_Id : Entity_Id := Empty); + -- Perform full analysis of delayed pragma Always_Terminates. Freeze_Id is + -- the entity of [generic] package body or [generic] subprogram body which + -- caused "freezing" of the related contract where the pragma resides. + procedure Analyze_Contract_Cases_In_Decl_Part (N : Node_Id; Freeze_Id : Entity_Id := Empty); @@ -445,6 +455,7 @@ package Sem_Prag is (Prag : Node_Id; Do_Checks : Boolean := False) return Node_Id; -- Subsidiary to the analysis of pragmas + -- Always_Terminates -- Contract_Cases -- Depends -- Exceptional_Cases diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index c736bc3..b82978b 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -20558,7 +20558,8 @@ package body Sem_Util is Nam := Pragma_Name (Item); end if; - return Nam = Name_Contract_Cases + return Nam = Name_Always_Terminates + or else Nam = Name_Contract_Cases or else Nam = Name_Depends or else Nam = Name_Exceptional_Cases or else Nam = Name_Extensions_Visible diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 539ebeb..3751fb7 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -2349,6 +2349,7 @@ package Sem_Util is function Is_Subprogram_Contract_Annotation (Item : Node_Id) return Boolean; -- Determine whether aspect specification or pragma Item is one of the -- following subprogram contract annotations: + -- Always_Terminates -- Contract_Cases -- Depends -- Exceptional_Cases diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index b565221..0efbd44 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -1711,6 +1711,7 @@ package Sinfo is -- a source construct, applies to a generic unit or its body, and denotes -- one of the following contract-related annotations: -- Abstract_State + -- Always_Terminates -- Contract_Cases -- Depends -- Exceptional_Cases @@ -7978,6 +7979,7 @@ package Sinfo is -- establish dependencies between subprogram or package inputs and -- outputs. Currently the following pragmas appear in this list: -- Abstract_States + -- Always_Terminates -- Async_Readers -- Async_Writers -- Constant_After_Elaboration diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index 135b253..5044abb 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -503,6 +503,7 @@ package Snames is Name_Abort_Defer : constant Name_Id := N + $; -- GNAT Name_Abstract_State : constant Name_Id := N + $; -- GNAT Name_All_Calls_Remote : constant Name_Id := N + $; + Name_Always_Terminates : constant Name_Id := N + $; -- GNAT Name_Assert : constant Name_Id := N + $; -- Ada 05 Name_Assert_And_Cut : constant Name_Id := N + $; -- GNAT Name_Assume : constant Name_Id := N + $; -- GNAT @@ -1813,6 +1814,7 @@ package Snames is Pragma_Abort_Defer, Pragma_Abstract_State, Pragma_All_Calls_Remote, + Pragma_Always_Terminates, Pragma_Assert, Pragma_Assert_And_Cut, Pragma_Assume, |