Aspect_Address,
Aspect_Aggregate,
Aspect_Alignment,
+ Aspect_Always_Terminates, -- GNAT
Aspect_Annotate, -- GNAT
Aspect_Async_Readers, -- GNAT
Aspect_Async_Writers, -- GNAT
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,
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,
Aspect_Address => True,
Aspect_Aggregate => False,
Aspect_Alignment => True,
+ Aspect_Always_Terminates => False,
Aspect_Annotate => False,
Aspect_Async_Readers => False,
Aspect_Async_Writers => False,
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,
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,
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;
end if;
-- Entry or subprogram declarations, the applicable pragmas are:
+ -- Always_Terminates
-- Attach_Handler
-- Contract_Cases
-- Depends
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
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);
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.
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
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,
-- The following are valid pragmas:
--
-- Abstract_State
+ -- Always_Terminates
-- Async_Readers
-- Async_Writers
-- Attach_Handler
-- 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)
-- 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
-- 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
-- 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
-- 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
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 --
--------------------------
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;
-- 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
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
| Pragma_Aggregate_Individually_Assign
| Pragma_All_Calls_Remote
| Pragma_Allow_Integer_Address
+ | Pragma_Always_Terminates
| Pragma_Annotate
| Pragma_Assert
| Pragma_Assert_And_Cut
-- 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
Is_Instance : Boolean := False);
-- Subsidiary to the analysis of aspects
-- Abstract_State
+ -- Always_Terminates
-- Attach_Handler
-- Contract_Cases
-- Depends
-- 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
-- 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
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 =>
-- 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
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 --
-----------------------------------------
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 --
--------------
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,
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,
-- 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,
-- 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,
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);
(Prag : Node_Id;
Do_Checks : Boolean := False) return Node_Id;
-- Subsidiary to the analysis of pragmas
+ -- Always_Terminates
-- Contract_Cases
-- Depends
-- Exceptional_Cases
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
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
-- 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
-- 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
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
Pragma_Abort_Defer,
Pragma_Abstract_State,
Pragma_All_Calls_Remote,
+ Pragma_Always_Terminates,
Pragma_Assert,
Pragma_Assert_And_Cut,
Pragma_Assume,
projects / thirdparty / gcc.git / commitdiff
