* [COMMITTED] ada: Implement new aspect Always_Terminates for SPARK
@ 2023-06-13 7:38 Marc Poulhiès
0 siblings, 0 replies; only message in thread
From: Marc Poulhiès @ 2023-06-13 7:38 UTC (permalink / raw)
To: gcc-patches; +Cc: Piotr Trojanek
From: Piotr Trojanek <trojanek@adacore.com>
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.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/aspects.ads | 6 ++
gcc/ada/contracts.adb | 29 ++++--
gcc/ada/contracts.ads | 4 +
gcc/ada/einfo-utils.adb | 1 +
gcc/ada/einfo-utils.ads | 1 +
gcc/ada/exp_prag.adb | 10 ++
gcc/ada/exp_prag.ads | 4 +
gcc/ada/inline.adb | 4 +-
gcc/ada/par-prag.adb | 1 +
gcc/ada/sem_ch12.adb | 7 +-
gcc/ada/sem_ch13.adb | 30 ++++--
gcc/ada/sem_prag.adb | 199 ++++++++++++++++++++++++++++++++++++++++
gcc/ada/sem_prag.ads | 15 ++-
gcc/ada/sem_util.adb | 3 +-
gcc/ada/sem_util.ads | 1 +
gcc/ada/sinfo.ads | 2 +
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 bd8e7c61a83..19f7c07130f 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 19073d1e4d8..0e87cee3ef5 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 d52e1aaed4a..c3dc5d67734 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 d1db66ff697..dad3a654743 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 e8055020a67..fee771c20f4 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 e660196c0f1..1cc4653a3b0 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 9f810dab227..10ccaf70c67 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 a4c32e984da..edb90a9fe20 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 ac50c846bf9..b1398625fe2 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 a38ab284ce7..f584a9f3fb5 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 2b8b64aa392..e771c0d2020 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 abc0e5dbb9d..bca4eb50430 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 49c1d0b4892..e8e9856d8a3 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 c736bc34bb1..b82978ba99e 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 539ebebafcb..3751fb73702 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 b565221f730..0efbd4479e0 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 135b2533f9b..5044abbc7d0 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,
--
2.40.0
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2023-06-13 7:38 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2023-06-13 7:38 [COMMITTED] ada: Implement new aspect Always_Terminates for SPARK Marc Poulhiès
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).