Aspect_Storage_Size,
Aspect_Stream_Size,
Aspect_String_Literal,
+ Aspect_Subprogram_Variant, -- GNAT
Aspect_Suppress,
Aspect_Synchronization,
Aspect_Test_Case, -- GNAT
Aspect_Storage_Size => Expression,
Aspect_Stream_Size => Expression,
Aspect_String_Literal => Name,
+ Aspect_Subprogram_Variant => Expression,
Aspect_Suppress => Name,
Aspect_Synchronization => Name,
Aspect_Test_Case => Expression,
Aspect_Storage_Size => True,
Aspect_Stream_Size => True,
Aspect_String_Literal => False,
+ Aspect_Subprogram_Variant => False,
Aspect_Suppress => False,
Aspect_Synchronization => False,
Aspect_Test_Case => False,
Aspect_Storage_Size => Name_Storage_Size,
Aspect_Stream_Size => Name_Stream_Size,
Aspect_String_Literal => Name_String_Literal,
+ Aspect_Subprogram_Variant => Name_Subprogram_Variant,
Aspect_Suppress => Name_Suppress,
Aspect_Suppress_Debug_Info => Name_Suppress_Debug_Info,
Aspect_Suppress_Initialization => Name_Suppress_Initialization,
Aspect_Relaxed_Initialization => Never_Delay,
Aspect_SPARK_Mode => Never_Delay,
Aspect_Static => Never_Delay,
+ Aspect_Subprogram_Variant => Never_Delay,
Aspect_Synchronization => Never_Delay,
Aspect_Test_Case => Never_Delay,
Aspect_Unimplemented => 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, invariants and predicates. Body_Id denotes the
- -- entity of the subprogram body.
+ -- well as Contract_Cases, Subprogram_Variant, invariants and predicates.
+ -- Body_Id denotes the entity of the subprogram body.
-----------------------
-- Add_Contract_Item --
then
Add_Classification;
- elsif Prag_Nam in Name_Contract_Cases | Name_Test_Case then
+ elsif Prag_Nam in Name_Contract_Cases
+ | Name_Subprogram_Variant
+ | Name_Test_Case
+ then
Add_Contract_Test_Case;
elsif Prag_Nam in Name_Postcondition | Name_Precondition then
end if;
-- Deal with preconditions, [refined] postconditions, Contract_Cases,
- -- invariants and predicates associated with body and its spec. Do not
- -- expand the contract of subprogram body stubs.
+ -- 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);
else
Analyze_Contract_Cases_In_Decl_Part (Prag, Freeze_Id);
end if;
+
+ elsif Prag_Nam = Name_Subprogram_Variant then
+ Analyze_Subprogram_Variant_In_Decl_Part (Prag);
+
else
pragma Assert (Prag_Nam = Name_Test_Case);
Analyze_Test_Case_In_Decl_Part (Prag);
Stmts : List_Id;
Result : Entity_Id)
is
- procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id);
- -- Insert node Stmt before the first source declaration of the
- -- related subprogram's body. If no such declaration exists, Stmt
- -- becomes the last declaration.
-
- --------------------------------------------
- -- Insert_Before_First_Source_Declaration --
- --------------------------------------------
-
- procedure Insert_Before_First_Source_Declaration (Stmt : Node_Id) is
- Decls : constant List_Id := Declarations (Body_Decl);
- Decl : Node_Id;
-
- begin
- -- Inspect the declarations of the related subprogram body looking
- -- for the first source declaration.
-
- if Present (Decls) then
- Decl := First (Decls);
- while Present (Decl) loop
- if Comes_From_Source (Decl) then
- Insert_Before (Decl, Stmt);
- return;
- end if;
-
- Next (Decl);
- end loop;
-
- -- If we get there, then the subprogram body lacks any source
- -- declarations. The body of _Postconditions now acts as the
- -- last declaration.
-
- Append (Stmt, Decls);
-
- -- Ensure that the body has a declaration list
-
- else
- Set_Declarations (Body_Decl, New_List (Stmt));
- end if;
- end Insert_Before_First_Source_Declaration;
-
- -- Local variables
-
Loc : constant Source_Ptr := Sloc (Body_Decl);
Params : List_Id := No_List;
Proc_Bod : Node_Id;
Proc_Id : Entity_Id;
Proc_Spec : Node_Id;
- -- Start of processing for Build_Postconditions_Procedure
-
begin
-- Nothing to do if there are no actions to check on exit
-- order reference. The body of _Postconditions must be placed after
-- the declaration of Temp to preserve correct visibility.
- Insert_Before_First_Source_Declaration (Proc_Decl);
+ Insert_Before_First_Source_Declaration
+ (Proc_Decl, Declarations (Body_Decl));
Analyze (Proc_Decl);
-- Set an explicit End_Label to override the sloc of the implicit
if Present (Items) then
Prag := Contract_Test_Cases (Items);
while Present (Prag) loop
- if Pragma_Name (Prag) = Name_Contract_Cases
- and then Is_Checked (Prag)
- then
- Expand_Pragma_Contract_Cases
- (CCs => Prag,
- Subp_Id => Subp_Id,
- Decls => Declarations (Body_Decl),
- Stmts => Stmts);
+ if Is_Checked (Prag) then
+ if Pragma_Name (Prag) = Name_Contract_Cases then
+ Expand_Pragma_Contract_Cases
+ (CCs => Prag,
+ Subp_Id => Subp_Id,
+ Decls => Declarations (Body_Decl),
+ Stmts => Stmts);
+
+ elsif Pragma_Name (Prag) = Name_Subprogram_Variant then
+ Expand_Pragma_Subprogram_Variant
+ (Prag => Prag,
+ Subp_Id => Subp_Id,
+ Body_Decls => Declarations (Body_Decl));
+ end if;
end if;
Prag := Next_Pragma (Prag);
-- subprogram body Body_Id as if they appeared at the end of a declarative
-- region. Pragmas in question are:
--
- -- Contract_Cases (stand alone subprogram body)
- -- Depends (stand alone subprogram body)
- -- Global (stand alone subprogram body)
- -- Postcondition (stand alone subprogram body)
- -- Precondition (stand alone subprogram body)
+ -- Contract_Cases (stand alone subprogram body)
+ -- Depends (stand alone subprogram body)
+ -- Global (stand alone subprogram body)
+ -- Postcondition (stand alone subprogram body)
+ -- Precondition (stand alone subprogram body)
-- Refined_Depends
-- Refined_Global
-- Refined_Post
- -- Test_Case (stand alone subprogram body)
+ -- Subprogram_Variant (stand alone subprogram body)
+ -- Test_Case (stand alone subprogram body)
procedure Analyze_Entry_Or_Subprogram_Contract
(Subp_Id : Entity_Id;
-- Global
-- Postcondition
-- Precondition
+ -- Subprogram_Variant
-- Test_Case
--
-- Freeze_Id is the entity of a [generic] package body or a [generic]
Id = Pragma_Refined_State or else
Id = Pragma_Volatile_Function;
- -- Contract / test case pragmas
+ -- Contract / subprogram variant / test case pragmas
Is_CTC : constant Boolean :=
Id = Pragma_Contract_Cases or else
+ Id = Pragma_Subprogram_Variant or else
Id = Pragma_Test_Case;
-- Pre / postcondition pragmas
-- Refined_Global
-- Refined_Post
-- Refined_State
+ -- Subprogram_Variant
-- Test_Case
-- Volatile_Function
-- though useless predicate checks will be generally removed by
-- back-end optimizations.
+ procedure Check_Subprogram_Variant;
+ -- Emit a call to the internally generated procedure with checks for
+ -- aspect Subprogrgram_Variant, if present and enabled.
+
function Inherited_From_Formal (S : Entity_Id) return Entity_Id;
-- Within an instance, a type derived from an untagged formal derived
-- type inherits from the original parent, not from the actual. The
end if;
end Can_Fold_Predicate_Call;
+ ------------------------------
+ -- Check_Subprogram_Variant --
+ ------------------------------
+
+ procedure Check_Subprogram_Variant is
+ Variant_Prag : constant Node_Id :=
+ Get_Pragma (Current_Scope, Pragma_Subprogram_Variant);
+
+ Variant_Proc : Entity_Id;
+
+ begin
+ if Present (Variant_Prag) and then Is_Checked (Variant_Prag) then
+
+ -- Analysis of the pragma rewrites its argument with a reference
+ -- to the internally generated procedure.
+
+ Variant_Proc :=
+ Entity
+ (Expression
+ (First
+ (Pragma_Argument_Associations (Variant_Prag))));
+
+ Insert_Action (Call_Node,
+ Make_Procedure_Call_Statement (Loc,
+ Name =>
+ New_Occurrence_Of (Variant_Proc, Loc),
+ Parameter_Associations =>
+ New_Copy_List (Parameter_Associations (Call_Node))));
+ end if;
+ end Check_Subprogram_Variant;
+
---------------------------
-- Inherited_From_Formal --
---------------------------
Expand_Actuals (Call_Node, Subp, Post_Call);
+ -- If it is a recursive call then call the internal procedure that
+ -- verifies Subprogram_Variant contract (if present and enabled).
+ -- Detecting calls to subprogram aliases is necessary for recursive
+ -- calls in instances of generic subprograms, where the renaming of
+ -- the current subprogram is called.
+
+ if Is_Subprogram (Subp)
+ and then Same_Or_Aliased_Subprograms (Subp, Current_Scope)
+ then
+ Check_Subprogram_Variant;
+ end if;
+
-- Verify that the actuals do not share storage. This check must be done
-- on the caller side rather that inside the subprogram to avoid issues
-- of parameter passing.
---------------------
procedure Process_Variant (Variant : Node_Id; Is_Last : Boolean) is
- function Make_Op
- (Loc : Source_Ptr;
- Curr_Val : Node_Id;
- Old_Val : Node_Id) return Node_Id;
- -- Generate a comparison between Curr_Val and Old_Val depending on
- -- the change mode (Increases / Decreases) of the variant.
-
- -------------
- -- Make_Op --
- -------------
-
- function Make_Op
- (Loc : Source_Ptr;
- Curr_Val : Node_Id;
- Old_Val : Node_Id) return Node_Id
- is
- begin
- if Chars (Variant) = Name_Increases then
- return Make_Op_Gt (Loc, Curr_Val, Old_Val);
- else pragma Assert (Chars (Variant) = Name_Decreases);
- return Make_Op_Lt (Loc, Curr_Val, Old_Val);
- end if;
- end Make_Op;
-
- -- Local variables
-
Expr : constant Node_Id := Expression (Variant);
Expr_Typ : constant Entity_Id := Etype (Expr);
Loc : constant Source_Ptr := Sloc (Expr);
Old_Id : Entity_Id;
Prag : Node_Id;
- -- Start of processing for Process_Variant
-
begin
-- All temporaries generated in this routine must be inserted before
-- the related loop statement. Ensure that the proper scope is on the
Expression => Make_Identifier (Loc, Name_Loop_Variant)),
Make_Pragma_Argument_Association (Loc,
Expression =>
- Make_Op (Loc,
+ Make_Variant_Comparison (Loc,
+ Mode => Chars (Variant),
Curr_Val => New_Occurrence_Of (Curr_Id, Loc),
Old_Val => New_Occurrence_Of (Old_Id, Loc)))));
end if;
end Expand_Pragma_Relative_Deadline;
+ --------------------------------------
+ -- Expand_Pragma_Subprogram_Variant --
+ --------------------------------------
+
+ -- Aspect Subprogram_Variant is expanded in the following manner:
+
+ -- Original code
+
+ -- procedure Proc (Param : T) with
+ -- with Variant (Increases => Incr_Expr,
+ -- Decreases => Decr_Expr)
+ -- <declarations>
+ -- is
+ -- <source statements>
+ -- Proc (New_Param_Value);
+ -- end Proc;
+
+ -- Expanded code
+
+ -- procedure Proc (Param : T) is
+ -- Old_Incr : constant <type of Incr_Expr> := <Incr_Expr>;
+ -- Old_Decr : constant <type of Decr_Expr> := <Decr_Expr> ;
+ --
+ -- procedure Variants (Param : T);
+ --
+ -- procedure Variants (Param : T) is
+ -- Curr_Incr : constant <type of Incr_Expr> := <Incr_Expr>;
+ -- Curr_Decr : constant <type of Decr_Expr> := <Decr_Expr>;
+ -- begin
+ -- if Curr_Incr /= Old_Incr then
+ -- pragma Check (Variant, Curr_Incr > Old_Incr);
+ -- else
+ -- pragma Check (Variant, Curr_Decr < Old_Decr);
+ -- end if;
+ -- end Variants;
+ --
+ -- <declarations>
+ -- begin
+ -- <source statements>
+ -- Variants (New_Param_Value);
+ -- Proc (New_Param_Value);
+ -- end Proc;
+
+ procedure Expand_Pragma_Subprogram_Variant
+ (Prag : Node_Id;
+ Subp_Id : Node_Id;
+ Body_Decls : List_Id)
+ is
+ Curr_Decls : List_Id;
+ If_Stmt : Node_Id := Empty;
+
+ function Formal_Param_Map
+ (Old_Subp : Entity_Id;
+ New_Subp : Entity_Id) return Elist_Id;
+ -- Given two subprogram entities Old_Subp and New_Subp with the same
+ -- number of formal parameters return a list of the form:
+ --
+ -- old formal 1
+ -- new formal 1
+ -- old formal 2
+ -- new formal 2
+ -- ...
+ --
+ -- as required by New_Copy_Tree to replace references to formal
+ -- parameters of Old_Subp with references to formal parameters of
+ -- New_Subp.
+
+ procedure Process_Variant
+ (Variant : Node_Id;
+ Formal_Map : Elist_Id;
+ Prev_Decl : in out Node_Id;
+ Is_Last : Boolean);
+ -- Process a single increasing / decreasing termination variant given by
+ -- a component association Variant. Formal_Map is a list of formal
+ -- parameters of the annotated subprogram and of the internal procedure
+ -- that verifies the variant in the format required by New_Copy_Tree.
+ -- The Old_... object created by this routine will be appended after
+ -- Prev_Decl and is stored in this parameter for a next call to this
+ -- routine. Is_Last is True when there are no more variants to process.
+
+ ----------------------
+ -- Formal_Param_Map --
+ ----------------------
+
+ function Formal_Param_Map
+ (Old_Subp : Entity_Id;
+ New_Subp : Entity_Id) return Elist_Id
+ is
+ Old_Formal : Entity_Id := First_Formal (Old_Subp);
+ New_Formal : Entity_Id := First_Formal (New_Subp);
+
+ Param_Map : Elist_Id;
+ begin
+ if Present (Old_Formal) then
+ Param_Map := New_Elmt_List;
+ while Present (Old_Formal) and then Present (New_Formal) loop
+ Append_Elmt (Old_Formal, Param_Map);
+ Append_Elmt (New_Formal, Param_Map);
+
+ Next_Formal (Old_Formal);
+ Next_Formal (New_Formal);
+ end loop;
+
+ return Param_Map;
+ else
+ return No_Elist;
+ end if;
+ end Formal_Param_Map;
+
+ ---------------------
+ -- Process_Variant --
+ ---------------------
+
+ procedure Process_Variant
+ (Variant : Node_Id;
+ Formal_Map : Elist_Id;
+ Prev_Decl : in out Node_Id;
+ Is_Last : Boolean)
+ is
+ Expr : constant Node_Id := Expression (Variant);
+ Expr_Typ : constant Entity_Id := Etype (Expr);
+ Loc : constant Source_Ptr := Sloc (Expr);
+
+ Old_Id : Entity_Id;
+ Old_Decl : Node_Id;
+ Curr_Id : Entity_Id;
+ Curr_Decl : Node_Id;
+ Prag : Node_Id;
+
+ begin
+ -- Create temporaries that store the old values of the associated
+ -- expression.
+
+ -- Generate:
+ -- Old : constant <type of Expr> := <Expr>;
+
+ Old_Id := Make_Temporary (Loc, 'P');
+
+ Old_Decl :=
+ Make_Object_Declaration (Loc,
+ Defining_Identifier => Old_Id,
+ Constant_Present => True,
+ Object_Definition => New_Occurrence_Of (Expr_Typ, Loc),
+ Expression => New_Copy_Tree (Expr));
+
+ Insert_After_And_Analyze (Prev_Decl, Old_Decl);
+
+ Prev_Decl := Old_Decl;
+
+ -- Generate:
+ -- Curr : constant <type of Expr> := <Expr>;
+
+ Curr_Id := Make_Temporary (Loc, 'C');
+
+ Curr_Decl :=
+ Make_Object_Declaration (Loc,
+ Defining_Identifier => Curr_Id,
+ Constant_Present => True,
+ Object_Definition => New_Occurrence_Of (Expr_Typ, Loc),
+ Expression =>
+ New_Copy_Tree (Expr, Map => Formal_Map));
+
+ Append (Curr_Decl, Curr_Decls);
+
+ -- Generate:
+ -- pragma Check (Variant, Curr <|> Old);
+
+ Prag :=
+ Make_Pragma (Loc,
+ Chars => Name_Check,
+ Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression =>
+ Make_Identifier (Loc,
+ Name_Subprogram_Variant)),
+ Make_Pragma_Argument_Association (Loc,
+ Expression =>
+ Make_Variant_Comparison (Loc,
+ Mode => Chars (First (Choices (Variant))),
+ Curr_Val => New_Occurrence_Of (Curr_Id, Loc),
+ Old_Val => New_Occurrence_Of (Old_Id, Loc)))));
+
+ -- Generate:
+ -- if Curr /= Old then
+ -- <Prag>;
+
+ if No (If_Stmt) then
+
+ -- When there is just one termination variant, do not compare
+ -- the old and current value for equality, just check the
+ -- pragma.
+
+ if Is_Last then
+ If_Stmt := Prag;
+ else
+ If_Stmt :=
+ Make_If_Statement (Loc,
+ Condition =>
+ Make_Op_Ne (Loc,
+ Left_Opnd => New_Occurrence_Of (Curr_Id, Loc),
+ Right_Opnd => New_Occurrence_Of (Old_Id, Loc)),
+ Then_Statements => New_List (Prag));
+ end if;
+
+ -- Generate:
+ -- else
+ -- <Prag>;
+ -- end if;
+
+ elsif Is_Last then
+ Set_Else_Statements (If_Stmt, New_List (Prag));
+
+ -- Generate:
+ -- elsif Curr /= Old then
+ -- <Prag>;
+
+ else
+ if Elsif_Parts (If_Stmt) = No_List then
+ Set_Elsif_Parts (If_Stmt, New_List);
+ end if;
+
+ Append_To (Elsif_Parts (If_Stmt),
+ Make_Elsif_Part (Loc,
+ Condition =>
+ Make_Op_Ne (Loc,
+ Left_Opnd => New_Occurrence_Of (Curr_Id, Loc),
+ Right_Opnd => New_Occurrence_Of (Old_Id, Loc)),
+ Then_Statements => New_List (Prag)));
+ end if;
+ end Process_Variant;
+
+ -- Local variables
+
+ Loc : constant Source_Ptr := Sloc (Prag);
+
+ Aggr : Node_Id;
+ Formal_Map : Elist_Id;
+ Last : Node_Id;
+ Last_Variant : Node_Id;
+ Proc_Bod : Node_Id;
+ Proc_Decl : Node_Id;
+ Proc_Id : Entity_Id;
+ Proc_Spec : Node_Id;
+ Variant : Node_Id;
+
+ begin
+ -- Do nothing if pragma is not present or is disabled
+
+ if Is_Ignored (Prag) then
+ return;
+ end if;
+
+ Aggr := Expression (First (Pragma_Argument_Associations (Prag)));
+
+ -- The expansion of Subprogram Variant is quite distributed as it
+ -- produces various statements to capture and compare the arguments.
+ -- To preserve the original context, set the Is_Assertion_Expr flag.
+ -- This aids the Ghost legality checks when verifying the placement
+ -- of a reference to a Ghost entity.
+
+ In_Assertion_Expr := In_Assertion_Expr + 1;
+
+ -- Create declaration of the procedure that compares values of the
+ -- variant expressions captured at the start of subprogram with their
+ -- values at the recursive call of the subprogram.
+
+ Proc_Id := Make_Defining_Identifier (Loc, Name_uVariants);
+
+ Proc_Spec :=
+ Make_Procedure_Specification
+ (Loc,
+ Defining_Unit_Name => Proc_Id,
+ Parameter_Specifications => Copy_Parameter_List (Subp_Id));
+
+ Proc_Decl :=
+ Make_Subprogram_Declaration (Loc, Proc_Spec);
+
+ Insert_Before_First_Source_Declaration (Proc_Decl, Body_Decls);
+ Analyze (Proc_Decl);
+
+ -- Create a mapping between formals of the annotated subprogram (which
+ -- are used to compute values of the variant expression at the start of
+ -- subprogram) and formals of the internal procedure (which are used to
+ -- compute values of of the variant expression at the recursive call).
+
+ Formal_Map :=
+ Formal_Param_Map (Old_Subp => Subp_Id, New_Subp => Proc_Id);
+
+ -- Process invidual increasing / decreasing variants
+
+ Last := Proc_Decl;
+ Curr_Decls := New_List;
+ Last_Variant := Nlists.Last (Component_Associations (Aggr));
+
+ Variant := First (Component_Associations (Aggr));
+ while Present (Variant) loop
+ Process_Variant
+ (Variant => Variant,
+ Formal_Map => Formal_Map,
+ Prev_Decl => Last,
+ Is_Last => Variant = Last_Variant);
+ Next (Variant);
+ end loop;
+
+ -- Create a subprogram body with declarations of objects that capture
+ -- the current values of variant expressions at a recursive call and an
+ -- if-then-else statement that compares current with old values.
+
+ Proc_Bod :=
+ Make_Subprogram_Body (Loc,
+ Specification =>
+ Copy_Subprogram_Spec (Proc_Spec),
+ Declarations => Curr_Decls,
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (Loc,
+ Statements => New_List (If_Stmt),
+ End_Label => Make_Identifier (Loc, Chars (Proc_Id))));
+
+ Insert_After_And_Analyze (Last, Proc_Bod);
+
+ -- Restore assertion context
+
+ In_Assertion_Expr := In_Assertion_Expr - 1;
+
+ -- Rewrite the aspect expression, which is no longer needed, with
+ -- a reference to the procedure that has just been created. We will
+ -- generate a call to this procedure at each recursive call of the
+ -- subprogram that has been annotated with Subprogram_Variant.
+
+ Rewrite (Aggr, New_Occurrence_Of (Proc_Id, Loc));
+ end Expand_Pragma_Subprogram_Variant;
+
-------------------------------------------
-- Expand_Pragma_Suppress_Initialization --
-------------------------------------------
-- applies to package Pack_Id. N denotes the related package spec or
-- body.
+ procedure Expand_Pragma_Subprogram_Variant
+ (Prag : Node_Id;
+ Subp_Id : Entity_Id;
+ Body_Decls : List_Id);
+ -- Given pragma Subprogram_Variant Prag, create the circuitry needed
+ -- to evaluate variant expressions at the subprogram entry and at the
+ -- recursive call. Subp_Id is the related subprogram for which the pragma
+ -- applies and Body_Decls are its body declarations. On exit, the argument
+ -- of Prag is replaced with a reference to procedure with checks for the
+ -- variant expressions.
+
end Exp_Prag;
Constraints => List_Constr));
end Make_Subtype_From_Expr;
+ -----------------------------
+ -- Make_Variant_Comparison --
+ -----------------------------
+
+ function Make_Variant_Comparison
+ (Loc : Source_Ptr;
+ Mode : Name_Id;
+ Curr_Val : Node_Id;
+ Old_Val : Node_Id) return Node_Id
+ is
+ begin
+ if Mode = Name_Increases then
+ return Make_Op_Gt (Loc, Curr_Val, Old_Val);
+ else pragma Assert (Mode = Name_Decreases);
+ return Make_Op_Lt (Loc, Curr_Val, Old_Val);
+ end if;
+ end Make_Variant_Comparison;
+
---------------
-- Map_Types --
---------------
-- wide type. Set Related_Id to request an external name for the subtype
-- rather than an internal temporary.
+ function Make_Variant_Comparison
+ (Loc : Source_Ptr;
+ Mode : Name_Id;
+ Curr_Val : Node_Id;
+ Old_Val : Node_Id) return Node_Id;
+ -- Subsidiary to the expansion of pragmas Loop_Variant and
+ -- Subprogram_Variant. Generate a comparison between Curr_Val and Old_Val
+ -- depending on the variant mode (Increases / Decreases).
+
procedure Map_Types (Parent_Type : Entity_Id; Derived_Type : Entity_Id);
-- Establish the following mapping between the attributes of tagged parent
-- type Parent_Type and tagged derived type Derived_Type.
-- Refined_Global
-- Refined_Depends
-- Refined_Post
+ -- Subprogram_Variant
-- Test_Case
-- Unmodified
-- Unreferenced
| Name_Refined_Global
| Name_Refined_Depends
| Name_Refined_Post
+ | Name_Subprogram_Variant
| Name_Test_Case
| Name_Unmodified
| Name_Unreferenced
| Pragma_Storage_Unit
| Pragma_Stream_Convert
| Pragma_Subtitle
+ | Pragma_Subprogram_Variant
| Pragma_Suppress
| Pragma_Suppress_Debug_Info
| Pragma_Suppress_Exception_Locations
end if;
end Insert_Before_And_Analyze;
+ --------------------------------------------
+ -- Insert_Before_First_Source_Declaration --
+ --------------------------------------------
+
+ procedure Insert_Before_First_Source_Declaration
+ (Stmt : Node_Id;
+ Decls : List_Id)
+ is
+ Decl : Node_Id;
+ begin
+ -- Inspect the declarations of the related subprogram body looking for
+ -- the first source declaration.
+
+ pragma Assert (Present (Decls));
+
+ Decl := First (Decls);
+ while Present (Decl) loop
+ if Comes_From_Source (Decl) then
+ Insert_Before (Decl, Stmt);
+ return;
+ end if;
+
+ Next (Decl);
+ end loop;
+
+ -- If we get there, then the subprogram body lacks any source
+ -- declarations. The body of _Postconditions now acts as the
+ -- last declaration.
+
+ Append (Stmt, Decls);
+ end Insert_Before_First_Source_Declaration;
+
-----------------------------------
-- Insert_List_After_And_Analyze --
-----------------------------------
-- Suppress argument is present, then the analysis is done with the
-- specified check suppressed (can be All_Checks to suppress all checks).
+ procedure Insert_Before_First_Source_Declaration
+ (Stmt : Node_Id;
+ Decls : List_Id);
+ -- Insert node Stmt before the first source declaration of the related
+ -- subprogram's body. If no such declaration exists, Stmt becomes the last
+ -- declaration.
+
function External_Ref_In_Generic (E : Entity_Id) return Boolean;
-- Return True if we are in the context of a generic and E is
-- external (more global) to it.
-- Refined_Depends
-- Refined_Global
-- Refined_Post
+ -- Subprogram_Variant
-- Test_Case
-- Most package contract annotations utilize forward references to classify
-- Refined_Global
-- Refined_State
-- SPARK_Mode
+ -- Subprogram_Variant
-- Warnings
-- Insert pragma Prag such that it mimics the placement of a source
-- pragma of the same kind. Flag Is_Generic should be set when the
-- analyzed right now.
-- Note that there is a special handling for Pre, Post, Test_Case,
- -- Contract_Cases 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 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 whose corresponding
- -- pragmas take care of the delay.
+ -- Pre/Post/Test_Case/Contract_Cases/Subprogram_Variant whose
+ -- corresponding pragmas take care of the delay.
-- Pre/Post
Insert_Pragma (Aitem);
goto Continue;
+ -- Subprogram_Variant
+
+ when Aspect_Subprogram_Variant =>
+ 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;
+
-- Case 5: Special handling for aspects with an optional
-- boolean argument.
| Aspect_Refined_State
| Aspect_Relaxed_Initialization
| Aspect_SPARK_Mode
+ | Aspect_Subprogram_Variant
| Aspect_Test_Case
| Aspect_Unimplemented
| Aspect_Volatile_Function
procedure Ensure_Aggregate_Form (Arg : Node_Id);
-- Subsidiary routine to the processing of pragmas Abstract_State,
-- Contract_Cases, Depends, Global, Initializes, Refined_Depends,
- -- Refined_Global and Refined_State. Transform argument Arg into
- -- an aggregate if not one already. N_Null is never transformed.
- -- Arg may denote an aspect specification or a pragma argument
- -- association.
+ -- Refined_Global, Refined_State and Subprogram_Variant. Transform
+ -- argument Arg into an aggregate if not one already. N_Null is never
+ -- transformed. Arg may denote an aspect specification or a pragma
+ -- argument association.
procedure Error_Pragma (Msg : String);
pragma No_Return (Error_Pragma);
end if;
end Style_Checks;
+ ------------------------
+ -- Subprogram_Variant --
+ ------------------------
+
+ -- pragma Subprogram_Variant ( SUBPROGRAM_VARIANT_ITEM
+ -- {, SUBPROGRAM_VARIANT_ITEM } );
+
+ -- SUBPROGRAM_VARIANT_ITEM ::=
+ -- CHANGE_DIRECTION => discrete_EXPRESSION
+
+ -- CHANGE_DIRECTION ::= Increases | Decreases
+
+ -- Characteristics:
+
+ -- * Analysis - The annotation undergoes initial checks to verify
+ -- the legal placement and context. Secondary checks preanalyze the
+ -- expressions in:
+
+ -- Analyze_Subprogram_Variant_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_Subprogram_Variant => Subprogram_Variant : 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. Subprogram_Variant
+ -- 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 Subprogram_Variant 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 procedure is not
+ -- recursive.
+
+ 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;
+ return;
+ 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);
+ Ensure_Aggregate_Form (Get_Argument (N, Spec_Id));
+
+ -- Chain the pragma on the contract for further processing by
+ -- Analyze_Contract_Cases_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 Subprogram_Variant 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_Subprogram_Variant_In_Decl_Part (N);
+ end if;
+ end Subprogram_Variant;
+
--------------
-- Subtitle --
--------------
Set_Is_Analyzed_Pragma (N);
end Analyze_Refined_State_In_Decl_Part;
+ ---------------------------------------------
+ -- Analyze_Subprogram_Variant_In_Decl_Part --
+ ---------------------------------------------
+
+ -- WARNING: This routine manages Ghost regions. Return statements must be
+ -- replaced by gotos which jump to the end of the routine and restore the
+ -- Ghost mode.
+
+ procedure Analyze_Subprogram_Variant_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);
+
+ procedure Analyze_Variant (Variant : Node_Id);
+ -- Verify the legality of a single contract case
+
+ ---------------------
+ -- Analyze_Variant --
+ ---------------------
+
+ procedure Analyze_Variant (Variant : Node_Id) is
+ Direction : Node_Id;
+ Expr : Node_Id;
+ Errors : Nat;
+ Extra_Direction : Node_Id;
+
+ begin
+ if Nkind (Variant) /= N_Component_Association then
+ Error_Msg_N ("wrong syntax in subprogram variant", Variant);
+ return;
+ end if;
+
+ Direction := First (Choices (Variant));
+ Expr := Expression (Variant);
+
+ -- Each variant must have exactly one direction
+
+ Extra_Direction := Next (Direction);
+
+ if Present (Extra_Direction) then
+ Error_Msg_N
+ ("subprogram variant case must have exactly one direction",
+ Extra_Direction);
+ end if;
+
+ -- Check placement of OTHERS if available (SPARK RM 6.1.3(1))
+
+ if Nkind (Direction) = N_Identifier then
+ if Chars (Direction) /= Name_Decreases
+ and then
+ Chars (Direction) /= Name_Increases
+ then
+ Error_Msg_N ("wrong direction", Direction);
+ end if;
+ else
+ Error_Msg_N ("wrong syntax", Direction);
+ end if;
+
+ Errors := Serious_Errors_Detected;
+ Preanalyze_Assert_Expression (Expr, Any_Discrete);
+
+ -- Emit a clarification message when the variant 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;
+ end Analyze_Variant;
+
+ -- Local variables
+
+ Variants : 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
+
+ Variant : Node_Id;
+ Restore_Scope : Boolean := False;
+
+ -- Start of processing for Analyze_Subprogram_Variant_In_Decl_Part
+
+ 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);
+
+ -- Single and multiple contract cases must appear in aggregate form. If
+ -- this is not the case, then either the parser of the analysis of the
+ -- pragma failed to produce an aggregate.
+
+ pragma Assert (Nkind (Variants) = N_Aggregate);
+
+ if Present (Component_Associations (Variants)) then
+
+ -- Ensure that the formal parameters are visible when analyzing all
+ -- clauses. This falls out of the general rule of aspects pertaining
+ -- to subprogram declarations.
+
+ if not In_Open_Scopes (Spec_Id) then
+ Restore_Scope := True;
+ Push_Scope (Spec_Id);
+
+ if Is_Generic_Subprogram (Spec_Id) then
+ Install_Generic_Formals (Spec_Id);
+ else
+ Install_Formals (Spec_Id);
+ end if;
+ end if;
+
+ Variant := First (Component_Associations (Variants));
+ while Present (Variant) loop
+ Analyze_Variant (Variant);
+ Next (Variant);
+ end loop;
+
+ if Restore_Scope then
+ End_Scope;
+ end if;
+
+ -- Otherwise the pragma is illegal
+
+ else
+ Error_Msg_N ("wrong syntax for subprogram variant", N);
+ end if;
+
+ Set_Is_Analyzed_Pragma (N);
+
+ Restore_Ghost_Region (Saved_GM, Saved_IGR);
+ end Analyze_Subprogram_Variant_In_Decl_Part;
+
------------------------------------
-- Analyze_Test_Case_In_Decl_Part --
------------------------------------
Pragma_Storage_Unit => 0,
Pragma_Stream_Convert => 0,
Pragma_Style_Checks => 0,
+ Pragma_Subprogram_Variant => -1,
Pragma_Subtitle => 0,
Pragma_Suppress => 0,
Pragma_Suppress_All => 0,
| Name_Predicate
| Name_Refined_Post
| Name_Statement_Assertions
+ | Name_Subprogram_Variant
=>
return True;
-- the entity of [generic] package body or [generic] subprogram body which
-- caused "freezing" of the related contract where the pragma resides.
+ procedure Analyze_Subprogram_Variant_In_Decl_Part
+ (N : Node_Id;
+ Freeze_Id : Entity_Id := Empty);
+ -- Perform full analysis of delayed pragma Subprogram_Variant. 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_Test_Case_In_Decl_Part (N : Node_Id);
-- Perform preanalysis of pragma Test_Case
------------------
procedure Resolve_Call (N : Node_Id; Typ : Entity_Id) is
- function Same_Or_Aliased_Subprograms
- (S : Entity_Id;
- E : Entity_Id) return Boolean;
- -- Returns True if the subprogram entity S is the same as E or else
- -- S is an alias of E.
-
- ---------------------------------
- -- Same_Or_Aliased_Subprograms --
- ---------------------------------
-
- function Same_Or_Aliased_Subprograms
- (S : Entity_Id;
- E : Entity_Id) return Boolean
- is
- Subp_Alias : constant Entity_Id := Alias (S);
- begin
- return S = E or else (Present (Subp_Alias) and then Subp_Alias = E);
- end Same_Or_Aliased_Subprograms;
-
- -- Local variables
-
Loc : constant Source_Ptr := Sloc (N);
Subp : constant Node_Id := Name (N);
Body_Id : Entity_Id;
Rtype : Entity_Id;
Scop : Entity_Id;
- -- Start of processing for Resolve_Call
-
begin
-- Preserve relevant elaboration-related attributes of the context which
-- are no longer available or very expensive to recompute once analysis,
or else Nam = Name_Refined_Depends
or else Nam = Name_Refined_Global
or else Nam = Name_Refined_Post
+ or else Nam = Name_Subprogram_Variant
or else Nam = Name_Test_Case;
end Is_Subprogram_Contract_Annotation;
end if;
end Same_Object;
+ ---------------------------------
+ -- Same_Or_Aliased_Subprograms --
+ ---------------------------------
+
+ function Same_Or_Aliased_Subprograms
+ (S : Entity_Id;
+ E : Entity_Id) return Boolean
+ is
+ Subp_Alias : constant Entity_Id := Alias (S);
+ begin
+ return S = E or else (Present (Subp_Alias) and then Subp_Alias = E);
+ end Same_Or_Aliased_Subprograms;
+
---------------
-- Same_Type --
---------------
-- Refined_Depends
-- Refined_Global
-- Refined_Post
+ -- Subprogram_Variant
-- Test_Case
function Is_Subprogram_Stub_Without_Prior_Declaration
-- mean that different objects are designated, just that this could not
-- be reliably determined at compile time.
+ function Same_Or_Aliased_Subprograms
+ (S : Entity_Id;
+ E : Entity_Id) return Boolean;
+ -- Returns True if the subprogram entity S is the same as E or else S is an
+ -- alias of E.
+
function Same_Type (T1, T2 : Entity_Id) return Boolean;
-- Determines if T1 and T2 represent exactly the same type. Two types
-- are the same if they are identical, or if one is an unconstrained
-- operation) are also in this list.
-- Contract_Test_Cases contains a collection of pragmas that correspond
- -- to aspects/pragmas Contract_Cases and Test_Case. The ordering in the
- -- list is in LIFO fashion.
+ -- to aspects/pragmas Contract_Cases, Test_Case and Subprogram_Variant.
+ -- The ordering in the list is in LIFO fashion.
-- Classifications contains pragmas that either declare, categorize, or
-- establish dependencies between subprogram or package inputs and
Name_uTask_Name : constant Name_Id := N + $;
Name_uTrace_Sp : constant Name_Id := N + $;
Name_uType_Invariant : constant Name_Id := N + $;
+ Name_uVariants : constant Name_Id := N + $;
-- Names of predefined primitives used in the expansion of dispatching
-- requeue and select statements, Abort, 'Callable and 'Terminated.
Name_Source_Reference : constant Name_Id := N + $; -- GNAT
Name_Static_Elaboration_Desired : constant Name_Id := N + $; -- GNAT
Name_Stream_Convert : constant Name_Id := N + $; -- GNAT
+ Name_Subprogram_Variant : constant Name_Id := N + $; -- GNAT
Name_Subtitle : constant Name_Id := N + $; -- GNAT
Name_Suppress_All : constant Name_Id := N + $; -- GNAT
Name_Suppress_Debug_Info : constant Name_Id := N + $; -- GNAT
Pragma_Source_Reference,
Pragma_Static_Elaboration_Desired,
Pragma_Stream_Convert,
+ Pragma_Subprogram_Variant,
Pragma_Subtitle,
Pragma_Suppress_All,
Pragma_Suppress_Debug_Info,
projects / gcc.git / commitdiff