+2013-10-10 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * aspects.adb: Add an entry for Aspect_Refined_Post in table
+ Canonical_Aspect.
+ * aspects.ads: Add an entry for Aspect_Refined_Post in tables
+ Aspect_Id, Aspect_Argument, Aspect_Names, Aspect_Delay,
+ Aspect_On_Body_Or_Stub_OK. Update the comment on the use of
+ table Aspect_On_Body_Or_Stub_OK.
+ * par-prag.adb: Add pragma Refined_Post to the list of pragmas
+ that do not require special processing by the parser.
+ * sem_attr.adb (Analyze_Attribute): Add special analysis for
+ attributes 'Old and 'Result when code generation is disabled and
+ they appear in aspect/pragma Refined_Post.
+ (In_Refined_Post): New routine.
+ * sem_ch6.adb (Analyze_Expression_Function): Move various
+ aspects and/or pragmas that apply to an expression function to the
+ corresponding spec or body.
+ (Collect_Body_Postconditions): New routine.
+ (Process_PPCs): Use routine Collect_Body_Postconditions
+ to gather all postcondition pragmas.
+ * sem_ch10.adb (Analyze_Proper_Body): Use routine
+ Relocate_Pragmas_To_Body to move all source pragmas that follow
+ a body stub to the proper body.
+ (Move_Stub_Pragmas_To_Body): Removed.
+ * sem_ch13.adb (Analyze_Aspect_Specifications): Add processing
+ for aspect Refined_Post.
+ (Check_Aspect_At_Freeze_Point): Aspect
+ Refined_Post does not need delayed processing at the freeze point.
+ * sem_prag.adb: Add an entry for pragma Refined_Post in
+ table Sig_Flags.
+ (Analyze_Pragma): Add processing for pragma
+ Refined_Post. Update the processing of pragma Refined_Pre
+ to use common routine Analyze_Refined_Pre_Post.
+ (Analyze_Refined_Pre_Post): New routine.
+ (Relocate_Pragmas_To_Body): New routine.
+ * sem_prag.ads: Table Pragma_On_Stub_OK is now known as
+ Pragma_On_Body_Or_Stub_OK. Update the comment on usage of
+ table Pragma_On_Body_Or_Stub_OK.
+ (Relocate_Pragmas_To_Body): New routine.
+ * snames.ads-tmpl: Add new predefined name for Refined_Post. Add
+ new Pragma_Id for Refined_Post.
+
+2013-10-10 Robert Dewar <dewar@adacore.com>
+
+ * exp_ch3.adb (Expand_N_Variant_Part): Now null, expansion of
+ last choice to others is moved to Freeze_Record_Type.
+ * freeze.adb (Freeze_Record_Type): Expand last variant to others
+ if necessary (moved here from Expand_N_Variant_Part
+
2013-10-10 Robert Dewar <dewar@adacore.com>
* lib-xref-spark_specific.adb, par-ch13.adb, sem_prag.adb, sem_prag.ads,
Aspect_Pure_05 => Aspect_Pure_05,
Aspect_Pure_12 => Aspect_Pure_12,
Aspect_Pure_Function => Aspect_Pure_Function,
+ Aspect_Refined_Post => Aspect_Refined_Post,
Aspect_Refined_Pre => Aspect_Refined_Pre,
Aspect_Remote_Access_Type => Aspect_Remote_Access_Type,
Aspect_Remote_Call_Interface => Aspect_Remote_Call_Interface,
Aspect_Predicate, -- GNAT
Aspect_Priority,
Aspect_Read,
+ Aspect_Refined_Post, -- GNAT
Aspect_Refined_Pre, -- GNAT
Aspect_Relative_Deadline,
Aspect_Scalar_Storage_Order, -- GNAT
Aspect_Predicate => Expression,
Aspect_Priority => Expression,
Aspect_Read => Name,
+ Aspect_Refined_Post => Expression,
Aspect_Refined_Pre => Expression,
Aspect_Relative_Deadline => Expression,
Aspect_Scalar_Storage_Order => Expression,
Aspect_Pure_12 => Name_Pure_12,
Aspect_Pure_Function => Name_Pure_Function,
Aspect_Read => Name_Read,
+ Aspect_Refined_Post => Name_Refined_Post,
Aspect_Refined_Pre => Name_Refined_Pre,
Aspect_Relative_Deadline => Name_Relative_Deadline,
Aspect_Remote_Access_Type => Name_Remote_Access_Type,
Aspect_Convention => Never_Delay,
Aspect_Dimension => Never_Delay,
Aspect_Dimension_System => Never_Delay,
+ Aspect_Refined_Post => Never_Delay,
Aspect_Refined_Pre => Never_Delay,
Aspect_SPARK_Mode => Never_Delay,
Aspect_Synchronization => Never_Delay,
-- package P with SPARK_Mode ...;
-- package body P with SPARK_Mode is ...;
+ -- The table should be synchronized with Pragma_On_Body_Or_Stub_OK in unit
+ -- Sem_Prag if the aspects below are implemented by a pragma.
+
Aspect_On_Body_Or_Stub_OK : constant array (Aspect_Id) of Boolean :=
- (Aspect_Refined_Pre => True,
+ (Aspect_Refined_Post => True,
+ Aspect_Refined_Pre => True,
Aspect_SPARK_Mode => True,
Aspect_Warnings => True,
others => False);
-- Expand_N_Variant_Part --
---------------------------
- procedure Expand_N_Variant_Part (N : Node_Id) is
- Last_Var : constant Node_Id := Last_Non_Pragma (Variants (N));
- Others_Node : Node_Id;
+ -- Note: this procedure no longer has any effect. It used to be that we
+ -- would replace the choices in the last variant by a when others, and
+ -- also expanded static predicates in variant choices here, but both of
+ -- those activities were being done too early, since we can't check the
+ -- choices until the statically predicated subtypes are frozen, which can
+ -- happen as late as the free point of the record, and we can't change the
+ -- last choice to an others before checking the choices, which is now done
+ -- at the freeze point of the record.
+ procedure Expand_N_Variant_Part (N : Node_Id) is
begin
- -- If the last variant does not contain the Others choice, replace it
- -- with an N_Others_Choice node since Gigi always wants an Others. Note
- -- that we do not bother to call Analyze on the modified variant part,
- -- since its only effect would be to compute the Others_Discrete_Choices
- -- node laboriously, and of course we already know the list of choices
- -- corresponding to the others choice (it's the list we're replacing!)
-
- if Nkind (First (Discrete_Choices (Last_Var))) /= N_Others_Choice then
- Others_Node := Make_Others_Choice (Sloc (Last_Var));
- Set_Others_Discrete_Choices
- (Others_Node, Discrete_Choices (Last_Var));
- Set_Discrete_Choices (Last_Var, New_List (Others_Node));
- end if;
-
- -- We have one more expansion activity, which is to deal with static
- -- predicates in the variant choices. But we have to defer that to
- -- the freeze point, because the statically predicated subtype won't
- -- be fully processed till then, so this expansion activity is carried
- -- out in Freeze_Record_Type.
-
+ null;
end Expand_N_Variant_Part;
---------------------------------
C : Node_Id;
V : Node_Id;
- Others_Present : Boolean;
+ Others_Present : Boolean;
pragma Warnings (Off, Others_Present);
-- Indicates others present, not used in this case
end if;
end if;
- -- If we have a variant part, check choices
+ -- Case of variant part present
if Present (C) and then Present (Variant_Part (C)) then
V := Variant_Part (C);
+
+ -- Check choices
+
Check_Choices
(V, Variants (V), Etype (Name (V)), Others_Present);
+
+ -- If the last variant does not contain the Others choice,
+ -- replace it with an N_Others_Choice node since Gigi always
+ -- wants an Others. Note that we do not bother to call Analyze
+ -- on the modified variant part, since its only effect would be
+ -- to compute the Others_Discrete_Choices node laboriously, and
+ -- of course we already know the list of choices corresponding
+ -- to the others choice (it's the list we're replacing!)
+
+ declare
+ Last_Var : constant Node_Id :=
+ Last_Non_Pragma (Variants (V));
+ Others_Node : Node_Id;
+ begin
+ if Nkind (First (Discrete_Choices (Last_Var))) /=
+ N_Others_Choice
+ then
+ Others_Node := Make_Others_Choice (Sloc (Last_Var));
+ Set_Others_Discrete_Choices
+ (Others_Node, Discrete_Choices (Last_Var));
+ Set_Discrete_Choices (Last_Var, New_List (Others_Node));
+ end if;
+ end;
end if;
end Check_Variant_Part;
end Freeze_Record_Type;
Pragma_Pure_12 |
Pragma_Pure_Function |
Pragma_Queuing_Policy |
+ Pragma_Refined_Post |
Pragma_Refined_Pre |
Pragma_Relative_Deadline |
Pragma_Remote_Access_Type |
-- Verify that prefix of attribute N is a float type and that
-- two attribute expressions are present
- procedure Legal_Formal_Attribute;
- -- Common processing for attributes Definite and Has_Discriminants.
- -- Checks that prefix is generic indefinite formal type.
-
procedure Check_SPARK_Restriction_On_Attribute;
-- Issue an error in formal mode because attribute N is allowed
pragma No_Return (Error_Attr);
-- Like Error_Attr, but error is posted at the start of the prefix
+ function In_Refined_Post return Boolean;
+ -- Determine whether the current attribute appears in pragma
+ -- Refined_Post.
+
+ procedure Legal_Formal_Attribute;
+ -- Common processing for attributes Definite and Has_Discriminants.
+ -- Checks that prefix is generic indefinite formal type.
+
procedure Standard_Attribute (Val : Int);
-- Used to process attributes whose prefix is package Standard which
-- yield values of type Universal_Integer. The attribute reference
Error_Attr;
end Error_Attr_P;
+ ---------------------
+ -- In_Refined_Post --
+ ---------------------
+
+ function In_Refined_Post return Boolean is
+ function Is_Refined_Post (Prag : Node_Id) return Boolean;
+ -- Determine whether Prag denotes one of the incarnations of pragma
+ -- Refined_Post (either as is or pragma Check (Refined_Post, ...).
+
+ ---------------------
+ -- Is_Refined_Post --
+ ---------------------
+
+ function Is_Refined_Post (Prag : Node_Id) return Boolean is
+ Args : constant List_Id := Pragma_Argument_Associations (Prag);
+ Nam : constant Name_Id := Pragma_Name (Prag);
+
+ begin
+ if Nam = Name_Refined_Post then
+ return True;
+
+ elsif Nam = Name_Check then
+ pragma Assert (Present (Args));
+
+ return Chars (Expression (First (Args))) = Name_Refined_Post;
+ end if;
+
+ return False;
+ end Is_Refined_Post;
+
+ -- Local variables
+
+ Stmt : Node_Id;
+
+ -- Start of processing for In_Refined_Post
+
+ begin
+ Stmt := Parent (N);
+ while Present (Stmt) loop
+ if Nkind (Stmt) = N_Pragma and then Is_Refined_Post (Stmt) then
+ return True;
+
+ -- Prevent the search from going too far
+
+ elsif Is_Body_Or_Package_Declaration (Stmt) then
+ exit;
+ end if;
+
+ Stmt := Parent (Stmt);
+ end loop;
+
+ return False;
+ end In_Refined_Post;
+
----------------------------
-- Legal_Formal_Attribute --
----------------------------
Error_Attr ("% attribute can only appear in postcondition", P);
end if;
- -- Body case, where we must be inside a generated _Postcondition
+ -- Check the legality of attribute 'Old when it appears inside pragma
+ -- Refined_Post. These specialized checks are required only when code
+ -- generation is disabled. In the general case pragma Refined_Post is
+ -- transformed into pragma Check by Process_PPCs which in turn is
+ -- relocated to procedure _Postconditions. From then on the legality
+ -- of 'Old is determined as usual.
+
+ elsif not Expander_Active and then In_Refined_Post then
+ Preanalyze_And_Resolve (P);
+ P_Type := Etype (P);
+ Set_Etype (N, P_Type);
+
+ if Is_Limited_Type (P_Type) then
+ Error_Attr ("attribute % cannot apply to limited objects", P);
+ end if;
+
+ if Is_Entity_Name (P)
+ and then Is_Constant_Object (Entity (P))
+ then
+ Error_Msg_N
+ ("??attribute Old applied to constant has no effect", P);
+ end if;
+
+ return;
+
+ -- Body case, where we must be inside a generated _Postconditions
-- procedure, or else the attribute use is definitely misplaced. The
-- postcondition itself may have generated transient scopes, and is
-- not necessarily the current one.
-- If the attribute reference is generated for a Requires clause,
-- then no expressions follow. Otherwise it is a primary, in which
- -- case, if expressions follow, the attribute reference must be
- -- an indexable object, so rewrite the node accordingly.
+ -- case, if expressions follow, the attribute reference must be an
+ -- indexable object, so rewrite the node accordingly.
if Present (E1) then
Rewrite (N,
Check_E0;
- -- Prefix has not been analyzed yet, and its full analysis will
- -- take place during expansion (see below).
+ -- Prefix has not been analyzed yet, and its full analysis will take
+ -- place during expansion (see below).
Preanalyze_And_Resolve (P);
P_Type := Etype (P);
Set_Is_Overloaded (P, False);
end if;
- -- Body case, where we must be inside a generated _Postcondition
+ -- Check the legality of attribute 'Result when it appears inside
+ -- pragma Refined_Post. These specialized checks are required only
+ -- when code generation is disabled. In the general case pragma
+ -- Refined_Post is transformed into pragma Check by Process_PPCs
+ -- which in turn is relocated to procedure _Postconditions. From
+ -- then on the legality of 'Result is determined as usual.
+
+ elsif not Expander_Active and then In_Refined_Post then
+ PS := Current_Scope;
+
+ -- The prefix denotes the proper related function
+
+ if Is_Entity_Name (P)
+ and then Ekind (Entity (P)) = E_Function
+ and then Entity (P) = PS
+ then
+ null;
+
+ else
+ Error_Msg_Name_2 := Chars (PS);
+ Error_Attr ("incorrect prefix for % attribute, expected %", P);
+ end if;
+
+ Set_Etype (N, Etype (PS));
+
+ -- Body case, where we must be inside a generated _Postconditions
-- procedure, and the prefix must be on the scope stack, or else the
-- attribute use is definitely misplaced. The postcondition itself
-- may have generated transient scopes, and is not necessarily the
null;
else
- Error_Msg_NE
- ("incorrect prefix for % attribute, expected &", P, PS);
- Error_Attr;
+ Error_Msg_Name_2 := Chars (PS);
+ Error_Attr
+ ("incorrect prefix for % attribute, expected %", P);
end if;
Rewrite (N, Make_Identifier (Sloc (N), Name_uResult));
Subunit_Name : constant Unit_Name_Type := Get_Unit_Name (N);
Unum : Unit_Number_Type;
- procedure Move_Stub_Pragmas_To_Body (Bod : Node_Id);
- -- Relocate all pragmas that apply to a subprogram body stub to the
- -- declarations of proper body Bod.
- -- Should we do this for the reamining body stub kinds???
-
procedure Optional_Subunit;
-- This procedure is called when the main unit is a stub, or when we
-- are not generating code. In such a case, we analyze the subunit if
-- present, which is user-friendly and in fact required for ASIS, but
-- we don't complain if the subunit is missing.
- -------------------------------
- -- Move_Stub_Pragmas_To_Body --
- -------------------------------
-
- procedure Move_Stub_Pragmas_To_Body (Bod : Node_Id) is
- procedure Move_Pragma (Prag : Node_Id);
- -- Relocate one pragma to the declarations of Bod
-
- -----------------
- -- Move_Pragma --
- -----------------
-
- procedure Move_Pragma (Prag : Node_Id) is
- Decls : List_Id := Declarations (Bod);
-
- begin
- if No (Decls) then
- Decls := New_List;
- Set_Declarations (Bod, Decls);
- end if;
-
- -- Unhook the pragma from its current list
-
- Remove (Prag);
- Prepend (Prag, Decls);
- end Move_Pragma;
-
- -- Local variables
-
- Next_Stmt : Node_Id;
- Stmt : Node_Id;
-
- -- Start of processing for Move_Stub_Pragmas_To_Body
-
- begin
- pragma Assert (Nkind (N) = N_Subprogram_Body_Stub);
-
- -- Perform a bit of a lookahead - peek at any subsequent source
- -- pragmas while skipping internally generated code.
-
- Stmt := Next (N);
- while Present (Stmt) loop
- Next_Stmt := Next (Stmt);
-
- -- Move a source pragma that applies to a subprogram stub to the
- -- declarations of the proper body.
-
- if Comes_From_Source (Stmt)
- and then Nkind (Stmt) = N_Pragma
- and then Pragma_On_Stub_OK (Get_Pragma_Id (Stmt))
- then
- Move_Pragma (Stmt);
-
- -- Skip internally generated code
-
- elsif not Comes_From_Source (Stmt) then
- null;
-
- -- No valid pragmas are available for relocation
-
- else
- exit;
- end if;
-
- Stmt := Next_Stmt;
- end loop;
- end Move_Stub_Pragmas_To_Body;
-
----------------------
-- Optional_Subunit --
----------------------
Move_Or_Merge_Aspects (From => N, To => Prop_Body);
- -- Propagate all source pragmas associated with a
- -- subprogram body stub to the proper body.
+ -- Move all source pragmas that follow the body stub and
+ -- apply to it to the declarations of the proper body.
if Nkind (N) = N_Subprogram_Body_Stub then
- Move_Stub_Pragmas_To_Body (Prop_Body);
+ Relocate_Pragmas_To_Body (N, Target_Body => Prop_Body);
end if;
-- Analyze the unit if semantics active
Expression => Relocate_Node (Expr))),
Pragma_Name => Name_SPARK_Mode);
+ -- Refined_Post
+
+ when Aspect_Refined_Post =>
+ Make_Aitem_Pragma
+ (Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Relocate_Node (Expr))),
+ Pragma_Name => Name_Refined_Post);
+
-- Refined_Pre
when Aspect_Refined_Pre =>
Aspect_Postcondition |
Aspect_Pre |
Aspect_Precondition |
+ Aspect_Refined_Post |
Aspect_Refined_Pre |
Aspect_SPARK_Mode |
Aspect_Test_Case =>
Make_Handled_Sequence_Of_Statements (LocX,
Statements => New_List (Ret)));
+ -- If the expression completes a generic subprogram, we must create a
+ -- separate node for the body, because at instantiation the original
+ -- node of the generic copy must be a generic subprogram body, and
+ -- cannot be a expression function. Otherwise we just rewrite the
+ -- expression with the non-generic body.
+
if Present (Prev) and then Ekind (Prev) = E_Generic_Function then
+ Insert_After (N, New_Body);
- -- If the expression completes a generic subprogram, we must create a
- -- separate node for the body, because at instantiation the original
- -- node of the generic copy must be a generic subprogram body, and
- -- cannot be a expression function. Otherwise we just rewrite the
- -- expression with the non-generic body.
+ -- Propagate any aspects or pragmas that apply to the expression
+ -- function to the proper body when the expression function acts
+ -- as a completion.
+
+ if Has_Aspects (N) then
+ Move_Aspects (N, To => New_Body);
+ end if;
+
+ Relocate_Pragmas_To_Body (New_Body);
- Insert_After (N, New_Body);
Rewrite (N, Make_Null_Statement (Loc));
Set_Has_Completion (Prev, False);
Analyze (N);
Generate_Reference (Prev, Defining_Entity (N), 'b', Force => True);
Rewrite (N, New_Body);
+
+ -- Propagate any pragmas that apply to the expression function to the
+ -- proper body when the expression function acts as a completion.
+ -- Aspects are automatically transfered because of node rewriting.
+
+ Relocate_Pragmas_To_Body (N);
Analyze (N);
-- Prev is the previous entity with the same name, but it is can
-- under the same visibility conditions as for other invariant checks,
-- the type invariant must be applied to the returned value.
+ procedure Collect_Body_Postconditions (Post_Nam : Name_Id);
+ -- Examine the declarations of the body, looking for pragmas with name
+ -- Post_Nam. Parameter Post_Nam must denote either Name_Postcondition or
+ -- Name_Refined_Post. Chain any relevant postconditions to Plist.
+
function Grab_PPC (Pspec : Entity_Id := Empty) return Node_Id;
-- Prag contains an analyzed precondition or postcondition pragma. This
-- function copies the pragma, changes it to the corresponding Check
end if;
end Check_Access_Invariants;
+ ---------------------------------
+ -- Collect_Body_Postconditions --
+ ---------------------------------
+
+ procedure Collect_Body_Postconditions (Post_Nam : Name_Id) is
+ Next_Prag : Node_Id;
+
+ begin
+ pragma Assert
+ (Nam_In (Post_Nam, Name_Postcondition, Name_Refined_Post));
+
+ Prag := First (Declarations (N));
+ while Present (Prag) loop
+ Next_Prag := Next (Prag);
+
+ if Nkind (Prag) = N_Pragma then
+
+ -- Capture postcondition pragmas
+
+ if Pragma_Name (Prag) = Post_Nam then
+ Analyze (Prag);
+
+ -- All Refined_Post pragmas must be relocated to the body
+ -- of the generated _Postconditions routine, otherwise they
+ -- will be duplicated twice - once in the declarations of
+ -- the body and once in _Postconditions.
+
+ if Pragma_Name (Prag) = Name_Refined_Post then
+ Remove (Prag);
+ end if;
+
+ -- If expansion is disabled, as in a generic unit, save
+ -- pragma for later expansion.
+
+ if not Expander_Active then
+ Prepend (Grab_PPC, Declarations (N));
+ else
+ Append_Enabled_Item (Grab_PPC, Plist);
+ end if;
+ end if;
+
+ -- Skip internally generated code
+
+ elsif not Comes_From_Source (Prag) then
+ null;
+
+ else
+ exit;
+ end if;
+
+ Prag := Next_Prag;
+ end loop;
+ end Collect_Body_Postconditions;
+
--------------
-- Grab_PPC --
--------------
-- procedure _postconditions [(_Result : resulttype)] is
-- begin
+ -- pragma Check (Refined_Post, condition);
+ -- pragma Check (Refined_Post, condition);
-- pragma Check (Postcondition, condition [,message]);
-- pragma Check (Postcondition, condition [,message]);
-- ...
-- First we deal with the postconditions in the body
- if Is_Non_Empty_List (Declarations (N)) then
-
- -- Loop through declarations
-
- Prag := First (Declarations (N));
- while Present (Prag) loop
- if Nkind (Prag) = N_Pragma then
-
- -- Capture postcondition pragmas
-
- if Pragma_Name (Prag) = Name_Postcondition then
- Analyze (Prag);
-
- -- If expansion is disabled, as in a generic unit, save
- -- pragma for later expansion.
-
- if not Expander_Active then
- Prepend (Grab_PPC, Declarations (N));
- else
- Append_Enabled_Item (Grab_PPC, Plist);
- end if;
- end if;
-
- Next (Prag);
-
- -- Not a pragma, if comes from source, then end scan
-
- elsif Comes_From_Source (Prag) then
- exit;
-
- -- Skip stuff not coming from source
-
- else
- Next (Prag);
- end if;
- end loop;
- end if;
+ Collect_Body_Postconditions (Name_Refined_Post);
+ Collect_Body_Postconditions (Name_Postcondition);
-- Now deal with any postconditions from the spec
-- In Ada 95 or 05 mode, these are implementation defined pragmas, so
-- should be caught by the No_Implementation_Pragmas restriction.
+ procedure Analyze_Refined_Pre_Post
+ (Body_Decl : out Node_Id;
+ Spec_Id : out Entity_Id;
+ Legal : out Boolean);
+ -- Subsidiary routine to the analysis of pragmas Refined_Pre and
+ -- Refined_Post. Body_Decl is the declaration of the subprogram body
+ -- [stub] subject to the pragma. Spec_Id is the corresponding spec of
+ -- the subprogram body [stub]. Flag Legal denotes whether the pragma
+ -- passes all legality rules.
+
procedure Check_Ada_83_Warning;
-- Issues a warning message for the current pragma if operating in Ada
-- 83 mode (used for language pragmas that are not a standard part of
end if;
end Ada_2012_Pragma;
+ ------------------------------
+ -- Analyze_Refined_Pre_Post --
+ ------------------------------
+
+ procedure Analyze_Refined_Pre_Post
+ (Body_Decl : out Node_Id;
+ Spec_Id : out Entity_Id;
+ Legal : out Boolean)
+ is
+ Pack_Spec : Node_Id;
+ Spec_Decl : Node_Id;
+ Stmt : Node_Id;
+
+ begin
+ -- Assume that the pragma is illegal
+
+ Body_Decl := Parent (N);
+ Spec_Id := Empty;
+ Legal := False;
+
+ GNAT_Pragma;
+ Check_Arg_Count (1);
+ Check_No_Identifiers;
+
+ -- Verify the placement of the pragma and check for duplicates
+
+ Stmt := Prev (N);
+ while Present (Stmt) loop
+
+ -- Skip prior pragmas, but check for duplicates
+
+ if Nkind (Stmt) = N_Pragma then
+ if Pragma_Name (Stmt) = Pname then
+ Error_Msg_Name_1 := Pname;
+ Error_Msg_Sloc := Sloc (Stmt);
+ Error_Msg_N ("pragma % duplicates pragma declared #", N);
+ end if;
+
+ -- Emit an error when the pragma applies to an expression function
+ -- that does not act as a completion.
+
+ elsif Nkind (Stmt) = N_Subprogram_Declaration
+ and then Nkind (Original_Node (Stmt)) = N_Expression_Function
+ and then not
+ Has_Completion (Defining_Unit_Name (Specification (Stmt)))
+ then
+ Error_Pragma
+ ("pragma % cannot apply to a stand alone expression "
+ & "function");
+ return;
+
+ -- The pragma applies to a subprogram body stub
+
+ elsif Nkind (Stmt) = N_Subprogram_Body_Stub then
+ Body_Decl := Stmt;
+ exit;
+
+ -- Skip internally generated code
+
+ elsif not Comes_From_Source (Stmt) then
+ null;
+
+ -- The pragma does not apply to a legal construct, issue an error
+ -- and stop the analysis.
+
+ else
+ Pragma_Misplaced;
+ return;
+ end if;
+
+ Stmt := Prev (Stmt);
+ end loop;
+
+ -- Pragma Refined_Pre/Post must apply to a subprogram body [stub]
+
+ if not Nkind_In (Body_Decl, N_Subprogram_Body,
+ N_Subprogram_Body_Stub)
+ then
+ Pragma_Misplaced;
+ return;
+ end if;
+
+ -- The body [stub] must not act as a spec, in other words it has to
+ -- be paired with a corresponding spec.
+
+ if Nkind (Body_Decl) = N_Subprogram_Body then
+ Spec_Id := Corresponding_Spec (Body_Decl);
+ else
+ Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl);
+ end if;
+
+ if No (Spec_Id) then
+ Error_Pragma ("pragma % cannot apply to a stand alone body");
+ return;
+ end if;
+
+ -- Refined_Pre/Post may only apply to the body [stub] of a subprogram
+ -- declared in the visible part of a package. Retrieve the context of
+ -- the subprogram declaration.
+
+ Spec_Decl := Parent (Parent (Spec_Id));
+
+ pragma Assert
+ (Nkind_In (Spec_Decl, N_Abstract_Subprogram_Declaration,
+ N_Generic_Subprogram_Declaration,
+ N_Subprogram_Declaration));
+
+ Pack_Spec := Parent (Spec_Decl);
+
+ if Nkind (Pack_Spec) /= N_Package_Specification
+ or else List_Containing (Spec_Decl) /=
+ Visible_Declarations (Pack_Spec)
+ then
+ Error_Pragma
+ ("pragma % must apply to the body of a visible subprogram");
+ return;
+ end if;
+
+ -- If we get here, the placement and legality of the pragma is OK
+
+ Legal := True;
+ end Analyze_Refined_Pre_Post;
+
--------------------------
-- Check_Ada_83_Warning --
--------------------------
when Pragma_Rational =>
Set_Rational_Profile;
- -----------------
- -- Refined_Pre --
- -----------------
+ ------------------
+ -- Refined_Post --
+ ------------------
- -- pragma Refined_Pre (boolean_EXPRESSION);
+ -- pragma Refined_Post (boolean_EXPRESSION);
- when Pragma_Refined_Pre => Refined_Pre : declare
- Body_Decl : Node_Id := Parent (N);
- Pack_Spec : Node_Id;
- Restore : Boolean := False;
- Spec_Decl : Node_Id;
+ when Pragma_Refined_Post => Refined_Post : declare
+ Body_Decl : Node_Id;
+ Legal : Boolean;
Spec_Id : Entity_Id;
- Stmt : Node_Id;
begin
- GNAT_Pragma;
- Check_Arg_Count (1);
- Check_No_Identifiers;
-
- -- Verify the placement of the pragma and check for duplicates
-
- Stmt := Prev (N);
- while Present (Stmt) loop
-
- -- Skip prior pragmas, but check for duplicates
-
- if Nkind (Stmt) = N_Pragma then
- if Pragma_Name (Stmt) = Pname then
- Error_Msg_Name_1 := Pname;
- Error_Msg_Sloc := Sloc (Stmt);
- Error_Msg_N ("pragma % duplicates pragma declared #", N);
- end if;
-
- -- The pragma applies to a subprogram body stub
-
- elsif Nkind (Stmt) = N_Subprogram_Body_Stub then
- Body_Decl := Stmt;
- exit;
-
- -- The pragma applies to an expression function that does not
- -- act as a completion of a previous function declaration.
-
- elsif Nkind (Stmt) = N_Subprogram_Declaration
- and then Nkind (Original_Node (Stmt)) = N_Expression_Function
- and then not
- Has_Completion (Defining_Unit_Name (Specification (Stmt)))
- then
- Error_Pragma ("pragma % cannot apply to a stand alone body");
- return;
-
- -- Skip internally generated code
-
- elsif not Comes_From_Source (Stmt) then
- null;
-
- -- The pragma does not apply to a legal construct, issue an
- -- error and stop the analysis.
-
- else
- Pragma_Misplaced;
- return;
- end if;
+ -- Verify the legal placement of the pragma. The pragma is left
+ -- intentionally semi-analyzed. Process_PPCs does the remaining
+ -- analysis of the expression when Refined_Post is converted into
+ -- pragma Check.
- Stmt := Prev (Stmt);
- end loop;
-
- -- Pragma Refined_Pre must apply to a subprogram body [stub]
-
- if not Nkind_In (Body_Decl, N_Subprogram_Body,
- N_Subprogram_Body_Stub)
- then
- Pragma_Misplaced;
- return;
- end if;
-
- -- The body [stub] must not act as a spec
+ Analyze_Refined_Pre_Post (Body_Decl, Spec_Id, Legal);
- if Nkind (Body_Decl) = N_Subprogram_Body then
- Spec_Id := Corresponding_Spec (Body_Decl);
- else
- Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl);
- end if;
+ -- Analyze the expression when code generation is disabled because
+ -- the contract of the related subprogram will never be processed.
- if No (Spec_Id) then
- Error_Pragma ("pragma % cannot apply to a stand alone body");
- return;
+ if Legal and then not Expander_Active then
+ Analyze_And_Resolve (Get_Pragma_Arg (Arg1), Standard_Boolean);
end if;
+ end Refined_Post;
- -- Refined_Pre may only apply to the body [stub] of a subprogram
- -- declared in the visible part of a package. Retrieve the context
- -- of the subprogram declaration.
-
- Spec_Decl := Parent (Parent (Spec_Id));
+ -----------------
+ -- Refined_Pre --
+ -----------------
- pragma Assert
- (Nkind_In (Spec_Decl, N_Abstract_Subprogram_Declaration,
- N_Generic_Subprogram_Declaration,
- N_Subprogram_Declaration));
+ -- pragma Refined_Pre (boolean_EXPRESSION);
- Pack_Spec := Parent (Spec_Decl);
+ when Pragma_Refined_Pre => Refined_Pre : declare
+ Body_Decl : Node_Id;
+ Legal : Boolean;
+ Restore : Boolean := False;
+ Spec_Id : Entity_Id;
- if Nkind (Pack_Spec) /= N_Package_Specification
- or else List_Containing (Spec_Decl) /=
- Visible_Declarations (Pack_Spec)
- then
- Error_Pragma
- ("pragma % must apply to the body of a visible subprogram");
- end if;
+ begin
+ Analyze_Refined_Pre_Post (Body_Decl, Spec_Id, Legal);
- -- When the pragma applies to a subprogram stub without a proper
- -- body, we have to restore the visibility of the stub and its
- -- formals to perform analysis.
+ if Legal then
+ pragma Assert (Present (Body_Decl));
+ pragma Assert (Present (Spec_Id));
- if Nkind (Body_Decl) = N_Subprogram_Body_Stub
- and then No (Library_Unit (Body_Decl))
- and then Current_Scope /= Spec_Id
- then
- Restore := True;
- Push_Scope (Spec_Id);
- Install_Formals (Spec_Id);
- end if;
+ if Nkind (Body_Decl) = N_Subprogram_Body_Stub
+ and then No (Library_Unit (Body_Decl))
+ and then Current_Scope /= Spec_Id
+ then
+ Restore := True;
+ Push_Scope (Spec_Id);
+ Install_Formals (Spec_Id);
+ end if;
- -- Convert pragma Refined_Pre into pragma Check. The analysis of
- -- the generated pragma will take care of the expression.
+ -- Convert pragma Refined_Pre into pragma Check. The analysis
+ -- of the generated pragma will take care of the expression.
- Rewrite (N,
- Make_Pragma (Loc,
- Chars => Name_Check,
- Pragma_Argument_Associations => New_List (
- Make_Pragma_Argument_Association (Loc,
- Expression => Make_Identifier (Loc, Pname)),
+ Rewrite (N,
+ Make_Pragma (Loc,
+ Chars => Name_Check,
+ Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Make_Identifier (Loc, Pname)),
- Make_Pragma_Argument_Association (Sloc (Arg1),
- Expression => Relocate_Node (Get_Pragma_Arg (Arg1))))));
+ Make_Pragma_Argument_Association (Sloc (Arg1),
+ Expression => Relocate_Node (Get_Pragma_Arg (Arg1))))));
- Analyze (N);
+ Analyze (N);
- if Restore then
- Pop_Scope;
+ if Restore then
+ Pop_Scope;
+ end if;
end if;
end Refined_Pre;
Pragma_Queuing_Policy => -1,
Pragma_Rational => -1,
Pragma_Ravenscar => -1,
+ Pragma_Refined_Post => -1,
Pragma_Refined_Pre => -1,
Pragma_Relative_Deadline => -1,
Pragma_Remote_Access_Type => -1,
end Process_Compilation_Unit_Pragmas;
+ ------------------------------
+ -- Relocate_Pragmas_To_Body --
+ ------------------------------
+
+ procedure Relocate_Pragmas_To_Body
+ (Subp_Body : Node_Id;
+ Target_Body : Node_Id := Empty)
+ is
+ procedure Relocate_Pragma (Prag : Node_Id);
+ -- Remove a single pragma from its current list and add it to the
+ -- declarations of the proper body (either Subp_Body or Target_Body).
+
+ ---------------------
+ -- Relocate_Pragma --
+ ---------------------
+
+ procedure Relocate_Pragma (Prag : Node_Id) is
+ Decls : List_Id;
+ Target : Node_Id;
+
+ begin
+ -- When subprogram stubs or expression functions are involves, the
+ -- destination declaration list belongs to the proper body.
+
+ if Present (Target_Body) then
+ Target := Target_Body;
+ else
+ Target := Subp_Body;
+ end if;
+
+ Decls := Declarations (Target);
+
+ if No (Decls) then
+ Decls := New_List;
+ Set_Declarations (Target, Decls);
+ end if;
+
+ -- Unhook the pragma from its current list
+
+ Remove (Prag);
+ Prepend (Prag, Decls);
+ end Relocate_Pragma;
+
+ -- Local variables
+
+ Body_Id : constant Entity_Id :=
+ Defining_Unit_Name (Specification (Subp_Body));
+ Next_Stmt : Node_Id;
+ Stmt : Node_Id;
+
+ -- Start of processing for Relocate_Pragmas_To_Body
+
+ begin
+ -- Do not process a body that comes from a separate unit as no construct
+ -- can possibly follow it.
+
+ if not Is_List_Member (Subp_Body) then
+ return;
+
+ -- Do not relocate pragmas that follow a stub if the stub does not have
+ -- a proper body.
+
+ elsif Nkind (Subp_Body) = N_Subprogram_Body_Stub
+ and then No (Target_Body)
+ then
+ return;
+
+ -- Do not process internally generated routine _Postconditions
+
+ elsif Ekind (Body_Id) = E_Procedure
+ and then Chars (Body_Id) = Name_uPostconditions
+ then
+ return;
+ end if;
+
+ -- Look at what is following the body. We are interested in certain kind
+ -- of pragmas (either from source or byproducts of expansion) that can
+ -- apply to a body [stub].
+
+ Stmt := Next (Subp_Body);
+ while Present (Stmt) loop
+
+ -- Preserve the following statement for iteration purposes due to a
+ -- possible relocation of a pragma.
+
+ Next_Stmt := Next (Stmt);
+
+ -- Move a candidate pragma following the body to the declarations of
+ -- the body.
+
+ if Nkind (Stmt) = N_Pragma
+ and then Pragma_On_Body_Or_Stub_OK (Get_Pragma_Id (Stmt))
+ then
+ Relocate_Pragma (Stmt);
+
+ -- Skip internally generated code
+
+ elsif not Comes_From_Source (Stmt) then
+ null;
+
+ -- No candidate pragmas are available for relocation
+
+ else
+ exit;
+ end if;
+
+ Stmt := Next_Stmt;
+ end loop;
+ end Relocate_Pragmas_To_Body;
+
----------------------------
-- Rewrite_Assertion_Kind --
----------------------------
package Sem_Prag is
-- The following table lists all the implementation-defined pragmas that
- -- may apply to a body stub (no language defined pragmas apply).
+ -- may apply to a body stub (no language defined pragmas apply). The table
+ -- should be synchronized with Aspect_On_Body_Or_Stub_OK in unit Aspects if
+ -- the pragmas below implement an aspect.
- Pragma_On_Stub_OK : constant array (Pragma_Id) of Boolean :=
- (Pragma_Refined_Pre => True,
+ Pragma_On_Body_Or_Stub_OK : constant array (Pragma_Id) of Boolean :=
+ (Pragma_Refined_Post => True,
+ Pragma_Refined_Pre => True,
Pragma_SPARK_Mode => True,
+ Pragma_Warnings => True,
others => False);
-----------------
-- Suppress_All at this stage, since it can appear after the unit instead
-- of before (actually we allow it to appear anywhere).
+ procedure Relocate_Pragmas_To_Body
+ (Subp_Body : Node_Id;
+ Target_Body : Node_Id := Empty);
+ -- Resocate all pragmas that follow and apply to subprogram body Subp_Body
+ -- to its own declaration list. Candidate pragmas are classified in table
+ -- Pragma_On_Body_Or_Stub_OK. If Target_Body is set, the pragma are moved
+ -- to the declarations of Target_Body. This formal should be set when
+ -- dealing with subprogram body stubs or expression functions.
+
procedure Set_Encoded_Interface_Name (E : Entity_Id; S : Node_Id);
-- This routine is used to set an encoded interface name. The node S is an
-- N_String_Literal node for the external name to be set, and E is an
Name_Pure_05 : constant Name_Id := N + $; -- GNAT
Name_Pure_12 : constant Name_Id := N + $; -- GNAT
Name_Pure_Function : constant Name_Id := N + $; -- GNAT
+ Name_Refined_Post : constant Name_Id := N + $; -- GNAT
Name_Refined_Pre : constant Name_Id := N + $; -- GNAT
Name_Relative_Deadline : constant Name_Id := N + $; -- Ada 05
Name_Remote_Access_Type : constant Name_Id := N + $; -- GNAT
Pragma_Pure_05,
Pragma_Pure_12,
Pragma_Pure_Function,
+ Pragma_Refined_Post,
Pragma_Refined_Pre,
Pragma_Relative_Deadline,
Pragma_Remote_Access_Type,
projects / thirdparty / gcc.git / commitdiff
