+2015-03-02 Thomas Quinot <quinot@adacore.com>
+
+ * exp_attr.adb (Expand_N_Attribute_Reference, case Input): When
+ expanding a 'Input attribute reference for a class-wide type,
+ do not generate a separate object declaration for the controlling
+ tag dummy object; instead, generate the expression inline in the
+ dispatching call. Otherwise, the declaration (which involves a
+ call to String'Input, returning a dynamically sized value on the
+ secondary stack) will be expanded outside of proper secondary
+ stack mark/release operations, and will thus cause a secondary
+ stack leak.
+
+2015-03-02 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * checks.adb (Add_Validity_Check): Change the names of all
+ formal parameters to better illustrate their purpose. Update
+ the subprogram documentation. Update all occurrences of the
+ formal parameters. Generate a pre/postcondition pragma by
+ calling Build_Pre_Post_Condition.
+ (Build_PPC_Pragma): Removed.
+ (Build_Pre_Post_Condition): New routine.
+ * einfo.adb Node8 is no longer used as Postcondition_Proc. Node14
+ is now used as Postconditions_Proc. Flag240 is now renamed to
+ Has_Expanded_Contract. (First_Formal): The routine can now
+ operate on generic subprograms.
+ (First_Formal_With_Extras): The routine can now operate on generic
+ subprograms.
+ (Has_Expanded_Contract): New routine.
+ (Has_Postconditions): Removed.
+ (Postcondition_Proc): Removed.
+ (Postconditions_Proc): New routine.
+ (Set_Has_Expanded_Contract): New routine.
+ (Set_Has_Postconditions): Removed.
+ (Set_Postcondition_Proc): Removed.
+ (Set_Postconditions_Proc): New routine.
+ (Write_Entity_Flags): Remove the output of Has_Postconditions. Add
+ the output of Has_Expanded_Contract.
+ (Write_Field8_Name): Remove the output of Postcondition_Proc.
+ (Write_Field14_Name): Add the output of Postconditions_Proc.
+ * einfo.ads New attributes Has_Expanded_Contract and
+ Postconditions_Proc along with occurrences in entities.
+ Remove attributes Has_Postconditions and Postcondition_Proc
+ along with occurrences in entities.
+ (Has_Expanded_Contract): New routine along with pragma Inline.
+ (Has_Postconditions): Removed along with pragma Inline.
+ (Postcondition_Proc): Removed along with pragma Inline.
+ (Postconditions_Proc): New routine along with pragma Inline.
+ (Set_Has_Expanded_Contract): New routine along with pragma Inline.
+ (Set_Has_Postconditions): Removed along with pragma Inline.
+ (Set_Postcondition_Proc): Removed along with pragma Inline.
+ (Set_Postconditions_Proc): New routine along with pragma Inline.
+ * exp_ch6.adb (Add_Return): Code cleanup. Update the
+ generation of the call to the _Postconditions routine of
+ the procedure. (Expand_Non_Function_Return): Reformat the
+ comment on usage. Code cleanup. Update the generation of
+ the call to the _Postconditions routine of the procedure or
+ entry [family].
+ (Expand_Simple_Function_Return): Update the
+ generation of the _Postconditions routine of the function.
+ (Expand_Subprogram_Contract): Reimplemented.
+ * exp_ch6.ads (Expand_Subprogram_Contract): Update the parameter
+ profile along the comment on usage.
+ * exp_ch9.adb (Build_PPC_Wrapper): Code cleanup.
+ (Expand_N_Task_Type_Declaration): Generate pre/postconditions
+ wrapper when the entry [family] has a contract with
+ pre/postconditions.
+ * exp_prag.adb (Expand_Attributes_In_Consequence): New routine.
+ (Expand_Contract_Cases): This routine and its subsidiaries now
+ analyze all generated code.
+ (Expand_Old_In_Consequence): Removed.
+ * sem_attr.adb Add with and use clause for Sem_Prag.
+ (Analyze_Attribute): Reimplment the analysis of attribute 'Result.
+ (Check_Use_In_Test_Case): Use routine Test_Case_Arg to obtain
+ "Ensures".
+ * sem_ch3.adb (Analyze_Declarations): Analyze the contract of
+ a generic subprogram.
+ (Analyze_Object_Declaration): Do not create a contract node.
+ (Derive_Subprogram): Do not create a contract node.
+ * sem_ch6.adb (Analyze_Abstract_Subprogram_Declaration): Do
+ not create a contract node.
+ (Analyze_Completion_Contract): New routine.
+ (Analyze_Function_Return): Alphabetize.
+ (Analyze_Generic_Subprogram_Body): Alphabetize. Do not create a
+ contract node. Do not copy pre/postconditions to the original
+ generic template.
+ (Analyze_Null_Procedure): Do not create a contract node.
+ (Analyze_Subprogram_Body_Contract): Reimplemented.
+ (Analyze_Subprogram_Body_Helper): Do not mark the enclosing scope
+ as having postconditions. Do not create a contract node. Analyze
+ the subprogram body contract of a body that acts as a compilation
+ unit. Expand the subprogram contract after the declarations have
+ been analyzed.
+ (Analyze_Subprogram_Contract): Reimplemented.
+ (Analyze_Subprogram_Specification): Do not create a contract node.
+ (List_Inherited_Pre_Post_Aspects): Code cleanup.
+ * sem_ch6.adb (Analyze_Subprogram_Body_Contract): Update the
+ comment on usage.
+ (Analyze_Subprogram_Contract): Update the
+ parameter profile and the comment on usage.
+ * sem_ch7.adb (Analyze_Package_Body_Helper): Do not create a
+ contract node.
+ (Analyze_Package_Declaration): Do not create a
+ contract node.
+ (Is_Subp_Or_Const_Ref): Ensure that the prefix has an entity.
+ * sem_ch8.adb (Analyze_Subprogram_Renaming): Do not create a
+ contract node.
+ * sem_ch9.adb (Analyze_Entry_Declaration): Do not create a
+ contract node.
+ * sem_ch10.adb (Analyze_Compilation_Unit): Move local variables to
+ their proper section and alphabetize them. Analyze the contract of
+ a [generic] subprogram after all Pragmas_After have been analyzed.
+ (Analyze_Subprogram_Body_Stub_Contract): Alphabetize.
+ * sem_ch12.adb (Analyze_Generic_Package_Declaration): Do not
+ create a contract node.
+ (Analyze_Generic_Subprogram_Declaration):
+ Alphabetize local variables. Do not create a contract
+ node. Do not generate aspects out of pragmas for ASIS.
+ (Analyze_Subprogram_Instantiation): Instantiate
+ the contract of the subprogram. Do not create a
+ contract node. (Instantiate_Contract): New routine.
+ (Instantiate_Subprogram_Body): Alphabetize local variables.
+ (Save_Global_References_In_Aspects): New routine.
+ (Save_References): Do not save the global references found within
+ the aspects of a generic subprogram.
+ * sem_ch12.ads (Save_Global_References_In_Aspects): New routine.
+ * sem_ch13.adb (Analyze_Aspect_Specifications): Do not use
+ Original_Node for establishing linkages.
+ (Insert_Pragma): Insertion in a subprogram body takes precedence over
+ the case where the subprogram body is also a compilation unit.
+ * sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part): Use
+ Get_Argument to obtain the proper expression. Install the generic
+ formals when the related context is a generic subprogram.
+ (Analyze_Depends_In_Decl_Part): Use Get_Argument to obtain
+ the proper expression. Use Corresponding_Spec_Of to obtain
+ the spec. Install the generic formal when the related context
+ is a generic subprogram.
+ (Analyze_Global_In_Decl_Part): Use Get_Argument to obtain the proper
+ expression. Use Corresponding_Spec_Of to obtain the spec. Install the
+ generic formal when the related context is a generic subprogram.
+ (Analyze_Initial_Condition_In_Decl_Part): Use Get_Argument
+ to obtain the proper expression. Remove the call to
+ Check_SPARK_Aspect_For_ASIS as the analysis is now done
+ automatically.
+ (Analyze_Pragma): Update all occurrences
+ to Original_Aspect_Name. Pragmas Contract_Cases, Depends,
+ Extensions_Visible, Global, Postcondition, Precondition and
+ Test_Case now carry generic templates when the related context
+ is a generic subprogram. The same pragmas are no longer
+ forcefully fully analyzed when the context is a subprogram
+ that acts as a compilation unit. Pragmas Abstract_State,
+ Initial_Condition, Initializes and Refined_State have been clean
+ up. Pragmas Post, Post_Class, Postcondition, Pre, Pre_Class
+ and Precondition now use the same routine for analysis. Pragma
+ Refined_Post does not need to check the use of 'Result or
+ the lack of a post-state in its expression. Reimplement the
+ analysis of pragma Test_Case.
+ (Analyze_Pre_Post_Condition): New routine.
+ (Analyze_Pre_Post_Condition_In_Decl_Part):
+ Reimplemented.
+ (Analyze_Refined_Depends_In_Decl_Part): Use Get_Argument to obtain the
+ proper expression.
+ (Analyze_Refined_Global_In_Decl_Part): Use Get_Argument to obtain
+ the proper expression.
+ (Analyze_Test_Case_In_Decl_Part): Reimplemented.
+ (Check_Pre_Post): Removed.
+ (Check_Precondition_Postcondition): Removed.
+ (Check_SPARK_Aspect_For_ASIS): Removed.
+ (Check_Test_Case): Removed.
+ (Collect_Subprogram_Inputs_Outputs): Use Get_Argument
+ to obtain the proper expression. Use Corresponding_Spec_Of to
+ find the proper spec.
+ (Create_Generic_Template): New routine.
+ (Duplication_Error): New routine.
+ (Expression_Function_Error): New routine.
+ (Find_Related_Subprogram_Or_Body): Moved to the spec
+ of Sem_Prag. Emit precise error messages. Account for cases of
+ rewritten expression functions, generic instantiations, handled
+ sequence of statements and pragmas from aspects.
+ (Get_Argument): New routine.
+ (Make_Aspect_For_PPC_In_Gen_Sub_Decl): Removed.
+ (Preanalyze_CTC_Args): Removed.
+ (Process_Class_Wide_Condition): New routine.
+ * sem_prag.ads (Analyze_Test_Case_In_Decl_Part): Update
+ the parameter profile along with the comment on usage.
+ (Find_Related_Subprogram_Or_Body): Moved from the body of Sem_Prag.
+ (Make_Aspect_For_PPC_In_Gen_Sub_Decl): Removed.
+ (Test_Case_Arg): New routine.
+ * sem_util.adb Add with and use clauses for Sem_Ch6.
+ (Add_Contract_Item): This routine now creates a contract
+ node the first time an item is added. Remove the duplicate
+ aspect/pragma checks.
+ (Check_Result_And_Post_State): Reimplemented.
+ (Corresponding_Spec_Of): New routine.
+ (Get_Ensures_From_CTC_Pragma): Removed.
+ (Get_Requires_From_CTC_Pragma): Removed.
+ (Has_Significant_Contract): New routine.
+ (Inherit_Subprogram_Contract): Inherit only if the source
+ has a contract.
+ (Install_Generic_Formals): New routine.
+ (Original_Aspect_Name): Removed.
+ (Original_Aspect_Pragma_Name): New routine.
+ * sem_util.ads (Check_Result_And_Post_State): Reimplemented.
+ (Corresponding_Spec_Of): New routine.
+ (Get_Ensures_From_CTC_Pragma): Removed.
+ (Get_Requires_From_CTC_Pragma): Removed.
+ (Has_Significant_Contract): New routine.
+ (Install_Generic_Formals): New routine.
+ (Original_Aspect_Name): Removed.
+ (Original_Aspect_Pragma_Name): New routine.
+ * sem_warn.adb Add with and use clauses for Sem_Prag.
+ (Within_Postcondition): Use Test_Case_Arg to extract "Ensures".
+
2015-03-02 Ed Schonberg <schonberg@adacore.com>
* sem_ch8.adb (Available_Subtype): Optimization in
Subp_Decl : Node_Id;
procedure Add_Validity_Check
- (Context : Entity_Id;
- PPC_Nam : Name_Id;
+ (Formal : Entity_Id;
+ Prag_Nam : Name_Id;
For_Result : Boolean := False);
-- Add a single 'Valid[_Scalar] check which verifies the initialization
- -- of Context. PPC_Nam denotes the pre or post condition pragma name.
+ -- of Formal. Prag_Nam denotes the pre or post condition pragma name.
-- Set flag For_Result when to verify the result of a function.
- procedure Build_PPC_Pragma (PPC_Nam : Name_Id; Check : Node_Id);
- -- Create a pre or post condition pragma with name PPC_Nam which
- -- tests expression Check.
-
------------------------
-- Add_Validity_Check --
------------------------
procedure Add_Validity_Check
- (Context : Entity_Id;
- PPC_Nam : Name_Id;
+ (Formal : Entity_Id;
+ Prag_Nam : Name_Id;
For_Result : Boolean := False)
is
+ procedure Build_Pre_Post_Condition (Expr : Node_Id);
+ -- Create a pre/postcondition pragma that tests expression Expr
+
+ ------------------------------
+ -- Build_Pre_Post_Condition --
+ ------------------------------
+
+ procedure Build_Pre_Post_Condition (Expr : Node_Id) is
+ Loc : constant Source_Ptr := Sloc (Subp);
+ Decls : List_Id;
+ Prag : Node_Id;
+
+ begin
+ Prag :=
+ Make_Pragma (Loc,
+ Pragma_Identifier =>
+ Make_Identifier (Loc, Prag_Nam),
+ Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Chars => Name_Check,
+ Expression => Expr)));
+
+ -- Add a message unless exception messages are suppressed
+
+ if not Exception_Locations_Suppressed then
+ Append_To (Pragma_Argument_Associations (Prag),
+ Make_Pragma_Argument_Association (Loc,
+ Chars => Name_Message,
+ Expression =>
+ Make_String_Literal (Loc,
+ Strval => "failed "
+ & Get_Name_String (Prag_Nam)
+ & " from "
+ & Build_Location_String (Loc))));
+ end if;
+
+ -- Insert the pragma in the tree
+
+ if Nkind (Parent (Subp_Decl)) = N_Compilation_Unit then
+ Add_Global_Declaration (Prag);
+ Analyze (Prag);
+
+ -- PPC pragmas associated with subprogram bodies must be inserted
+ -- in the declarative part of the body.
+
+ elsif Nkind (Subp_Decl) = N_Subprogram_Body then
+ Decls := Declarations (Subp_Decl);
+
+ if No (Decls) then
+ Decls := New_List;
+ Set_Declarations (Subp_Decl, Decls);
+ end if;
+
+ Prepend_To (Decls, Prag);
+ Analyze (Prag);
+
+ -- For subprogram declarations insert the PPC pragma right after
+ -- the declarative node.
+
+ else
+ Insert_After_And_Analyze (Subp_Decl, Prag);
+ end if;
+ end Build_Pre_Post_Condition;
+
+ -- Local variables
+
Loc : constant Source_Ptr := Sloc (Subp);
- Typ : constant Entity_Id := Etype (Context);
+ Typ : constant Entity_Id := Etype (Formal);
Check : Node_Id;
Nam : Name_Id;
+ -- Start of processing for Add_Validity_Check
+
begin
-- For scalars, generate 'Valid test
-- Step 1: Create the expression to verify the validity of the
-- context.
- Check := New_Occurrence_Of (Context, Loc);
+ Check := New_Occurrence_Of (Formal, Loc);
-- When processing a function result, use 'Result. Generate
-- Context'Result
-- Step 2: Create a pre or post condition pragma
- Build_PPC_Pragma (PPC_Nam, Check);
+ Build_Pre_Post_Condition (Check);
end Add_Validity_Check;
- ----------------------
- -- Build_PPC_Pragma --
- ----------------------
-
- procedure Build_PPC_Pragma (PPC_Nam : Name_Id; Check : Node_Id) is
- Loc : constant Source_Ptr := Sloc (Subp);
- Decls : List_Id;
- Prag : Node_Id;
-
- begin
- Prag :=
- Make_Pragma (Loc,
- Pragma_Identifier => Make_Identifier (Loc, PPC_Nam),
- Pragma_Argument_Associations => New_List (
- Make_Pragma_Argument_Association (Loc,
- Chars => Name_Check,
- Expression => Check)));
-
- -- Add a message unless exception messages are suppressed
-
- if not Exception_Locations_Suppressed then
- Append_To (Pragma_Argument_Associations (Prag),
- Make_Pragma_Argument_Association (Loc,
- Chars => Name_Message,
- Expression =>
- Make_String_Literal (Loc,
- Strval => "failed " & Get_Name_String (PPC_Nam) &
- " from " & Build_Location_String (Loc))));
- end if;
-
- -- Insert the pragma in the tree
-
- if Nkind (Parent (Subp_Decl)) = N_Compilation_Unit then
- Add_Global_Declaration (Prag);
- Analyze (Prag);
-
- -- PPC pragmas associated with subprogram bodies must be inserted in
- -- the declarative part of the body.
-
- elsif Nkind (Subp_Decl) = N_Subprogram_Body then
- Decls := Declarations (Subp_Decl);
-
- if No (Decls) then
- Decls := New_List;
- Set_Declarations (Subp_Decl, Decls);
- end if;
-
- Prepend_To (Decls, Prag);
-
- -- Ensure the proper visibility of the subprogram body and its
- -- parameters.
-
- Push_Scope (Subp);
- Analyze (Prag);
- Pop_Scope;
-
- -- For subprogram declarations insert the PPC pragma right after the
- -- declarative node.
-
- else
- Insert_After_And_Analyze (Subp_Decl, Prag);
- end if;
- end Build_PPC_Pragma;
-
-- Local variables
Formal : Entity_Id;
-- Hiding_Loop_Variable Node8
-- Mechanism Uint8 (but returns Mechanism_Type)
-- Normalized_First_Bit Uint8
- -- Postcondition_Proc Node8
-- Refinement_Constituents Elist8
-- Return_Applies_To Node8
-- First_Exit_Statement Node8
-- Alignment Uint14
-- Normalized_Position Uint14
+ -- Postconditions_Proc Node14
-- Shadow_Entities List14
-- Discriminant_Number Uint15
-- Warnings_Off_Used_Unmodified Flag237
-- Warnings_Off_Used_Unreferenced Flag238
-- OK_To_Reorder_Components Flag239
- -- Has_Postconditions Flag240
+ -- Has_Expanded_Contract Flag240
-- Optimize_Alignment_Space Flag241
-- Optimize_Alignment_Time Flag242
return Flag47 (Id);
end Has_Exit;
+ function Has_Expanded_Contract (Id : E) return B is
+ begin
+ pragma Assert (Is_Subprogram (Id));
+ return Flag240 (Id);
+ end Has_Expanded_Contract;
+
function Has_Forward_Instantiation (Id : E) return B is
begin
return Flag175 (Id);
return Flag154 (Id);
end Has_Per_Object_Constraint;
- function Has_Postconditions (Id : E) return B is
- begin
- pragma Assert (Is_Subprogram (Id));
- return Flag240 (Id);
- end Has_Postconditions;
-
function Has_Pragma_Controlled (Id : E) return B is
begin
pragma Assert (Is_Access_Type (Id));
return Elist15 (Id);
end Pending_Access_Types;
- function Postcondition_Proc (Id : E) return E is
+ function Postconditions_Proc (Id : E) return E is
begin
- pragma Assert (Ekind (Id) = E_Procedure);
- return Node8 (Id);
- end Postcondition_Proc;
+ pragma Assert (Ekind_In (Id, E_Entry,
+ E_Entry_Family,
+ E_Function,
+ E_Procedure));
+ return Node14 (Id);
+ end Postconditions_Proc;
function PPC_Wrapper (Id : E) return E is
begin
Set_Flag47 (Id, V);
end Set_Has_Exit;
+ procedure Set_Has_Expanded_Contract (Id : E; V : B := True) is
+ begin
+ pragma Assert (Ekind_In (Id, E_Entry,
+ E_Entry_Family,
+ E_Function,
+ E_Procedure));
+ Set_Flag240 (Id, V);
+ end Set_Has_Expanded_Contract;
+
procedure Set_Has_Forward_Instantiation (Id : E; V : B := True) is
begin
Set_Flag175 (Id, V);
Set_Flag154 (Id, V);
end Set_Has_Per_Object_Constraint;
- procedure Set_Has_Postconditions (Id : E; V : B := True) is
- begin
- pragma Assert (Is_Subprogram (Id));
- Set_Flag240 (Id, V);
- end Set_Has_Postconditions;
-
procedure Set_Has_Pragma_Controlled (Id : E; V : B := True) is
begin
pragma Assert (Is_Access_Type (Id));
Set_Elist15 (Id, V);
end Set_Pending_Access_Types;
- procedure Set_Postcondition_Proc (Id : E; V : E) is
+ procedure Set_Postconditions_Proc (Id : E; V : E) is
begin
- pragma Assert (Ekind (Id) = E_Procedure);
- Set_Node8 (Id, V);
- end Set_Postcondition_Proc;
+ pragma Assert (Ekind_In (Id, E_Entry,
+ E_Entry_Family,
+ E_Function,
+ E_Procedure));
+ Set_Node14 (Id, V);
+ end Set_Postconditions_Proc;
procedure Set_PPC_Wrapper (Id : E; V : E) is
begin
begin
pragma Assert
- (Is_Overloadable (Id)
+ (Is_Generic_Subprogram (Id)
+ or else Is_Overloadable (Id)
or else Ekind_In (Id, E_Entry_Family,
E_Subprogram_Body,
E_Subprogram_Type));
else
Formal := First_Entity (Id);
+ -- The first/next entity chain of a generic subprogram contains all
+ -- generic formal parameters, followed by the formal parameters. Go
+ -- directly to the paramters by skipping the formal part.
+
+ if Is_Generic_Subprogram (Id) then
+ while Present (Formal) and then not Is_Formal (Formal) loop
+ Next_Entity (Formal);
+ end loop;
+ end if;
+
if Present (Formal) and then Is_Formal (Formal) then
return Formal;
else
begin
pragma Assert
- (Is_Overloadable (Id)
+ (Is_Generic_Subprogram (Id)
+ or else Is_Overloadable (Id)
or else Ekind_In (Id, E_Entry_Family,
E_Subprogram_Body,
E_Subprogram_Type));
else
Formal := First_Entity (Id);
+ -- The first/next entity chain of a generic subprogram contains all
+ -- generic formal parameters, followed by the formal parameters. Go
+ -- directly to the paramters by skipping the formal part.
+
+ if Is_Generic_Subprogram (Id) then
+ while Present (Formal) and then not Is_Formal (Formal) loop
+ Next_Entity (Formal);
+ end loop;
+ end if;
+
if Present (Formal) and then Is_Formal (Formal) then
return Formal;
else
W ("Has_Dynamic_Predicate_Aspect", Flag258 (Id));
W ("Has_Enumeration_Rep_Clause", Flag66 (Id));
W ("Has_Exit", Flag47 (Id));
+ W ("Has_Expanded_Contract", Flag240 (Id));
W ("Has_Forward_Instantiation", Flag175 (Id));
W ("Has_Fully_Qualified_Name", Flag173 (Id));
W ("Has_Gigi_Rep_Item", Flag82 (Id));
W ("Has_Out_Or_In_Out_Parameter", Flag110 (Id));
W ("Has_Object_Size_Clause", Flag172 (Id));
W ("Has_Per_Object_Constraint", Flag154 (Id));
- W ("Has_Postconditions", Flag240 (Id));
W ("Has_Pragma_Controlled", Flag27 (Id));
W ("Has_Pragma_Elaborate_Body", Flag150 (Id));
W ("Has_Pragma_Inline", Flag157 (Id));
E_Discriminant =>
Write_Str ("Normalized_First_Bit");
- when E_Procedure =>
- Write_Str ("Postcondition_Proc");
-
when E_Abstract_State =>
Write_Str ("Refinement_Constituents");
Formal_Kind |
E_Constant |
E_Exception |
- E_Variable |
- E_Loop_Parameter =>
+ E_Loop_Parameter |
+ E_Variable =>
Write_Str ("Alignment");
when E_Component |
E_Discriminant =>
Write_Str ("Normalized_Position");
- when E_Package |
- E_Generic_Package =>
+ when E_Entry |
+ E_Entry_Family |
+ E_Function |
+ E_Procedure =>
+ Write_Str ("Postconditions_Proc");
+
+ when E_Generic_Package |
+ E_Package =>
Write_Str ("Shadow_Entities");
when others =>
-- Has_Exit (Flag47)
-- Defined in loop entities. Set if the loop contains an exit statement.
+-- Has_Expanded_Contract (Flag240)
+-- Defined in functions, procedures, entries, and entry families. Set
+-- when a subprogram has a N_Contract node that has been expanded. The
+-- flag prevents double expansion of a contract when a construct is
+-- rewritten into something else and subsequently reanalyzed/expanded.
+
-- Has_Foreign_Convention (synthesized)
-- Applies to all entities. Determines if the Convention for the
-- entity is a foreign convention (i.e. is other than Convention_Ada,
-- 5. N_Range_Constraint - when the range expression uses the
-- discriminant of the enclosing type.
--- Has_Postconditions (Flag240)
--- Defined in subprogram entities. Set if postconditions are active for
--- the procedure, and a _postconditions procedure has been generated.
-
-- Has_Pragma_Controlled (Flag27) [implementation base type only]
-- Defined in access type entities. It is set if a pragma Controlled
-- applies to the access type.
-- ensure that the finalization masters of all pending access types are
-- fully initialized when the full view is frozen.
--- Postcondition_Proc (Node8)
--- Defined only in procedure entities, saves the entity of the generated
--- postcondition proc if one is present, otherwise is set to Empty. Used
--- to generate the call to this procedure in case the expander inserts
--- implicit return statements.
+-- Postconditions_Proc (Node14)
+-- Defined in functions, procedures, entries, and entry families. Refers
+-- to the entity of the _Postconditions procedure used to check contract
+-- assertions on exit from a subprogram.
-- PPC_Wrapper (Node25)
-- Defined in entries and entry families. Set only if pre- or post-
-- E_Entry_Family
-- Protected_Body_Subprogram (Node11)
-- Barrier_Function (Node12)
+ -- Postconditions_Proc (Node14)
-- Entry_Parameters_Type (Node15)
-- First_Entity (Node17)
-- Alias (Node18) (for entry only. Empty)
-- PPC_Wrapper (Node25)
-- Extra_Formals (Node28)
-- Contract (Node34)
+ -- Needs_No_Actuals (Flag22)
+ -- Uses_Sec_Stack (Flag95)
-- Default_Expressions_Processed (Flag108)
-- Entry_Accepted (Flag152)
- -- Needs_No_Actuals (Flag22)
-- Sec_Stack_Needed_For_Return (Flag167)
- -- Uses_Sec_Stack (Flag95)
+ -- Has_Expanded_Contract (Flag240)
-- Address_Clause (synth)
-- Entry_Index_Type (synth)
-- First_Formal (synth)
-- Protected_Body_Subprogram (Node11)
-- Next_Inlined_Subprogram (Node12)
-- Elaboration_Entity (Node13) (not implicit /=)
+ -- Postconditions_Proc (Node14) (non-generic case only)
-- DT_Position (Uint15)
-- DTC_Entity (Node16)
-- First_Entity (Node17)
-- Has_Anonymous_Master (Flag253)
-- Has_Completion (Flag26)
-- Has_Controlling_Result (Flag98)
+ -- Has_Expanded_Contract (Flag240) (non-generic case only)
-- Has_Invariants (Flag232)
-- Has_Master_Entity (Flag21)
-- Has_Missing_Return (Flag142)
-- Has_Nested_Block_With_Handler (Flag101)
-- Has_Out_Or_In_Out_Parameter (Flag110)
- -- Has_Postconditions (Flag240)
-- Has_Recursive_Call (Flag143)
-- Is_Abstract_Subprogram (Flag19) (non-generic case only)
-- Is_Called (Flag102) (non-generic case only)
-- Linker_Section_Pragma (Node33)
-- Contract (Node34)
-- Has_Invariants (Flag232)
- -- Has_Postconditions (Flag240)
-- Is_Machine_Code_Subprogram (Flag137)
-- Is_Pure (Flag44)
-- Is_Intrinsic_Subprogram (Flag64)
-- E_Procedure
-- E_Generic_Procedure
- -- Postcondition_Proc (Node8) (non-generic case only)
-- Renaming_Map (Uint9)
-- Handler_Records (List10) (non-generic case only)
-- Protected_Body_Subprogram (Node11)
-- Next_Inlined_Subprogram (Node12)
-- Elaboration_Entity (Node13)
+ -- Postconditions_Proc (Node14) (non-generic case only)
-- DT_Position (Uint15)
-- DTC_Entity (Node16)
-- First_Entity (Node17)
-- Discard_Names (Flag88)
-- Has_Anonymous_Master (Flag253)
-- Has_Completion (Flag26)
+ -- Has_Expanded_Contract (Flag240) (non-generic case only)
-- Has_Invariants (Flag232)
-- Has_Master_Entity (Flag21)
-- Has_Nested_Block_With_Handler (Flag101)
- -- Has_Postconditions (Flag240)
-- Is_Abstract_Subprogram (Flag19) (non-generic case only)
-- Is_Asynchronous (Flag81)
-- Is_Called (Flag102) (non-generic case only)
function Has_Dynamic_Predicate_Aspect (Id : E) return B;
function Has_Enumeration_Rep_Clause (Id : E) return B;
function Has_Exit (Id : E) return B;
+ function Has_Expanded_Contract (Id : E) return B;
function Has_Forward_Instantiation (Id : E) return B;
function Has_Fully_Qualified_Name (Id : E) return B;
function Has_Gigi_Rep_Item (Id : E) return B;
function Has_Object_Size_Clause (Id : E) return B;
function Has_Out_Or_In_Out_Parameter (Id : E) return B;
function Has_Per_Object_Constraint (Id : E) return B;
- function Has_Postconditions (Id : E) return B;
function Has_Pragma_Controlled (Id : E) return B;
function Has_Pragma_Elaborate_Body (Id : E) return B;
function Has_Pragma_Inline (Id : E) return B;
function Part_Of_Constituents (Id : E) return L;
function Partial_View_Has_Unknown_Discr (Id : E) return B;
function Pending_Access_Types (Id : E) return L;
- function Postcondition_Proc (Id : E) return E;
+ function Postconditions_Proc (Id : E) return E;
function Prival (Id : E) return E;
function Prival_Link (Id : E) return E;
function Private_Dependents (Id : E) return L;
procedure Set_Has_Dynamic_Predicate_Aspect (Id : E; V : B := True);
procedure Set_Has_Enumeration_Rep_Clause (Id : E; V : B := True);
procedure Set_Has_Exit (Id : E; V : B := True);
+ procedure Set_Has_Expanded_Contract (Id : E; V : B := True);
procedure Set_Has_Forward_Instantiation (Id : E; V : B := True);
procedure Set_Has_Fully_Qualified_Name (Id : E; V : B := True);
procedure Set_Has_Gigi_Rep_Item (Id : E; V : B := True);
procedure Set_Has_Object_Size_Clause (Id : E; V : B := True);
procedure Set_Has_Out_Or_In_Out_Parameter (Id : E; V : B := True);
procedure Set_Has_Per_Object_Constraint (Id : E; V : B := True);
- procedure Set_Has_Postconditions (Id : E; V : B := True);
procedure Set_Has_Pragma_Controlled (Id : E; V : B := True);
procedure Set_Has_Pragma_Elaborate_Body (Id : E; V : B := True);
procedure Set_Has_Pragma_Inline (Id : E; V : B := True);
procedure Set_Part_Of_Constituents (Id : E; V : L);
procedure Set_Partial_View_Has_Unknown_Discr (Id : E; V : B := True);
procedure Set_Pending_Access_Types (Id : E; V : L);
- procedure Set_Postcondition_Proc (Id : E; V : E);
+ procedure Set_Postconditions_Proc (Id : E; V : E);
procedure Set_Prival (Id : E; V : E);
procedure Set_Prival_Link (Id : E; V : E);
procedure Set_Private_Dependents (Id : E; V : L);
pragma Inline (Has_Dynamic_Predicate_Aspect);
pragma Inline (Has_Enumeration_Rep_Clause);
pragma Inline (Has_Exit);
+ pragma Inline (Has_Expanded_Contract);
pragma Inline (Has_Forward_Instantiation);
pragma Inline (Has_Fully_Qualified_Name);
pragma Inline (Has_Gigi_Rep_Item);
pragma Inline (Has_Object_Size_Clause);
pragma Inline (Has_Out_Or_In_Out_Parameter);
pragma Inline (Has_Per_Object_Constraint);
- pragma Inline (Has_Postconditions);
pragma Inline (Has_Pragma_Controlled);
pragma Inline (Has_Pragma_Elaborate_Body);
pragma Inline (Has_Pragma_Inline);
pragma Inline (Part_Of_Constituents);
pragma Inline (Partial_View_Has_Unknown_Discr);
pragma Inline (Pending_Access_Types);
- pragma Inline (Postcondition_Proc);
+ pragma Inline (Postconditions_Proc);
pragma Inline (Prival);
pragma Inline (Prival_Link);
pragma Inline (Private_Dependents);
pragma Inline (Set_Has_Dynamic_Predicate_Aspect);
pragma Inline (Set_Has_Enumeration_Rep_Clause);
pragma Inline (Set_Has_Exit);
+ pragma Inline (Set_Has_Expanded_Contract);
pragma Inline (Set_Has_Forward_Instantiation);
pragma Inline (Set_Has_Fully_Qualified_Name);
pragma Inline (Set_Has_Gigi_Rep_Item);
pragma Inline (Set_Has_Object_Size_Clause);
pragma Inline (Set_Has_Out_Or_In_Out_Parameter);
pragma Inline (Set_Has_Per_Object_Constraint);
- pragma Inline (Set_Has_Postconditions);
pragma Inline (Set_Has_Pragma_Controlled);
pragma Inline (Set_Has_Pragma_Elaborate_Body);
pragma Inline (Set_Has_Pragma_Inline);
pragma Inline (Set_Part_Of_Constituents);
pragma Inline (Set_Partial_View_Has_Unknown_Discr);
pragma Inline (Set_Pending_Access_Types);
- pragma Inline (Set_Postcondition_Proc);
+ pragma Inline (Set_Postconditions_Proc);
pragma Inline (Set_Prival);
pragma Inline (Set_Prival_Link);
pragma Inline (Set_Private_Dependents);
declare
Rtyp : constant Entity_Id := Root_Type (P_Type);
- Dnn : Entity_Id;
- Decl : Node_Id;
Expr : Node_Id;
begin
-- Read the internal tag (RM 13.13.2(34)) and use it to
- -- initialize a dummy tag object:
+ -- initialize a dummy tag value:
- -- Dnn : Ada.Tags.Tag :=
- -- Descendant_Tag (String'Input (Strm), P_Type);
+ -- Descendant_Tag (String'Input (Strm), P_Type);
- -- This dummy object is used only to provide a controlling
+ -- This value is used only to provide a controlling
-- argument for the eventual _Input call. Descendant_Tag is
-- called rather than Internal_Tag to ensure that we have a
-- tag for a type that is descended from the prefix type and
-- required for Ada 2005 because tagged types can be
-- extended in nested scopes (AI-344).
+ -- Note: we used to generate an explicit declaration of a
+ -- constant Ada.Tags.Tag object, and use an occurrence of
+ -- this constant in Cntrl, but this caused a secondary stack
+ -- leak.
+
Expr :=
Make_Function_Call (Loc,
Name =>
Make_Attribute_Reference (Loc,
Prefix => New_Occurrence_Of (P_Type, Loc),
Attribute_Name => Name_Tag)));
-
- Dnn := Make_Temporary (Loc, 'D', Expr);
-
- Decl :=
- Make_Object_Declaration (Loc,
- Defining_Identifier => Dnn,
- Object_Definition =>
- New_Occurrence_Of (RTE (RE_Tag), Loc),
- Expression => Expr);
-
- Insert_Action (N, Decl);
+ Set_Etype (Expr, RTE (RE_Tag));
-- Now we need to get the entity for the call, and construct
-- a function call node, where we preset a reference to Dnn
-- tagged object).
Fname := Find_Prim_Op (Rtyp, TSS_Stream_Input);
- Cntrl :=
- Unchecked_Convert_To (P_Type,
- New_Occurrence_Of (Dnn, Loc));
+ Cntrl := Unchecked_Convert_To (P_Type, Expr);
Set_Etype (Cntrl, P_Type);
Set_Parent (Cntrl, N);
end;
-- secondary stack using 'reference.
procedure Expand_Non_Function_Return (N : Node_Id);
- -- Called by Expand_N_Simple_Return_Statement in case we're returning from
- -- a procedure body, entry body, accept statement, or extended return
- -- statement. Note that all non-function returns are simple return
- -- statements.
+ -- Expand a simple return statement found in a procedure body, entry body,
+ -- accept statement, or an extended return statement. Note that all non-
+ -- function returns are simple return statements.
function Expand_Protected_Object_Reference
(N : Node_Id;
----------------
procedure Add_Return (S : List_Id) is
- Last_Stm : Node_Id;
- Loc : Source_Ptr;
+ Last_Stmt : Node_Id;
+ Loc : Source_Ptr;
+ Stmt : Node_Id;
begin
-- Get last statement, ignoring any Pop_xxx_Label nodes, which are
-- not relevant in this context since they are not executable.
- Last_Stm := Last (S);
- while Nkind (Last_Stm) in N_Pop_xxx_Label loop
- Prev (Last_Stm);
+ Last_Stmt := Last (S);
+ while Nkind (Last_Stmt) in N_Pop_xxx_Label loop
+ Prev (Last_Stmt);
end loop;
-- Now insert return unless last statement is a transfer
- if not Is_Transfer (Last_Stm) then
+ if not Is_Transfer (Last_Stmt) then
-- The source location for the return is the end label of the
-- procedure if present. Otherwise use the sloc of the last
if Nkind (Parent (S)) = N_Exception_Handler
and then not Comes_From_Source (Parent (S))
then
- Loc := Sloc (Last_Stm);
+ Loc := Sloc (Last_Stmt);
elsif Present (End_Label (H)) then
Loc := Sloc (End_Label (H));
else
- Loc := Sloc (Last_Stm);
+ Loc := Sloc (Last_Stmt);
end if;
- declare
- Rtn : constant Node_Id := Make_Simple_Return_Statement (Loc);
+ -- Append return statement, and set analyzed manually. We can't
+ -- call Analyze on this return since the scope is wrong.
- begin
- -- Append return statement, and set analyzed manually. We can't
- -- call Analyze on this return since the scope is wrong.
+ -- Note: it almost works to push the scope and then do the Analyze
+ -- call, but something goes wrong in some weird cases and it is
+ -- not worth worrying about ???
- -- Note: it almost works to push the scope and then do the
- -- Analyze call, but something goes wrong in some weird cases
- -- and it is not worth worrying about ???
+ Stmt := Make_Simple_Return_Statement (Loc);
- -- The return statement is handled properly, and the call
- -- to the postcondition, inserted below, does not require
- -- information from the body either. However, that call is
- -- analyzed in the enclosing scope, and an elaboration check
- -- might improperly be added to it. A guard in Sem_Elab is
- -- needed to prevent that spurious check, see Check_Elab_Call.
+ -- The return statement is handled properly, and the call to the
+ -- postcondition, inserted below, does not require information
+ -- from the body either. However, that call is analyzed in the
+ -- enclosing scope, and an elaboration check might improperly be
+ -- added to it. A guard in Sem_Elab is needed to prevent that
+ -- spurious check, see Check_Elab_Call.
- Append_To (S, Rtn);
- Set_Analyzed (Rtn);
+ Append_To (S, Stmt);
+ Set_Analyzed (Stmt);
- -- Call _Postconditions procedure if appropriate. We need to
- -- do this explicitly because we did not analyze the generated
- -- return statement above, so the call did not get inserted.
+ -- Call the _Postconditions procedure if the related subprogram
+ -- has contract assertions that need to be verified on exit.
- if Ekind (Spec_Id) = E_Procedure
- and then Has_Postconditions (Spec_Id)
- then
- pragma Assert (Present (Postcondition_Proc (Spec_Id)));
- Insert_Action (Rtn,
- Make_Procedure_Call_Statement (Loc,
- Name =>
- New_Occurrence_Of
- (Postcondition_Proc (Spec_Id), Loc)));
- end if;
- end;
+ if Ekind (Spec_Id) = E_Procedure
+ and then Present (Postconditions_Proc (Spec_Id))
+ then
+ Insert_Action (Stmt,
+ Make_Procedure_Call_Statement (Loc,
+ Name =>
+ New_Occurrence_Of (Postconditions_Proc (Spec_Id), Loc)));
+ end if;
end if;
end Add_Return;
-- the initial value itself (which may well be invalid).
-- Predicate checks are disabled as well (RM 6.4.1 (13/3))
- A := Make_Assignment_Statement (Loc,
+ A :=
+ Make_Assignment_Statement (Loc,
Name => New_Occurrence_Of (F, Loc),
Expression => Get_Simple_Init_Val (Etype (F), N));
Set_Suppress_Assignment_Checks (A);
procedure Expand_Non_Function_Return (N : Node_Id) is
pragma Assert (No (Expression (N)));
- Loc : constant Source_Ptr := Sloc (N);
- Scope_Id : Entity_Id :=
- Return_Applies_To (Return_Statement_Entity (N));
- Kind : constant Entity_Kind := Ekind (Scope_Id);
- Call : Node_Id;
- Acc_Stat : Node_Id;
- Goto_Stat : Node_Id;
- Lab_Node : Node_Id;
+ Loc : constant Source_Ptr := Sloc (N);
+ Scope_Id : Entity_Id := Return_Applies_To (Return_Statement_Entity (N));
+ Kind : constant Entity_Kind := Ekind (Scope_Id);
+ Call : Node_Id;
+ Acc_Stat : Node_Id;
+ Goto_Stat : Node_Id;
+ Lab_Node : Node_Id;
begin
- -- Call _Postconditions procedure if procedure with active
- -- postconditions. Here, we use the Postcondition_Proc attribute,
- -- which is needed for implicitly-generated returns. Functions
- -- never have implicitly-generated returns, and there's no
- -- room for Postcondition_Proc in E_Function, so we look up the
- -- identifier Name_uPostconditions for function returns (see
- -- Expand_Simple_Function_Return).
-
- if Ekind (Scope_Id) = E_Procedure
- and then Has_Postconditions (Scope_Id)
+ -- Call the _Postconditions procedure if the related subprogram has
+ -- contract assertions that need to be verified on exit.
+
+ if Ekind_In (Scope_Id, E_Entry, E_Entry_Family, E_Procedure)
+ and then Present (Postconditions_Proc (Scope_Id))
then
- pragma Assert (Present (Postcondition_Proc (Scope_Id)));
Insert_Action (N,
Make_Procedure_Call_Statement (Loc,
- Name => New_Occurrence_Of (Postcondition_Proc (Scope_Id), Loc)));
+ Name => New_Occurrence_Of (Postconditions_Proc (Scope_Id), Loc)));
end if;
-- If it is a return from a procedure do no extra steps
end;
end if;
- -- Generate call to postcondition checks if they are present
+ -- Call the _Postconditions procedure if the related function has
+ -- contract assertions that need to be verified on exit.
if Ekind (Scope_Id) = E_Function
- and then Has_Postconditions (Scope_Id)
+ and then Present (Postconditions_Proc (Scope_Id))
then
-- We are going to reference the returned value twice in this case,
-- once in the call to _Postconditions, and once in the actual return
end;
end if;
- -- Generate call to _postconditions
+ -- Generate call to _Postconditions
Insert_Action (Exp,
Make_Procedure_Call_Statement (Loc,
- Name => Make_Identifier (Loc, Name_uPostconditions),
+ Name =>
+ New_Occurrence_Of (Postconditions_Proc (Scope_Id), Loc),
Parameter_Associations => New_List (Duplicate_Subexpr (Exp))));
end if;
-- Expand_Subprogram_Contract --
--------------------------------
- procedure Expand_Subprogram_Contract
- (N : Node_Id;
- Spec_Id : Entity_Id;
- Body_Id : Entity_Id)
- is
+ procedure Expand_Subprogram_Contract (N : Node_Id) is
+ Body_Id : constant Entity_Id := Defining_Entity (N);
+ Spec_Id : constant Entity_Id := Corresponding_Spec (N);
+
procedure Add_Invariant_And_Predicate_Checks
(Subp_Id : Entity_Id;
Stmts : in out List_Id;
-- the routine corrects the references of all formals of Inher_Id to
-- point to the formals of Subp_Id.
- procedure Collect_Body_Postconditions (Stmts : in out List_Id);
- -- Process all postconditions found in the declarations of the body. The
- -- routine appends the pragma Check equivalents to list Stmts.
-
- procedure Collect_Spec_Postconditions
- (Subp_Id : Entity_Id;
- Stmts : in out List_Id);
- -- Process all [inherited] postconditions of subprogram spec Subp_Id.
- -- The routine appends the pragma Check equivalents to list Stmts.
+ procedure Process_Contract_Cases (Stmts : in out List_Id);
+ -- Process pragma Contract_Cases. This routine prepends items to the
+ -- body declarations and appends items to list Stmts.
- procedure Collect_Spec_Preconditions (Subp_Id : Entity_Id);
- -- Process all [inherited] preconditions of subprogram spec Subp_Id. The
- -- routine prepends the pragma Check equivalents to the declarations of
- -- the body.
+ procedure Process_Postconditions (Stmts : in out List_Id);
+ -- Collect all [inherited] spec and body postconditions and accumulate
+ -- their pragma Check equivalents in list Stmts.
- procedure Prepend_To_Declarations (Item : Node_Id);
- -- Prepend a single item to the declarations of the subprogram body
-
- procedure Process_Contract_Cases
- (Subp_Id : Entity_Id;
- Stmts : in out List_Id);
- -- Process pragma Contract_Cases of subprogram spec Subp_Id. The routine
- -- appends the expanded code to list Stmts.
+ procedure Process_Preconditions;
+ -- Collect all [inherited] spec and body preconditions and prepend their
+ -- pragma Check equivalents to the declarations of the body.
----------------------------------------
-- Add_Invariant_And_Predicate_Checks --
begin
Result := Empty;
- -- Do not generate any checks if no code is being generated
-
- if not Expander_Active then
- return;
- end if;
-
-- Process the result of a function
- if Ekind_In (Subp_Id, E_Function, E_Generic_Function) then
+ if Ekind (Subp_Id) = E_Function then
Typ := Etype (Subp_Id);
-- Generate _Result which is used in procedure _Postconditions to
-- Local variables
- Loc : constant Source_Ptr := Sloc (N);
- Params : List_Id := No_List;
- Proc_Id : Entity_Id;
+ Loc : constant Source_Ptr := Sloc (N);
+ Params : List_Id := No_List;
+ Proc_Bod : Node_Id;
+ Proc_Id : Entity_Id;
-- Start of processing for Build_Postconditions_Procedure
begin
- -- Do not create the routine if no code is being generated
-
- if not Expander_Active then
- return;
-
-- Nothing to do if there are no actions to check on exit
- elsif No (Stmts) then
+ if No (Stmts) then
return;
end if;
Proc_Id := Make_Defining_Identifier (Loc, Name_uPostconditions);
+ Set_Debug_Info_Needed (Proc_Id);
+ Set_Postconditions_Proc (Subp_Id, Proc_Id);
-- The related subprogram is a function, create the specification of
-- parameter _Result.
-- order reference. The body of _Postconditions must be placed after
-- the declaration of Temp to preserve correct visibility.
- -- Note that we set an explicit End_Label in order to override the
- -- sloc of the implicit RETURN statement, and prevent it from
- -- inheriting the sloc of one of the postconditions: this would cause
- -- confusing debug info to be produced, interfering with coverage
- -- analysis tools.
+ -- Set an explicit End_Lavel to override the sloc of the implicit
+ -- RETURN statement, and prevent it from inheriting the sloc of one
+ -- the postconditions: this would cause confusing debug into to be
+ -- produced, interfering with coverage analysis tools.
- Insert_Before_First_Source_Declaration (
+ Proc_Bod :=
Make_Subprogram_Body (Loc,
Specification =>
Make_Procedure_Specification (Loc,
Handled_Statement_Sequence =>
Make_Handled_Sequence_Of_Statements (Loc,
Statements => Stmts,
- End_Label => Make_Identifier (Loc, Chars (Proc_Id)))));
-
- -- Set the attributes of the related subprogram to capture the
- -- generated procedure.
-
- if Ekind_In (Subp_Id, E_Generic_Procedure, E_Procedure) then
- Set_Postcondition_Proc (Subp_Id, Proc_Id);
- end if;
+ End_Label => Make_Identifier (Loc, Chars (Proc_Id))));
- Set_Has_Postconditions (Subp_Id);
+ Insert_Before_First_Source_Declaration (Proc_Bod);
+ Analyze (Proc_Bod);
end Build_Postconditions_Procedure;
-----------------------------------
Set_Comes_From_Source (Check_Prag, False);
Set_Analyzed (Check_Prag, False);
- -- For a postcondition pragma within a generic, preserve the pragma
- -- for later expansion. This is also used when an error was detected,
- -- thus setting Expander_Active to False.
-
- if Prag_Nam = Name_Postcondition and then not Expander_Active then
- return Check_Prag;
- end if;
-
if Present (Corresponding_Aspect (Prag)) then
Nam := Chars (Identifier (Corresponding_Aspect (Prag)));
else
return Check_Prag;
end Build_Pragma_Check_Equivalent;
- ---------------------------------
- -- Collect_Body_Postconditions --
- ---------------------------------
+ ----------------------------
+ -- Process_Contract_Cases --
+ ----------------------------
+
+ procedure Process_Contract_Cases (Stmts : in out List_Id) is
+ procedure Process_Contract_Cases_For (Subp_Id : Entity_Id);
+ -- Process pragma Contract_Cases for subprogram Subp_Id
- procedure Collect_Body_Postconditions (Stmts : in out List_Id) is
- procedure Collect_Body_Postconditions_Of_Kind (Post_Nam : Name_Id);
- -- Process all postconditions of the kind denoted by Post_Nam
+ --------------------------------
+ -- Process_Contract_Cases_For --
+ --------------------------------
- -----------------------------------------
- -- Collect_Body_Postconditions_Of_Kind --
- -----------------------------------------
+ procedure Process_Contract_Cases_For (Subp_Id : Entity_Id) is
+ Items : constant Node_Id := Contract (Subp_Id);
+ Prag : Node_Id;
- procedure Collect_Body_Postconditions_Of_Kind (Post_Nam : Name_Id) is
- procedure Collect_Body_Postconditions_In_Decls
- (First_Decl : Node_Id);
- -- Process all postconditions found in a declarative list starting
- -- with declaration First_Decl.
+ begin
+ if Present (Items) then
+ Prag := Contract_Test_Cases (Items);
+ while Present (Prag) loop
+ if Pragma_Name (Prag) = Name_Contract_Cases then
+ Expand_Contract_Cases
+ (CCs => Prag,
+ Subp_Id => Subp_Id,
+ Decls => Declarations (N),
+ Stmts => Stmts);
+ end if;
- ------------------------------------------
- -- Collect_Body_Postconditions_In_Decls --
- ------------------------------------------
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end if;
+ end Process_Contract_Cases_For;
- procedure Collect_Body_Postconditions_In_Decls
- (First_Decl : Node_Id)
- is
- Check_Prag : Node_Id;
- Decl : Node_Id;
+ -- Start of processing for Process_Contract_Cases
- begin
- -- Inspect the declarative list looking for a pragma that
- -- matches the desired name.
+ begin
+ Process_Contract_Cases_For (Body_Id);
- Decl := First_Decl;
- while Present (Decl) loop
+ if Present (Spec_Id) then
+ Process_Contract_Cases_For (Spec_Id);
+ end if;
+ end Process_Contract_Cases;
- -- Note that non-matching pragmas are skipped
+ ----------------------------
+ -- Process_Postconditions --
+ ----------------------------
- if Nkind (Decl) = N_Pragma then
- if Pragma_Name (Decl) = Post_Nam then
- if not Analyzed (Decl) then
- Analyze (Decl);
- end if;
+ procedure Process_Postconditions (Stmts : in out List_Id) is
+ procedure Process_Body_Postconditions (Post_Nam : Name_Id);
+ -- Collect all [refined] postconditions of a specific kind denoted
+ -- by Post_Nam that belong to the body and generate pragma Check
+ -- equivalents in list Stmts.
+
+ procedure Process_Spec_Postconditions;
+ -- Collect all [inherited] postconditions of the spec and generate
+ -- pragma Check equivalents in list Stmts.
- Check_Prag := Build_Pragma_Check_Equivalent (Decl);
+ ---------------------------------
+ -- Process_Body_Postconditions --
+ ---------------------------------
- if Expander_Active then
- Append_Enabled_Item
- (Item => Check_Prag,
- List => Stmts);
+ procedure Process_Body_Postconditions (Post_Nam : Name_Id) is
+ Items : constant Node_Id := Contract (Body_Id);
+ Unit_Decl : constant Node_Id := Parent (N);
+ Decl : Node_Id;
+ Prag : Node_Id;
- -- If analyzing a generic unit, save pragma for later
+ begin
+ -- Process the contract
- else
- Prepend_To_Declarations (Check_Prag);
- end if;
+ if Present (Items) then
+ Prag := Pre_Post_Conditions (Items);
+ while Present (Prag) loop
+ if Pragma_Name (Prag) = Post_Nam then
+ Append_Enabled_Item
+ (Item => Build_Pragma_Check_Equivalent (Prag),
+ List => Stmts);
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end if;
+
+ -- The subprogram body being processed is actually the proper body
+ -- of a stub with a corresponding spec. The subprogram stub may
+ -- carry a postcondition pragma in which case it must be taken
+ -- into account. The pragma appears after the stub.
+
+ if Present (Spec_Id) and then Nkind (Unit_Decl) = N_Subunit then
+ Decl := Next (Corresponding_Stub (Unit_Decl));
+ while Present (Decl) loop
+
+ -- Note that non-matching pragmas are skipped
+
+ if Nkind (Decl) = N_Pragma then
+ if Pragma_Name (Decl) = Post_Nam then
+ Append_Enabled_Item
+ (Item => Build_Pragma_Check_Equivalent (Decl),
+ List => Stmts);
end if;
-- Skip internally generated code
Next (Decl);
end loop;
- end Collect_Body_Postconditions_In_Decls;
-
- -- Local variables
+ end if;
+ end Process_Body_Postconditions;
- Unit_Decl : constant Node_Id := Parent (N);
+ ---------------------------------
+ -- Process_Spec_Postconditions --
+ ---------------------------------
- -- Start of processing for Collect_Body_Postconditions_Of_Kind
+ procedure Process_Spec_Postconditions is
+ Subps : constant Subprogram_List :=
+ Inherited_Subprograms (Spec_Id);
+ Items : Node_Id;
+ Prag : Node_Id;
+ Subp_Id : Entity_Id;
begin
- pragma Assert (Nam_In (Post_Nam, Name_Postcondition,
- Name_Refined_Post));
+ -- Process the contract
- -- Inspect the declarations of the subprogram body looking for a
- -- pragma that matches the desired name.
+ Items := Contract (Spec_Id);
- Collect_Body_Postconditions_In_Decls
- (First_Decl => First (Declarations (N)));
-
- -- The subprogram body being processed is actually the proper body
- -- of a stub with a corresponding spec. The subprogram stub may
- -- carry a postcondition pragma in which case it must be taken
- -- into account. The pragma appears after the stub.
+ if Present (Items) then
+ Prag := Pre_Post_Conditions (Items);
+ while Present (Prag) loop
+ if Pragma_Name (Prag) = Name_Postcondition then
+ Append_Enabled_Item
+ (Item => Build_Pragma_Check_Equivalent (Prag),
+ List => Stmts);
+ end if;
- if Present (Spec_Id) and then Nkind (Unit_Decl) = N_Subunit then
- Collect_Body_Postconditions_In_Decls
- (First_Decl => Next (Corresponding_Stub (Unit_Decl)));
+ Prag := Next_Pragma (Prag);
+ end loop;
end if;
- end Collect_Body_Postconditions_Of_Kind;
-
- -- Start of processing for Collect_Body_Postconditions
-
- begin
- Collect_Body_Postconditions_Of_Kind (Name_Refined_Post);
- Collect_Body_Postconditions_Of_Kind (Name_Postcondition);
- end Collect_Body_Postconditions;
-
- ---------------------------------
- -- Collect_Spec_Postconditions --
- ---------------------------------
-
- procedure Collect_Spec_Postconditions
- (Subp_Id : Entity_Id;
- Stmts : in out List_Id)
- is
- Inher_Subps : constant Subprogram_List :=
- Inherited_Subprograms (Subp_Id);
- Check_Prag : Node_Id;
- Prag : Node_Id;
- Inher_Subp_Id : Entity_Id;
-
- begin
- -- Process the contract of the spec
- Prag := Pre_Post_Conditions (Contract (Subp_Id));
- while Present (Prag) loop
- if Pragma_Name (Prag) = Name_Postcondition then
- Check_Prag := Build_Pragma_Check_Equivalent (Prag);
+ -- Process the contracts of all inherited subprograms, looking for
+ -- class-wide postconditions.
- if Expander_Active then
- Append_Enabled_Item
- (Item => Check_Prag,
- List => Stmts);
+ for Index in Subps'Range loop
+ Subp_Id := Subps (Index);
+ Items := Contract (Subp_Id);
- -- When analyzing a generic unit, save the pragma for later
+ if Present (Items) then
+ Prag := Pre_Post_Conditions (Items);
+ while Present (Prag) loop
+ if Pragma_Name (Prag) = Name_Postcondition
+ and then Class_Present (Prag)
+ then
+ Append_Enabled_Item
+ (Item =>
+ Build_Pragma_Check_Equivalent
+ (Prag => Prag,
+ Subp_Id => Spec_Id,
+ Inher_Id => Subp_Id),
+ List => Stmts);
+ end if;
- else
- Prepend_To_Declarations (Check_Prag);
+ Prag := Next_Pragma (Prag);
+ end loop;
end if;
- end if;
-
- Prag := Next_Pragma (Prag);
- end loop;
-
- -- Process the contracts of all inherited subprograms, looking for
- -- class-wide postconditions.
-
- for Index in Inher_Subps'Range loop
- Inher_Subp_Id := Inher_Subps (Index);
+ end loop;
+ end Process_Spec_Postconditions;
- Prag := Pre_Post_Conditions (Contract (Inher_Subp_Id));
- while Present (Prag) loop
- if Pragma_Name (Prag) = Name_Postcondition
- and then Class_Present (Prag)
- then
- Check_Prag :=
- Build_Pragma_Check_Equivalent
- (Prag => Prag,
- Subp_Id => Subp_Id,
- Inher_Id => Inher_Subp_Id);
+ -- Start of processing for Process_Postconditions
- if Expander_Active then
- Append_Enabled_Item
- (Item => Check_Prag,
- List => Stmts);
+ begin
+ -- The processing of postconditions is done in reverse order (body
+ -- first) to ensure the following arrangement:
- -- When analyzing a generic unit, save the pragma for later
+ -- <refined postconditions from body>
+ -- <postconditions from body>
+ -- <postconditions from spec>
+ -- <inherited postconditions>
- else
- Prepend_To_Declarations (Check_Prag);
- end if;
- end if;
+ Process_Body_Postconditions (Name_Refined_Post);
+ Process_Body_Postconditions (Name_Postcondition);
- Prag := Next_Pragma (Prag);
- end loop;
- end loop;
- end Collect_Spec_Postconditions;
+ if Present (Spec_Id) then
+ Process_Spec_Postconditions;
+ end if;
+ end Process_Postconditions;
- --------------------------------
- -- Collect_Spec_Preconditions --
- --------------------------------
+ ---------------------------
+ -- Process_Preconditions --
+ ---------------------------
- procedure Collect_Spec_Preconditions (Subp_Id : Entity_Id) is
+ procedure Process_Preconditions is
Class_Pre : Node_Id := Empty;
- -- The sole class-wide precondition pragma that applies to the
- -- subprogram.
+ -- The sole [inherited] class-wide precondition pragma that applies
+ -- to the subprogram.
- procedure Add_Or_Save_Precondition (Prag : Node_Id);
- -- Save a class-wide precondition or add a regulat precondition to
- -- the declarative list of the body.
+ Insert_Node : Node_Id := Empty;
+ -- The insertion node after which all pragma Check equivalents are
+ -- inserted.
procedure Merge_Preconditions (From : Node_Id; Into : Node_Id);
-- Merge two class-wide preconditions by "or else"-ing them. The
-- changes are accumulated in parameter Into. Update the error
-- message of Into.
- ------------------------------
- -- Add_Or_Save_Precondition --
- ------------------------------
-
- procedure Add_Or_Save_Precondition (Prag : Node_Id) is
- Check_Prag : Node_Id;
-
- begin
- Check_Prag := Build_Pragma_Check_Equivalent (Prag);
+ procedure Prepend_To_Decls (Item : Node_Id);
+ -- Prepend a single item to the declarations of the subprogram body
- -- Save the sole class-wide precondition (if any) for the next
- -- step where it will be merged with inherited preconditions.
+ procedure Prepend_To_Decls_Or_Save (Prag : Node_Id);
+ -- Save a class-wide precondition into Class_Pre or prepend a normal
+ -- precondition ot the declarations of the body and analyze it.
- if Class_Present (Prag) then
- pragma Assert (No (Class_Pre));
- Class_Pre := Check_Prag;
+ procedure Process_Inherited_Preconditions;
+ -- Collect all inherited class-wide preconditions and merge them into
+ -- one big precondition to be evaluated as pragma Check.
- -- Accumulate the corresponding Check pragmas to the top of the
- -- declarations. Prepending the items ensures that they will be
- -- evaluated in their original order.
-
- else
- Prepend_To_Declarations (Check_Prag);
- end if;
- end Add_Or_Save_Precondition;
+ procedure Process_Preconditions_For (Subp_Id : Entity_Id);
+ -- Collect all preconditions of subprogram Subp_Id and prepend their
+ -- pragma Check equivalents to the declarations of the body.
-------------------------
-- Merge_Preconditions --
end if;
end Merge_Preconditions;
- -- Local variables
-
- Inher_Subps : constant Subprogram_List :=
- Inherited_Subprograms (Subp_Id);
- Subp_Decl : constant Node_Id := Parent (Parent (Subp_Id));
- Check_Prag : Node_Id;
- Decl : Node_Id;
- Inher_Subp_Id : Entity_Id;
- Prag : Node_Id;
+ ----------------------
+ -- Prepend_To_Decls --
+ ----------------------
- -- Start of processing for Collect_Spec_Preconditions
+ procedure Prepend_To_Decls (Item : Node_Id) is
+ Decls : List_Id := Declarations (N);
- begin
- -- Process the contract of the spec
+ begin
+ -- Ensure that the body has a declarative list
- Prag := Pre_Post_Conditions (Contract (Subp_Id));
- while Present (Prag) loop
- if Pragma_Name (Prag) = Name_Precondition then
- Add_Or_Save_Precondition (Prag);
+ if No (Decls) then
+ Decls := New_List;
+ Set_Declarations (N, Decls);
end if;
- Prag := Next_Pragma (Prag);
- end loop;
+ Prepend_To (Decls, Item);
+ end Prepend_To_Decls;
- -- The subprogram declaration being processed is actually a body
- -- stub. The stub may carry a precondition pragma in which case it
- -- must be taken into account. The pragma appears after the stub.
+ ------------------------------
+ -- Prepend_To_Decls_Or_Save --
+ ------------------------------
- if Nkind (Subp_Decl) = N_Subprogram_Body_Stub then
+ procedure Prepend_To_Decls_Or_Save (Prag : Node_Id) is
+ Check_Prag : Node_Id;
- -- Inspect the declarations following the body stub
+ begin
+ Check_Prag := Build_Pragma_Check_Equivalent (Prag);
- Decl := Next (Subp_Decl);
- while Present (Decl) loop
+ -- Save the sole class-wide precondition (if any) for the next
+ -- step where it will be merged with inherited preconditions.
- -- Note that non-matching pragmas are skipped
+ if Class_Present (Prag) then
+ pragma Assert (No (Class_Pre));
+ Class_Pre := Check_Prag;
- if Nkind (Decl) = N_Pragma then
- if Pragma_Name (Decl) = Name_Precondition then
- if not Analyzed (Decl) then
- Analyze (Decl);
- end if;
+ -- Accumulate the corresponding Check pragmas at the top of the
+ -- declarations. Prepending the items ensures that they will be
+ -- evaluated in their original order.
- Add_Or_Save_Precondition (Decl);
- end if;
+ else
+ if Present (Insert_Node) then
+ Insert_After (Insert_Node, Check_Prag);
+ else
+ Prepend_To_Decls (Check_Prag);
+ end if;
- -- Skip internally generated code
+ Analyze (Check_Prag);
+ end if;
+ end Prepend_To_Decls_Or_Save;
- elsif not Comes_From_Source (Decl) then
- null;
+ -------------------------------------
+ -- Process_Inherited_Preconditions --
+ -------------------------------------
- -- Preconditions are usually grouped together. There is no need
- -- to inspect the whole declarative list.
+ procedure Process_Inherited_Preconditions is
+ Subps : constant Subprogram_List :=
+ Inherited_Subprograms (Spec_Id);
+ Check_Prag : Node_Id;
+ Items : Node_Id;
+ Prag : Node_Id;
+ Subp_Id : Entity_Id;
- else
- exit;
- end if;
+ begin
+ -- Process the contracts of all inherited subprograms, looking for
+ -- class-wide preconditions.
+
+ for Index in Subps'Range loop
+ Subp_Id := Subps (Index);
+ Items := Contract (Subp_Id);
+
+ if Present (Items) then
+ Prag := Pre_Post_Conditions (Items);
+ while Present (Prag) loop
+ if Pragma_Name (Prag) = Name_Precondition
+ and then Class_Present (Prag)
+ then
+ Check_Prag :=
+ Build_Pragma_Check_Equivalent
+ (Prag => Prag,
+ Subp_Id => Spec_Id,
+ Inher_Id => Subp_Id);
+
+ -- The spec or an inherited subprogram already yielded
+ -- a class-wide precondition. Merge the existing
+ -- precondition with the current one using "or else".
+
+ if Present (Class_Pre) then
+ Merge_Preconditions (Check_Prag, Class_Pre);
+ else
+ Class_Pre := Check_Prag;
+ end if;
+ end if;
- Next (Decl);
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end if;
end loop;
- end if;
- -- Process the contracts of all inherited subprograms, looking for
- -- class-wide preconditions.
+ -- Add the merged class-wide preconditions
- for Index in Inher_Subps'Range loop
- Inher_Subp_Id := Inher_Subps (Index);
+ if Present (Class_Pre) then
+ Prepend_To_Decls (Class_Pre);
+ Analyze (Class_Pre);
+ end if;
+ end Process_Inherited_Preconditions;
- Prag := Pre_Post_Conditions (Contract (Inher_Subp_Id));
- while Present (Prag) loop
- if Pragma_Name (Prag) = Name_Precondition
- and then Class_Present (Prag)
- then
- Check_Prag :=
- Build_Pragma_Check_Equivalent
- (Prag => Prag,
- Subp_Id => Subp_Id,
- Inher_Id => Inher_Subp_Id);
+ -------------------------------
+ -- Process_Preconditions_For --
+ -------------------------------
- -- The spec or an inherited subprogram already yielded a
- -- class-wide precondition. Merge the existing precondition
- -- with the current one using "or else".
+ procedure Process_Preconditions_For (Subp_Id : Entity_Id) is
+ Items : constant Node_Id := Contract (Subp_Id);
+ Decl : Node_Id;
+ Prag : Node_Id;
+ Subp_Decl : Node_Id;
- if Present (Class_Pre) then
- Merge_Preconditions (Check_Prag, Class_Pre);
+ begin
+ -- Process the contract
- else
- Class_Pre := Check_Prag;
+ if Present (Items) then
+ Prag := Pre_Post_Conditions (Items);
+ while Present (Prag) loop
+ if Pragma_Name (Prag) = Name_Precondition then
+ Prepend_To_Decls_Or_Save (Prag);
end if;
- end if;
- Prag := Next_Pragma (Prag);
- end loop;
- end loop;
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end if;
- -- Add the merged class-wide preconditions (if any)
+ -- The subprogram declaration being processed is actually a body
+ -- stub. The stub may carry a precondition pragma in which case it
+ -- must be taken into account. The pragma appears after the stub.
- if Present (Class_Pre) then
- Prepend_To_Declarations (Class_Pre);
- end if;
- end Collect_Spec_Preconditions;
+ Subp_Decl := Unit_Declaration_Node (Subp_Id);
- -----------------------------
- -- Prepend_To_Declarations --
- -----------------------------
+ if Nkind (Subp_Decl) = N_Subprogram_Body_Stub then
- procedure Prepend_To_Declarations (Item : Node_Id) is
- Decls : List_Id := Declarations (N);
+ -- Inspect the declarations following the body stub
- begin
- -- Ensure that the body has a declarative list
+ Decl := Next (Subp_Decl);
+ while Present (Decl) loop
- if No (Decls) then
- Decls := New_List;
- Set_Declarations (N, Decls);
- end if;
+ -- Note that non-matching pragmas are skipped
+
+ if Nkind (Decl) = N_Pragma then
+ if Pragma_Name (Decl) = Name_Precondition then
+ Prepend_To_Decls_Or_Save (Decl);
+ end if;
- Prepend_To (Decls, Item);
- end Prepend_To_Declarations;
+ -- Skip internally generated code
- ----------------------------
- -- Process_Contract_Cases --
- ----------------------------
+ elsif not Comes_From_Source (Decl) then
+ null;
- procedure Process_Contract_Cases
- (Subp_Id : Entity_Id;
- Stmts : in out List_Id)
- is
- Prag : Node_Id;
+ -- Preconditions are usually grouped together. There is no
+ -- need to inspect the whole declarative list.
+
+ else
+ exit;
+ end if;
+
+ Next (Decl);
+ end loop;
+ end if;
+ end Process_Preconditions_For;
+
+ -- Local variables
+
+ Decls : constant List_Id := Declarations (N);
+ Decl : Node_Id;
+
+ -- Start of processing for Process_Preconditions
begin
- -- Do not build the Contract_Cases circuitry if no code is being
- -- generated.
+ -- Find the last internally generate declaration starting from the
+ -- top of the body declarations. This ensures that discriminals and
+ -- subtypes are properly visible to the pragma Check equivalents.
- if not Expander_Active then
- return;
+ if Present (Decls) then
+ Decl := First (Decls);
+
+ while Present (Decl) loop
+ if not Comes_From_Source (Decl) then
+ Insert_Node := Decl;
+ exit;
+ end if;
+
+ Next (Decl);
+ end loop;
end if;
- Prag := Contract_Test_Cases (Contract (Subp_Id));
- while Present (Prag) loop
- if Pragma_Name (Prag) = Name_Contract_Cases then
- Expand_Contract_Cases
- (CCs => Prag,
- Subp_Id => Subp_Id,
- Decls => Declarations (N),
- Stmts => Stmts);
- end if;
+ -- The processing of preconditions is done in reverse order (body
+ -- first) because each pragma Check equivalent is inserted at the
+ -- top of the declarations. This ensures that the final order is
+ -- consistent with following diagram:
- Prag := Next_Pragma (Prag);
- end loop;
- end Process_Contract_Cases;
+ -- <inherited preconditions>
+ -- <preconditions from spec>
+ -- <preconditions from body>
+
+ Process_Preconditions_For (Body_Id);
+
+ if Present (Spec_Id) then
+ Process_Preconditions_For (Spec_Id);
+ Process_Inherited_Preconditions;
+ end if;
+ end Process_Preconditions;
-- Local variables
- Post_Stmts : List_Id := No_List;
- Result : Entity_Id;
- Subp_Id : Entity_Id;
+ Restore_Scope : Boolean := False;
+ Result : Entity_Id;
+ Stmts : List_Id := No_List;
+ Subp_Id : Entity_Id;
-- Start of processing for Expand_Subprogram_Contract
begin
+ -- Obtain the entity of the initial declaration
+
if Present (Spec_Id) then
Subp_Id := Spec_Id;
else
Subp_Id := Body_Id;
end if;
- -- Do not process a predicate function as its body will end up with a
- -- recursive call to itself and blow up the stack.
+ -- Do not perform expansion activity when it is not needed
- if Ekind (Subp_Id) = E_Function
- and then Is_Predicate_Function (Subp_Id)
- then
+ if not Expander_Active then
return;
- -- Do not process TSS subprograms
+ -- ASIS requires an unaltered tree
- elsif Get_TSS_Name (Subp_Id) /= TSS_Null then
+ elsif ASIS_Mode then
+ return;
+
+ -- GNATprove does not need the executable semantics of a contract
+
+ elsif GNATprove_Mode then
+ return;
+
+ -- The contract of a generic subprogram or one declared in a generic
+ -- context is not expanded as the corresponding instance will provide
+ -- the executable semantics of the contract.
+
+ elsif Is_Generic_Subprogram (Subp_Id) or else Inside_A_Generic then
+ return;
+
+ -- All subprograms carry a contract, but for some it is not significant
+ -- and should not be processed. This is a small optimization.
+
+ elsif not Has_Significant_Contract (Subp_Id) then
return;
end if;
- -- The expansion of a subprogram contract involves the relocation of
- -- various contract assertions to the declarations of the body in a
+ -- Do not re-expand the same contract. This scenario occurs when a
+ -- construct is rewritten into something else during its analysis
+ -- (expression functions for instance).
+
+ if Has_Expanded_Contract (Subp_Id) then
+ return;
+
+ -- Otherwise mark the subprogram
+
+ else
+ Set_Has_Expanded_Contract (Subp_Id);
+ end if;
+
+ -- Ensure that the formal parameters are visible when expanding all
+ -- contract items.
+
+ if not In_Open_Scopes (Subp_Id) then
+ Restore_Scope := True;
+ Push_Scope (Subp_Id);
+
+ if Is_Generic_Subprogram (Subp_Id) then
+ Install_Generic_Formals (Subp_Id);
+ else
+ Install_Formals (Subp_Id);
+ end if;
+ end if;
+
+ -- The expansion of a subprogram contract involves the creation of Check
+ -- pragmas to verify the contract assertions of the spec and body in a
-- particular order. The order is as follows:
-- function Example (...) return ... is
-- <postconditions from spec>
-- <inherited postconditions>
-- <contract case consequences>
- -- <invariant check of function result (if applicable)>
+ -- <invariant check of function result>
-- <invariant and predicate checks of parameters>
-- end _Postconditions;
-- <inherited preconditions>
-- <preconditions from spec>
-- <preconditions from body>
- -- <refined preconditions from body>
-- <contract case conditions>
-- <source declarations>
-- end Example;
-- Routine _Postconditions holds all contract assertions that must be
- -- verified on exit from the related routine.
+ -- verified on exit from the related subprogram.
- -- Collect all [inherited] preconditions from the spec, transform them
- -- into Check pragmas and add them to the declarations of the body in
- -- the order outlined above.
-
- if Present (Spec_Id) then
- Collect_Spec_Preconditions (Spec_Id);
- end if;
+ -- Step 1: Handle all preconditions. This action must come before the
+ -- processing of pragma Contract_Cases because the pragma prepends items
+ -- to the body declarations.
- -- Transform all [refined] postconditions of the body into Check
- -- pragmas. The resulting pragmas are accumulated in list Post_Stmts.
+ Process_Preconditions;
- Collect_Body_Postconditions (Post_Stmts);
+ -- Step 2: Handle all postconditions. This action must come before the
+ -- processing of pragma Contract_Cases because the pragma appends items
+ -- to list Stmts.
- -- Transform all [inherited] postconditions from the spec into Check
- -- pragmas. The resulting pragmas are accumulated in list Post_Stmts.
+ Process_Postconditions (Stmts);
- if Present (Spec_Id) then
- Collect_Spec_Postconditions (Spec_Id, Post_Stmts);
+ -- Step 3: Handle pragma Contract_Cases. This action must come before
+ -- the processing of invariants and predicates because those append
+ -- items to list Smts.
- -- Transform pragma Contract_Cases from the spec into its circuitry
+ Process_Contract_Cases (Stmts);
- Process_Contract_Cases (Spec_Id, Post_Stmts);
- end if;
+ -- Step 4: Apply invariant and predicate checks on a function result and
+ -- all formals. The resulting checks are accumulated in list Stmts.
- -- Apply invariant and predicate checks on the result of a function (if
- -- applicable) and all formals. The resulting checks are accumulated in
- -- list Post_Stmts.
+ Add_Invariant_And_Predicate_Checks (Subp_Id, Stmts, Result);
- Add_Invariant_And_Predicate_Checks (Subp_Id, Post_Stmts, Result);
+ -- Step 5: Construct procedure _Postconditions
- -- Construct procedure _Postconditions
+ Build_Postconditions_Procedure (Subp_Id, Stmts, Result);
- Build_Postconditions_Procedure (Subp_Id, Post_Stmts, Result);
+ if Restore_Scope then
+ End_Scope;
+ end if;
end Expand_Subprogram_Contract;
--------------------------------
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- This procedure contains common processing for Expand_N_Function_Call,
-- Expand_N_Procedure_Statement, and Expand_N_Entry_Call.
- procedure Expand_Subprogram_Contract
- (N : Node_Id;
- Spec_Id : Entity_Id;
- Body_Id : Entity_Id);
+ procedure Expand_Subprogram_Contract (N : Node_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. N is the body of the
- -- subprogram. Spec_Id denotes the entity of its specification. Body_Id
- -- denotes the entity of the subprogram body. This routine is not a "pure"
- -- expansion mechanism as it is invoked during analysis and may perform
- -- actions for generic subprograms or set up contract assertions for ASIS.
+ -- well as Contract_Cases, invariants and predicates. N denotes the body of
+ -- the subprogram.
procedure Freeze_Subprogram (N : Node_Id);
-- generate the appropriate expansions related to Subprogram freeze
-----------------------
procedure Build_PPC_Wrapper (E : Entity_Id; Decl : Node_Id) is
+ Items : constant Node_Id := Contract (E);
Loc : constant Source_Ptr := Sloc (E);
- Synch_Type : constant Entity_Id := Scope (E);
-
- Wrapper_Id : constant Entity_Id :=
- Make_Defining_Identifier (Loc,
- Chars => New_External_Name (Chars (E), 'E'));
- -- the wrapper procedure name
-
- Wrapper_Body : Node_Id;
-
- Synch_Id : constant Entity_Id :=
- Make_Defining_Identifier (Loc,
- Chars => New_External_Name (Chars (Scope (E)), 'A'));
- -- The parameter that designates the synchronized object in the call
-
- Actuals : constant List_Id := New_List;
- -- The actuals in the entry call
-
- Decls : constant List_Id := New_List;
-
+ Synch_Type : constant Entity_Id := Scope (E);
+ Actuals : List_Id;
+ Decls : List_Id;
Entry_Call : Node_Id;
Entry_Name : Node_Id;
-
- Specs : List_Id;
- -- The specification of the wrapper procedure
+ Params : List_Id;
+ Prag : Node_Id;
+ Synch_Id : Entity_Id;
+ Wrapper_Id : Entity_Id;
begin
-
- -- Only build the wrapper if entry has pre/postconditions.
+ -- Only build the wrapper if entry has pre/postconditions
-- Should this be done unconditionally instead ???
- declare
- P : Node_Id;
+ if Present (Items) then
+ Prag := Pre_Post_Conditions (Items);
- begin
- P := Pre_Post_Conditions (Contract (E));
-
- if No (P) then
+ if No (Prag) then
return;
end if;
-- Transfer ppc pragmas to the declarations of the wrapper
- while Present (P) loop
- if Nam_In (Pragma_Name (P), Name_Precondition,
- Name_Postcondition)
+ Decls := New_List;
+
+ while Present (Prag) loop
+ if Nam_In (Pragma_Name (Prag), Name_Precondition,
+ Name_Postcondition)
then
- Append (Relocate_Node (P), Decls);
+ Append (Relocate_Node (Prag), Decls);
Set_Analyzed (Last (Decls), False);
end if;
- P := Next_Pragma (P);
+ Prag := Next_Pragma (Prag);
end loop;
- end;
+ else
+ return;
+ end if;
+
+ Actuals := New_List;
+ Synch_Id :=
+ Make_Defining_Identifier (Loc,
+ Chars => New_External_Name (Chars (Scope (E)), 'A'));
-- First formal is synchronized object
- Specs := New_List (
+ Params := New_List (
Make_Parameter_Specification (Loc,
Defining_Identifier => Synch_Id,
- Out_Present => True,
- In_Present => True,
+ Out_Present => True,
+ In_Present => True,
Parameter_Type => New_Occurrence_Of (Scope (E), Loc)));
Entry_Name :=
Index : constant Entity_Id :=
Make_Defining_Identifier (Loc, Name_I);
begin
- Append_To (Specs,
+ Append_To (Params,
Make_Parameter_Specification (Loc,
Defining_Identifier => Index,
Parameter_Type =>
In_Present => In_Present (Parent (Form)),
Parameter_Type => New_Occurrence_Of (Etype (Form), Loc));
- Append (Parm_Spec, Specs);
+ Append (Parm_Spec, Params);
Append (New_Occurrence_Of (New_Form, Loc), Actuals);
Next_Formal (Form);
end loop;
end;
end if;
+ Wrapper_Id :=
+ Make_Defining_Identifier (Loc, New_External_Name (Chars (E), 'E'));
Set_PPC_Wrapper (E, Wrapper_Id);
- Wrapper_Body :=
+
+ -- The wrapper body is analyzed when the enclosing type is frozen
+
+ Append_Freeze_Action (Defining_Entity (Decl),
Make_Subprogram_Body (Loc,
Specification =>
Make_Procedure_Specification (Loc,
Defining_Unit_Name => Wrapper_Id,
- Parameter_Specifications => Specs),
+ Parameter_Specifications => Params),
Declarations => Decls,
Handled_Statement_Sequence =>
Make_Handled_Sequence_Of_Statements (Loc,
- Statements => New_List (Entry_Call)));
-
- -- The wrapper body is analyzed when the enclosing type is frozen
-
- Append_Freeze_Action (Defining_Entity (Decl), Wrapper_Body);
+ Statements => New_List (Entry_Call))));
end Build_PPC_Wrapper;
--------------------------
Ent := First_Entity (Tasktyp);
while Present (Ent) loop
if Ekind_In (Ent, E_Entry, E_Entry_Family)
+ and then Present (Contract (Ent))
and then Present (Pre_Post_Conditions (Contract (Ent)))
then
Build_PPC_Wrapper (Ent, N);
-- Given the entity Id of a boolean flag, generate:
-- Id : Boolean := False;
- procedure Expand_Old_In_Consequence
+ procedure Expand_Attributes_In_Consequence
(Decls : List_Id;
Evals : in out Node_Id;
Flag : Entity_Id;
Conseq : Node_Id);
-- Perform specialized expansion of all attribute 'Old references found
-- in consequence Conseq such that at runtime only prefixes coming from
- -- the selected consequence are evaluated. Any temporaries generated in
- -- the process are added to declarative list Decls. Evals is a complex
- -- if statement tasked with the evaluation of all prefixes coming from
- -- a selected consequence. Flag is the corresponding case guard flag.
- -- Conseq is the consequence expression.
+ -- the selected consequence are evaluated. Similarly expand attribute
+ -- 'Result references by replacing them with identifier _result which
+ -- resolves to the sole formal parameter of procedure _Postconditions.
+ -- Any temporaries generated in the process are added to declarations
+ -- Decls. Evals is a complex if statement tasked with the evaluation of
+ -- all prefixes coming from a single selected consequence. Flag is the
+ -- corresponding case guard flag. Conseq is the consequence expression.
function Increment (Id : Entity_Id) return Node_Id;
-- Given the entity Id of a numerical variable, generate:
Expression => New_Occurrence_Of (Standard_False, Loc));
end Declaration_Of;
- -------------------------------
- -- Expand_Old_In_Consequence --
- -------------------------------
+ --------------------------------------
+ -- Expand_Attributes_In_Consequence --
+ --------------------------------------
- procedure Expand_Old_In_Consequence
+ procedure Expand_Attributes_In_Consequence
(Decls : List_Id;
Evals : in out Node_Id;
Flag : Entity_Id;
-- The evaluation sequence expressed as assignment statements of all
-- prefixes of attribute 'Old found in the current consequence.
- function Expand_Old (N : Node_Id) return Traverse_Result;
- -- Determine whether an arbitrary node denotes attribute 'Old and if
- -- it does, perform all expansion-related actions.
+ function Expand_Attributes (N : Node_Id) return Traverse_Result;
+ -- Determine whether an arbitrary node denotes attribute 'Old or
+ -- 'Result and if it does, perform all expansion-related actions.
- ----------------
- -- Expand_Old --
- ----------------
+ -----------------------
+ -- Expand_Attributes --
+ -----------------------
- function Expand_Old (N : Node_Id) return Traverse_Result is
+ function Expand_Attributes (N : Node_Id) return Traverse_Result is
Decl : Node_Id;
Pref : Node_Id;
Temp : Entity_Id;
begin
+ -- Attribute 'Old
+
if Nkind (N) = N_Attribute_Reference
and then Attribute_Name (N) = Name_Old
then
Set_No_Initialization (Decl);
Prepend_To (Decls, Decl);
+ Analyze (Decl);
-- Evaluate the prefix, generate:
-- Temp := <Pref>;
-- generated temporary.
Rewrite (N, New_Occurrence_Of (Temp, Loc));
+
+ -- Attribute 'Result
+
+ elsif Is_Attribute_Result (N) then
+ Rewrite (N, Make_Identifier (Loc, Name_uResult));
end if;
return OK;
- end Expand_Old;
+ end Expand_Attributes;
- procedure Expand_Olds is new Traverse_Proc (Expand_Old);
+ procedure Expand_Attributes_In is
+ new Traverse_Proc (Expand_Attributes);
- -- Start of processing for Expand_Old_In_Consequence
+ -- Start of processing for Expand_Attributes_In_Consequence
begin
- -- Inspect the consequence and expand any attribute 'Old references
- -- found within.
+ -- Inspect the consequence and expand any attribute 'Old and 'Result
+ -- references found within.
+
+ Expand_Attributes_In (Conseq);
- Expand_Olds (Conseq);
+ -- The consequence does not contain any attribute 'Old references
+
+ if No (Eval_Stmts) then
+ return;
+ end if;
-- Augment the machinery to trigger the evaluation of all prefixes
-- found in the step above. If Eval is empty, then this is the first
Condition => New_Occurrence_Of (Flag, Loc),
Then_Statements => Eval_Stmts));
end if;
- end Expand_Old_In_Consequence;
+ end Expand_Attributes_In_Consequence;
---------------
-- Increment --
Conseq : Node_Id;
Conseq_Checks : Node_Id := Empty;
Count : Entity_Id;
+ Count_Decl : Node_Id;
Error_Decls : List_Id;
Flag : Entity_Id;
+ Flag_Decl : Node_Id;
+ If_Stmt : Node_Id;
Msg_Str : Entity_Id;
Multiple_PCs : Boolean;
Old_Evals : Node_Id := Empty;
+ Others_Decl : Node_Id;
Others_Flag : Entity_Id := Empty;
Post_Case : Node_Id;
-- Count : Natural := 0;
Count := Make_Temporary (Loc, 'C');
-
- Prepend_To (Decls,
+ Count_Decl :=
Make_Object_Declaration (Loc,
Defining_Identifier => Count,
Object_Definition => New_Occurrence_Of (Standard_Natural, Loc),
- Expression => Make_Integer_Literal (Loc, 0)));
+ Expression => Make_Integer_Literal (Loc, 0));
+
+ Prepend_To (Decls, Count_Decl);
+ Analyze (Count_Decl);
-- Create the base error message for multiple overlapping case guards
if Nkind (Case_Guard) = N_Others_Choice then
Others_Flag := Make_Temporary (Loc, 'F');
- Prepend_To (Decls, Declaration_Of (Others_Flag));
+ Others_Decl := Declaration_Of (Others_Flag);
+
+ Prepend_To (Decls, Others_Decl);
+ Analyze (Others_Decl);
-- Check possible overlap between a case guard and "others"
end if;
-- Inspect the consequence and perform special expansion of any
- -- attribute 'Old references found within.
+ -- attribute 'Old and 'Result references found within.
- Expand_Old_In_Consequence
+ Expand_Attributes_In_Consequence
(Decls => Decls,
Evals => Old_Evals,
Flag => Others_Flag,
-- guard.
Flag := Make_Temporary (Loc, 'F');
- Prepend_To (Decls, Declaration_Of (Flag));
+ Flag_Decl := Declaration_Of (Flag);
+
+ Prepend_To (Decls, Flag_Decl);
+ Analyze (Flag_Decl);
-- The flag is set when the case guard is evaluated to True
-- if Case_Guard then
-- Count := Count + 1;
-- end if;
- Append_To (Decls,
+ If_Stmt :=
Make_Implicit_If_Statement (CCs,
Condition => Relocate_Node (Case_Guard),
Then_Statements => New_List (
Set (Flag),
- Increment (Count))));
+ Increment (Count)));
+
+ Append_To (Decls, If_Stmt);
+ Analyze (If_Stmt);
-- Check whether this case guard overlaps with another one
end if;
-- Inspect the consequence and perform special expansion of any
- -- attribute 'Old references found within.
+ -- attribute 'Old and 'Result references found within.
- Expand_Old_In_Consequence
+ Expand_Attributes_In_Consequence
(Decls => Decls,
Evals => Old_Evals,
Flag => Flag,
end if;
Append_To (Decls, CG_Checks);
+ Analyze (CG_Checks);
-- Once all case guards are evaluated and checked, evaluate any prefixes
-- of attribute 'Old founds in the selected consequence.
- Append_To (Decls, Old_Evals);
+ if Present (Old_Evals) then
+ Append_To (Decls, Old_Evals);
+ Analyze (Old_Evals);
+ end if;
-- Raise Assertion_Error when the corresponding consequence of a case
-- guard that evaluated to True fails.
with Sem_Elab; use Sem_Elab;
with Sem_Elim; use Sem_Elim;
with Sem_Eval; use Sem_Eval;
+with Sem_Prag; use Sem_Prag;
with Sem_Res; use Sem_Res;
with Sem_Type; use Sem_Type;
with Sem_Util; use Sem_Util;
----------------------------
procedure Check_Use_In_Test_Case (Prag : Node_Id) is
- Ensures : constant Node_Id := Get_Ensures_From_CTC_Pragma (Prag);
+ Ensures : constant Node_Id := Test_Case_Arg (Prag, Name_Ensures);
Expr : Node_Id;
begin
------------
when Attribute_Result => Result : declare
- Post_Id : Entity_Id;
- -- The entity of the _Postconditions procedure
+ procedure Check_Placement_In_Check (Prag : Node_Id);
+ -- Verify that attribute 'Result appears within pragma Check that
+ -- emulates a postcondition.
- Prag : Node_Id;
- -- During pre-analysis, Prag is the enclosing pragma node if any
-
- Subp_Id : Entity_Id;
- -- The entity of the enclosing subprogram
+ procedure Check_Placement_In_Contract_Cases (Prag : Node_Id);
+ -- Verify that attribute 'Result appears within a consequence of
+ -- pragma Contract_Cases.
- begin
- -- Find the proper enclosing scope
+ procedure Check_Placement_In_Test_Case (Prag : Node_Id);
+ -- Verify that attribute 'Result appears within the Ensures argument
+ -- of pragma Test_Case.
- Post_Id := Current_Scope;
- while Present (Post_Id) loop
+ function Is_Within
+ (Nod : Node_Id;
+ Encl_Nod : Node_Id) return Boolean;
+ -- Subsidiary to Check_Placemenet_In_XXX_Case. Determine whether
+ -- arbitrary node Nod is within enclosing node Encl_Nod.
- -- Skip generated loops
+ ------------------------------
+ -- Check_Placement_In_Check --
+ ------------------------------
- if Ekind (Post_Id) = E_Loop then
- Post_Id := Scope (Post_Id);
+ procedure Check_Placement_In_Check (Prag : Node_Id) is
+ Args : constant List_Id := Pragma_Argument_Associations (Prag);
+ Nam : constant Name_Id := Chars (Get_Pragma_Arg (First (Args)));
- -- Skip the special _Parent scope generated to capture references
- -- to formals during the process of subprogram inlining.
+ begin
+ -- The "Name" argument of pragma Check denotes a postcondition
- elsif Ekind (Post_Id) = E_Function
- and then Chars (Post_Id) = Name_uParent
+ if Nam_In (Nam, Name_Post,
+ Name_Postcondition,
+ Name_Refined_Post)
then
- Post_Id := Scope (Post_Id);
+ null;
- -- Otherwise this must be _Postconditions
+ -- Otherwise the placement of attribute 'Result is illegal
else
- exit;
+ Error_Attr
+ ("% attribute can only appear in postcondition of function",
+ P);
end if;
- end loop;
+ end Check_Placement_In_Check;
- Subp_Id := Scope (Post_Id);
+ ---------------------------------------
+ -- Check_Placement_In_Contract_Cases --
+ ---------------------------------------
- -- If the enclosing subprogram is always inlined, the enclosing
- -- postcondition will not be propagated to the expanded call.
+ procedure Check_Placement_In_Contract_Cases (Prag : Node_Id) is
+ Args : constant List_Id := Pragma_Argument_Associations (Prag);
+ Cases : constant Node_Id := Get_Pragma_Arg (First (Args));
+ CCase : Node_Id;
- if not In_Spec_Expression
- and then Has_Pragma_Inline_Always (Subp_Id)
- and then Warn_On_Redundant_Constructs
- then
- Error_Msg_N
- ("postconditions on inlined functions not enforced?r?", N);
- end if;
+ begin
+ if Present (Component_Associations (Cases)) then
+ CCase := First (Component_Associations (Cases));
+ while Present (CCase) loop
+
+ -- Guard against a malformed contract case. Detect whether
+ -- attribute 'Result appears within the consequence of the
+ -- current contract case.
+
+ if Nkind (CCase) = N_Component_Association
+ and then Is_Within (N, Expression (CCase))
+ then
+ return;
+ end if;
- -- If we are in the scope of a function and in Spec_Expression mode,
- -- this is likely the prescan of the postcondition (or contract case,
- -- or test case) pragma, and we just set the proper type. If there is
- -- an error it will be caught when the real Analyze call is done.
+ Next (CCase);
+ end loop;
+ end if;
- if Ekind (Post_Id) = E_Function and then In_Spec_Expression then
+ -- Otherwise pragma Contract_Cases is either malformed in some
+ -- way or attribute 'Result does not appear within a consequence
+ -- expression.
- -- Check OK prefix
+ Error_Attr ("% attribute misplaced inside contract cases", P);
+ end Check_Placement_In_Contract_Cases;
- if Chars (Post_Id) /= Chars (P) then
- Error_Msg_Name_1 := Name_Result;
- Error_Msg_NE
- ("incorrect prefix for % attribute, expected &", P, Post_Id);
- Error_Attr;
+ ----------------------------------
+ -- Check_Placement_In_Test_Case --
+ ----------------------------------
+
+ procedure Check_Placement_In_Test_Case (Prag : Node_Id) is
+ begin
+ -- Detect whether attribute 'Result appears within the "Ensures"
+ -- expression of pragma Test_Case.
+
+ if not Is_Within (N, Test_Case_Arg (Prag, Name_Ensures)) then
+ Error_Attr ("% attribute misplaced inside test case", P);
end if;
+ end Check_Placement_In_Test_Case;
- -- Check in postcondition, Test_Case or Contract_Cases of function
+ ---------------
+ -- Is_Within --
+ ---------------
- Prag := N;
- while Present (Prag)
- and then not Nkind_In (Prag, N_Pragma,
- N_Function_Specification,
- N_Aspect_Specification,
- N_Subprogram_Body)
- loop
- Prag := Parent (Prag);
- end loop;
+ function Is_Within
+ (Nod : Node_Id;
+ Encl_Nod : Node_Id) return Boolean
+ is
+ Par : Node_Id;
- -- In ASIS mode, the aspect itself is analyzed, in addition to the
- -- corresponding pragma. Do not issue errors when analyzing the
- -- aspect.
+ begin
+ Par := Nod;
+ while Present (Par) loop
+ if Par = Encl_Nod then
+ return True;
- if Nkind (Prag) = N_Aspect_Specification then
- null;
+ -- Prevent the search from going too far
- -- Must have a pragma
+ elsif Is_Body_Or_Package_Declaration (Par) then
+ exit;
+ end if;
- elsif Nkind (Prag) /= N_Pragma then
- Error_Attr
- ("% attribute can only appear in postcondition of function",
- P);
+ Par := Parent (Par);
+ end loop;
- -- Processing depends on which pragma we have
+ return False;
+ end Is_Within;
- else
- case Get_Pragma_Id (Prag) is
- when Pragma_Test_Case =>
- declare
- Arg_Ens : constant Node_Id :=
- Get_Ensures_From_CTC_Pragma (Prag);
- Arg : Node_Id;
+ -- Local variables
- begin
- Arg := N;
- while Arg /= Prag and then Arg /= Arg_Ens loop
- Arg := Parent (Arg);
- end loop;
+ In_Post : Boolean := False;
+ Prag : Node_Id;
+ Prag_Id : Pragma_Id;
+ Pref_Id : Entity_Id;
+ Spec_Id : Entity_Id;
+ Subp_Decl : Node_Id;
+ Subp_Id : Entity_Id;
+ Subp_Spec : Node_Id;
- if Arg /= Arg_Ens then
- Error_Attr
- ("% attribute misplaced inside test case", P);
- end if;
- end;
+ -- Start of processing for Result
- when Pragma_Contract_Cases =>
- declare
- Aggr : constant Node_Id :=
- Expression (First
- (Pragma_Argument_Associations (Prag)));
- Arg : Node_Id;
+ begin
+ -- The attribute reference is a primary. If any expressions follow,
+ -- then the attribute reference is an indexable object. Transform the
+ -- attribute into an indexed component and analyze it.
- begin
- Arg := N;
- while Arg /= Prag
- and then Parent (Parent (Arg)) /= Aggr
- loop
- Arg := Parent (Arg);
- end loop;
+ if Present (E1) then
+ Rewrite (N,
+ Make_Indexed_Component (Loc,
+ Prefix =>
+ Make_Attribute_Reference (Loc,
+ Prefix => Relocate_Node (P),
+ Attribute_Name => Name_Result),
+ Expressions => Expressions (N)));
+ Analyze (N);
+ return;
+ end if;
- -- At this point, Parent (Arg) should be a component
- -- association. Attribute Result is only allowed in
- -- the expression part of this association.
+ -- Traverse the parent chain to find the aspect or pragma where
+ -- attribute 'Result resides.
- if Nkind (Parent (Arg)) /= N_Component_Association
- or else Arg /= Expression (Parent (Arg))
- then
- Error_Attr
- ("% attribute misplaced inside contract cases",
- P);
- end if;
- end;
+ Prag := N;
+ while Present (Prag) loop
+ if Nkind_In (Prag, N_Aspect_Specification, N_Pragma) then
+ exit;
- when Pragma_Postcondition | Pragma_Refined_Post =>
- null;
+ -- Prevent the search from going too far
- when others =>
- Error_Attr
- ("% attribute can only appear in postcondition "
- & "of function", P);
- end case;
+ elsif Is_Body_Or_Package_Declaration (Prag) then
+ exit;
end if;
- -- The attribute reference is a primary. If expressions follow,
- -- the attribute reference is really an indexable object, so
- -- rewrite and analyze as an indexed component.
+ Prag := Parent (Prag);
+ end loop;
- if Present (E1) then
- Rewrite (N,
- Make_Indexed_Component (Loc,
- Prefix =>
- Make_Attribute_Reference (Loc,
- Prefix => Relocate_Node (Prefix (N)),
- Attribute_Name => Name_Result),
- Expressions => Expressions (N)));
- Analyze (N);
+ -- Do not emit an error when preanalyzing an aspect for ASIS. If the
+ -- placement of attribute 'Result is illegal, the error is reported
+ -- when analyzing the corresponding pragma.
+
+ if ASIS_Mode and then Nkind (Prag) = N_Aspect_Specification then
+ null;
+
+ -- Attribute 'Result is allowed to appear only in postcondition-like
+ -- pragmas.
+
+ elsif Nkind (Prag) = N_Pragma then
+ Prag_Id := Get_Pragma_Id (Prag);
+
+ if Prag_Id = Pragma_Check then
+ Check_Placement_In_Check (Prag);
+
+ elsif Prag_Id = Pragma_Contract_Cases then
+ Check_Placement_In_Contract_Cases (Prag);
+
+ elsif Prag_Id = Pragma_Postcondition
+ or else Prag_Id = Pragma_Refined_Post
+ then
+ null;
+
+ elsif Prag_Id = Pragma_Test_Case then
+ Check_Placement_In_Test_Case (Prag);
+
+ else
+ Error_Attr
+ ("% attribute can only appear in postcondition of function",
+ P);
return;
end if;
- Set_Etype (N, Etype (Post_Id));
+ -- Otherwise the placement of the attribute is illegal
- -- If several functions with that name are visible, the intended
- -- one is the current scope.
+ else
+ Error_Attr
+ ("% attribute can only appear in postcondition of function", P);
+ return;
+ end if;
- if Is_Overloaded (P) then
- Set_Entity (P, Post_Id);
- Set_Is_Overloaded (P, False);
- end if;
+ -- Attribute 'Result appears within a postcondition-like pragma. Find
+ -- the related subprogram subject to the pragma.
- -- 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.
+ if Nkind (Prag) = N_Aspect_Specification then
+ Subp_Decl := Parent (Prag);
+ else
+ Subp_Decl := Find_Related_Subprogram_Or_Body (Prag);
+ end if;
- elsif not Expander_Active and then In_Refined_Post then
+ -- The pragma where attribute 'Result appears is associated with a
+ -- subprogram declaration or a body.
- -- Routine _Postconditions has not been generated yet, the nearest
- -- enclosing subprogram is denoted by the current scope.
+ if Nkind_In (Subp_Decl, N_Abstract_Subprogram_Declaration,
+ N_Entry_Declaration,
+ N_Generic_Subprogram_Declaration,
+ N_Subprogram_Body,
+ N_Subprogram_Body_Stub,
+ N_Subprogram_Declaration)
+ then
+ Subp_Id := Defining_Entity (Subp_Decl);
- if Ekind (Post_Id) /= E_Procedure
- or else Chars (Post_Id) /= Name_uPostconditions
- then
- Subp_Id := Current_Scope;
+ -- Attribute 'Result is part of the _Postconditions procedure of
+ -- the related subprogram. Retrieve the related subprogram.
+
+ if Chars (Subp_Id) = Name_uPostconditions then
+ In_Post := True;
+ Subp_Decl := Parent (Subp_Decl);
+ Subp_Id := Scope (Subp_Id);
end if;
- -- The prefix denotes the nearest enclosing function
+ -- Retrieve the entity of the spec (if any)
- if Is_Entity_Name (P)
- and then Ekind (Entity (P)) = E_Function
- and then Entity (P) = Subp_Id
+ if Nkind (Subp_Decl) = N_Subprogram_Body
+ and then Present (Corresponding_Spec (Subp_Decl))
then
- null;
+ Spec_Id := Corresponding_Spec (Subp_Decl);
- -- Otherwise the use of 'Result is illegal
+ elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub
+ and then Present (Corresponding_Spec_Of_Stub (Subp_Decl))
+ then
+ Spec_Id := Corresponding_Spec_Of_Stub (Subp_Decl);
else
- Error_Msg_Name_2 := Chars (Subp_Id);
- Error_Attr ("incorrect prefix for % attribute, expected %", P);
+ Spec_Id := Subp_Id;
end if;
- Set_Etype (N, Etype (Subp_Id));
+ -- When the subprogram is always inlined, the postcondition will
+ -- not be propagated to the expanded body.
- -- 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
- -- current one.
+ if Warn_On_Redundant_Constructs
+ and then Has_Pragma_Inline_Always (Spec_Id)
+ then
+ Error_Msg_N
+ ("postconditions on inlined functions not enforced?r?", P);
+ end if;
- else
- while Present (Post_Id)
- and then Post_Id /= Standard_Standard
- loop
- if Chars (Post_Id) = Name_uPostconditions then
- exit;
- else
- Post_Id := Scope (Post_Id);
+ -- Ensure that the prefix of attribute 'Result denotes the related
+ -- subprogram.
+
+ if Is_Entity_Name (P) then
+ Pref_Id := Entity (P);
+
+ -- When a subprogram with contract assertions is imported, it
+ -- is encapsulated in a wrapper. In this case the scope of the
+ -- wrapper denotes the original imported subprogram.
+
+ if Is_Imported (Pref_Id) then
+ Pref_Id := Scope (Pref_Id);
end if;
- end loop;
- Subp_Id := Scope (Post_Id);
+ if Ekind_In (Pref_Id, E_Function, E_Generic_Function) then
- if Chars (Post_Id) = Name_uPostconditions
- and then Ekind (Subp_Id) = E_Function
- then
- -- Check OK prefix
+ -- The prefix of attribute 'Result denotes the entity of
+ -- some other unrelated function.
- if Nkind_In (P, N_Identifier, N_Operator_Symbol)
- and then Chars (P) = Chars (Subp_Id)
- then
- null;
+ if Pref_Id /= Spec_Id then
+ Subp_Spec := Parent (Spec_Id);
- -- Within an instance, the prefix designates the local renaming
- -- of the original generic.
+ -- Attribute 'Result appears in a postcondition of a
+ -- generic function that acts as a compilation unit:
- elsif Is_Entity_Name (P)
- and then Ekind (Entity (P)) = E_Function
- and then Present (Alias (Entity (P)))
- and then Chars (Alias (Entity (P))) = Chars (Subp_Id)
- then
- null;
+ -- generic
+ -- function Gen_Func return ...
+ -- with Post => Gen_Func'Result ...;
+
+ -- When the function is instantiated, the Chars field of
+ -- attribute 'Result's prefix still denotes the generic
+ -- function. Note that any preemptive transformation is
+ -- impossible without a proper analysis. The structure of
+ -- the anonymous wrapper package is as follows:
+
+ -- package Anon_Gen_Pack is
+ -- <subtypes and renamings>
+ -- function Subp_Decl return ...;
+ -- pragma Postcondition (Gen_Func'Result ...);
+ -- function Gen_Func ... renames Subp_Decl;
+ -- end Anon_Gen_Pack;
+
+ -- Recognize this case and do not flag it as illegal
+
+ if Nkind (Subp_Spec) = N_Function_Specification
+ and then Present (Generic_Parent (Subp_Spec))
+ then
+ if Generic_Parent (Subp_Spec) = Pref_Id then
+ null;
+
+ elsif Ekind (Pref_Id) = E_Function
+ and then Present (Alias (Pref_Id))
+ and then Alias (Pref_Id) = Spec_Id
+ then
+ null;
+
+ else
+ Error_Msg_Name_2 := Chars (Spec_Id);
+ Error_Attr
+ ("incorrect prefix for % attribute, expected %",
+ P);
+ end if;
+
+ -- Otherwise the context is not a function instantiation
+ -- and the prefix is illegal
+
+ else
+ Error_Msg_Name_2 := Chars (Spec_Id);
+ Error_Attr
+ ("incorrect prefix for % attribute, expected %", P);
+ end if;
+ end if;
+
+ -- Otherwise the attribute's prefix denotes some other form of
+ -- a non-function subprogram.
else
- Error_Msg_Name_2 := Chars (Subp_Id);
Error_Attr
- ("incorrect prefix for % attribute, expected %", P);
+ ("% attribute can only appear in postcondition of "
+ & "function", P);
end if;
- Rewrite (N, Make_Identifier (Sloc (N), Name_uResult));
+ -- Otherwise the prefix is illegal
+
+ else
+ Error_Msg_Name_2 := Chars (Spec_Id);
+ Error_Attr ("incorrect prefix for % attribute, expected %", P);
+ end if;
+
+ -- Attribute 'Result is part of the _Postconditions procedure of
+ -- the related subprogram. Rewrite the attribute as a reference to
+ -- the _Result formal parameter of _Postconditions.
+
+ if In_Post then
+ Rewrite (N, Make_Identifier (Loc, Name_uResult));
Analyze_And_Resolve (N, Etype (Subp_Id));
+ -- Otherwise decorate the attribute
+
else
- Error_Attr
- ("% attribute can only appear in postcondition of function",
- P);
+ Set_Etype (N, Etype (Subp_Id));
end if;
end if;
end Result;
------------------------------
procedure Analyze_Compilation_Unit (N : Node_Id) is
- Unit_Node : constant Node_Id := Unit (N);
- Lib_Unit : Node_Id := Library_Unit (N);
- Spec_Id : Entity_Id;
- Main_Cunit : constant Node_Id := Cunit (Main_Unit);
- Par_Spec_Name : Unit_Name_Type;
- Unum : Unit_Number_Type;
-
procedure Check_Redundant_Withs
(Context_Items : List_Id;
Spec_Context_Items : List_Id := No_List);
end loop;
end Check_Redundant_Withs;
+ -- Local variables
+
+ Main_Cunit : constant Node_Id := Cunit (Main_Unit);
+ Unit_Node : constant Node_Id := Unit (N);
+ Lib_Unit : Node_Id := Library_Unit (N);
+ Par_Spec_Name : Unit_Name_Type;
+ Spec_Id : Entity_Id;
+ Unum : Unit_Number_Type;
+
-- Start of processing for Analyze_Compilation_Unit
begin
end;
end if;
+ -- Analyze the contract of a [generic] subprogram that acts as a
+ -- compilation unit after all compilation pragmas have been analyzed.
+
+ if Nkind_In (Unit_Node, N_Generic_Subprogram_Declaration,
+ N_Subprogram_Declaration)
+ then
+ Analyze_Subprogram_Contract (Defining_Entity (Unit_Node));
+ end if;
+
-- Generate distribution stubs if requested and no error
if N = Main_Cunit
end if;
end Analyze_Protected_Body_Stub;
- -------------------------------------------
- -- Analyze_Subprogram_Body_Stub_Contract --
- -------------------------------------------
-
- procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id) is
- Stub_Decl : constant Node_Id := Parent (Parent (Stub_Id));
- Spec_Id : constant Entity_Id := Corresponding_Spec_Of_Stub (Stub_Decl);
-
- begin
- -- A subprogram body stub may act as its own spec or as the completion
- -- of a previous declaration. Depending on the context, the contract of
- -- the stub may contain two sets of pragmas.
-
- -- The stub is a completion, the applicable pragmas are:
- -- Contract_Cases
- -- Depends
- -- Global
- -- Postcondition
- -- Precondition
- -- Test_Case
-
- if Present (Spec_Id) then
- Analyze_Subprogram_Body_Contract (Stub_Id);
-
- -- The stub acts as its own spec, the applicable pragmas are:
- -- Refined_Depends
- -- Refined_Global
-
- else
- Analyze_Subprogram_Contract (Stub_Id);
- end if;
- end Analyze_Subprogram_Body_Stub_Contract;
-
----------------------------------
-- Analyze_Subprogram_Body_Stub --
----------------------------------
Restore_Opt_Config_Switches (Opts);
end Analyze_Subprogram_Body_Stub;
+ -------------------------------------------
+ -- Analyze_Subprogram_Body_Stub_Contract --
+ -------------------------------------------
+
+ procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id) is
+ Stub_Decl : constant Node_Id := Parent (Parent (Stub_Id));
+ Spec_Id : constant Entity_Id := Corresponding_Spec_Of_Stub (Stub_Decl);
+
+ begin
+ -- A subprogram body stub may act as its own spec or as the completion
+ -- of a previous declaration. Depending on the context, the contract of
+ -- the stub may contain two sets of pragmas.
+
+ -- The stub is a completion, the applicable pragmas are:
+ -- Refined_Depends
+ -- Refined_Global
+
+ if Present (Spec_Id) then
+ Analyze_Subprogram_Body_Contract (Stub_Id);
+
+ -- The stub acts as its own spec, the applicable pragmas are:
+ -- Contract_Cases
+ -- Depends
+ -- Global
+ -- Postcondition
+ -- Precondition
+ -- Test_Case
+
+ else
+ Analyze_Subprogram_Contract (Stub_Id);
+ end if;
+ end Analyze_Subprogram_Body_Stub_Contract;
+
---------------------
-- Analyze_Subunit --
---------------------
when None =>
null;
- -- If with'ed unit had a detected fatal error, propagate it
+ -- If with'ed unit had a detected fatal error, propagate it
when Error_Detected =>
Set_Fatal_Error (Current_Sem_Unit, Error_Detected);
- -- If with'ed unit had an ignored error, then propagate it
- -- but do not overide an existring setting.
+ -- If with'ed unit had an ignored error, then propagate it but do not
+ -- overide an existring setting.
when Error_Ignored =>
if Fatal_Error (Current_Sem_Unit) = None then
with Sem_Elab; use Sem_Elab;
with Sem_Elim; use Sem_Elim;
with Sem_Eval; use Sem_Eval;
-with Sem_Prag; use Sem_Prag;
with Sem_Res; use Sem_Res;
with Sem_Type; use Sem_Type;
with Sem_Util; use Sem_Util;
Start_Generic;
Enter_Name (Id);
- Set_Ekind (Id, E_Generic_Package);
- Set_Etype (Id, Standard_Void_Type);
- Set_Contract (Id, Make_Contract (Sloc (Id)));
+ Set_Ekind (Id, E_Generic_Package);
+ Set_Etype (Id, Standard_Void_Type);
-- A generic package declared within a Ghost region is rendered Ghost
-- (SPARK RM 6.9(2)).
--------------------------------------------
procedure Analyze_Generic_Subprogram_Declaration (N : Node_Id) is
- Spec : Node_Id;
- Id : Entity_Id;
Formals : List_Id;
+ Id : Entity_Id;
New_N : Node_Id;
Result_Type : Entity_Id;
Save_Parent : Node_Id;
+ Spec : Node_Id;
Typ : Entity_Id;
begin
Spec := Specification (N);
Id := Defining_Entity (Spec);
Generate_Definition (Id);
- Set_Contract (Id, Make_Contract (Sloc (Id)));
if Nkind (Id) = N_Defining_Operator_Symbol then
Error_Msg_N
Set_Categorization_From_Pragmas (N);
Validate_Categorization_Dependency (N, Id);
- Save_Global_References (Original_Node (N));
-
- -- For ASIS purposes, convert any postcondition, precondition pragmas
- -- into aspects, if N is not a compilation unit by itself, in order to
- -- enable the analysis of expressions inside the corresponding PPC
- -- pragmas.
+ -- Capture all global references that occur within the profile of the
+ -- generic subprogram. Aspects are not part of this processing because
+ -- they must be delayed. If processed now, Save_Global_References will
+ -- destroy the Associated_Node links and prevent the capture of global
+ -- references when the contract of the generic subprogram is analyzed.
- if ASIS_Mode and then Is_List_Member (N) then
- Make_Aspect_For_PPC_In_Gen_Sub_Decl (N);
- end if;
+ Save_Global_References (Original_Node (N));
End_Generic;
End_Scope;
-- aspects that appear in the generic. This renaming declaration is
-- inserted after the instance declaration which it renames.
+ procedure Instantiate_Contract (Subp_Id : Entity_Id);
+ -- Instantiate all source pragmas found in the contract of subprogram
+ -- Subp_Id. The instantiated pragmas are added to list Renaming_List.
+
------------------------------------
-- Analyze_Instance_And_Renamings --
------------------------------------
Suffix_Index => Source_Offset (Sloc (Def_Ent))));
end if;
- Pack_Decl := Make_Package_Declaration (Loc,
- Specification => Make_Package_Specification (Loc,
- Defining_Unit_Name => Pack_Id,
- Visible_Declarations => Renaming_List,
- End_Label => Empty));
+ Pack_Decl :=
+ Make_Package_Declaration (Loc,
+ Specification => Make_Package_Specification (Loc,
+ Defining_Unit_Name => Pack_Id,
+ Visible_Declarations => Renaming_List,
+ End_Label => Empty));
Set_Instance_Spec (N, Pack_Decl);
Set_Is_Generic_Instance (Pack_Id);
end if;
end Build_Subprogram_Renaming;
+ --------------------------
+ -- Instantiate_Contract --
+ --------------------------
+
+ procedure Instantiate_Contract (Subp_Id : Entity_Id) is
+ procedure Instantiate_Pragmas (First_Prag : Node_Id);
+ -- Instantiate all contract-related source pragmas found in the list
+ -- starting with pragma First_Prag. Each instantiated pragma is added
+ -- to list Renaming_List.
+
+ -------------------------
+ -- Instantiate_Pragmas --
+ -------------------------
+
+ procedure Instantiate_Pragmas (First_Prag : Node_Id) is
+ Inst_Prag : Node_Id;
+ Prag : Node_Id;
+
+ begin
+ Prag := First_Prag;
+ while Present (Prag) loop
+ if Comes_From_Source (Prag)
+ and then Nam_In (Pragma_Name (Prag), Name_Contract_Cases,
+ Name_Depends,
+ Name_Extensions_Visible,
+ Name_Global,
+ Name_Postcondition,
+ Name_Precondition,
+ Name_Test_Case)
+ then
+ Inst_Prag :=
+ Copy_Generic_Node
+ (Original_Node (Prag), Empty, Instantiating => True);
+
+ Set_Analyzed (Inst_Prag, False);
+ Append_To (Renaming_List, Inst_Prag);
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end Instantiate_Pragmas;
+
+ -- Local variables
+
+ Items : constant Node_Id := Contract (Subp_Id);
+
+ -- Start of processing for Instantiate_Contract
+
+ begin
+ if Present (Items) then
+ Instantiate_Pragmas (Pre_Post_Conditions (Items));
+ Instantiate_Pragmas (Contract_Test_Cases (Items));
+ Instantiate_Pragmas (Classifications (Items));
+ end if;
+ end Instantiate_Contract;
+
-- Local variables
Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
end if;
Append (Act_Decl, Renaming_List);
+ Instantiate_Contract (Gen_Unit);
Build_Subprogram_Renaming;
+
Analyze_Instance_And_Renamings;
-- If the generic is marked Import (Intrinsic), then so is the
end if;
Generate_Definition (Act_Decl_Id);
- -- Set_Contract (Anon_Id, Make_Contract (Sloc (Anon_Id)));
- -- ??? needed?
- Set_Contract (Act_Decl_Id, Make_Contract (Sloc (Act_Decl_Id)));
-- Inherit all inlining-related flags which apply to the generic in
-- the subprogram and its declaration.
(Body_Info : Pending_Body_Info;
Body_Optional : Boolean := False)
is
- Act_Decl : constant Node_Id := Body_Info.Act_Decl;
- Inst_Node : constant Node_Id := Body_Info.Inst_Node;
- Loc : constant Source_Ptr := Sloc (Inst_Node);
- Gen_Id : constant Node_Id := Name (Inst_Node);
- Gen_Unit : constant Entity_Id := Get_Generic_Entity (Inst_Node);
- Gen_Decl : constant Node_Id := Unit_Declaration_Node (Gen_Unit);
- Anon_Id : constant Entity_Id :=
- Defining_Unit_Name (Specification (Act_Decl));
- Pack_Id : constant Entity_Id :=
- Defining_Unit_Name (Parent (Act_Decl));
- Gen_Body : Node_Id;
- Gen_Body_Id : Node_Id;
- Act_Body : Node_Id;
- Pack_Body : Node_Id;
- Ret_Expr : Node_Id;
-
- Parent_Installed : Boolean := False;
+ Act_Decl : constant Node_Id := Body_Info.Act_Decl;
+ Inst_Node : constant Node_Id := Body_Info.Inst_Node;
+ Loc : constant Source_Ptr := Sloc (Inst_Node);
+ Gen_Id : constant Node_Id := Name (Inst_Node);
+ Gen_Unit : constant Entity_Id := Get_Generic_Entity (Inst_Node);
+ Gen_Decl : constant Node_Id := Unit_Declaration_Node (Gen_Unit);
+ Anon_Id : constant Entity_Id :=
+ Defining_Unit_Name (Specification (Act_Decl));
+ Pack_Id : constant Entity_Id :=
+ Defining_Unit_Name (Parent (Act_Decl));
Saved_Style_Check : constant Boolean := Style_Check;
Saved_Warnings : constant Warning_Record := Save_Warnings;
- Par_Ent : Entity_Id := Empty;
- Par_Vis : Boolean := False;
+ Act_Body : Node_Id;
+ Gen_Body : Node_Id;
+ Gen_Body_Id : Node_Id;
+ Pack_Body : Node_Id;
+ Par_Ent : Entity_Id := Empty;
+ Par_Vis : Boolean := False;
+ Ret_Expr : Node_Id;
+
+ Parent_Installed : Boolean := False;
begin
Gen_Body_Id := Corresponding_Body (Gen_Decl);
end;
end if;
- -- If a node has aspects, references within their expressions must
- -- be saved separately, given they are not directly in the tree.
-
- if Has_Aspects (N) then
- declare
- Aspect : Node_Id;
-
- begin
- Aspect := First (Aspect_Specifications (N));
- while Present (Aspect) loop
- if Present (Expression (Aspect)) then
- Save_Global_References (Expression (Aspect));
- end if;
+ -- Save all global references found within the aspects of the related
+ -- node. This is not done for generic subprograms because the aspects
+ -- must be delayed and analyzed at the end of the declarative part.
+ -- Only then can global references be saved. This action is performed
+ -- by the analysis of the generic subprogram contract.
- Next (Aspect);
- end loop;
- end;
+ if Nkind (N) /= N_Generic_Subprogram_Declaration then
+ Save_Global_References_In_Aspects (N);
end if;
end Save_References;
Save_References (N);
end Save_Global_References;
+ ---------------------------------------
+ -- Save_Global_References_In_Aspects --
+ ---------------------------------------
+
+ procedure Save_Global_References_In_Aspects (N : Node_Id) is
+ Asp : Node_Id;
+ Expr : Node_Id;
+
+ begin
+ if Permits_Aspect_Specifications (N) and then Has_Aspects (N) then
+ Asp := First (Aspect_Specifications (N));
+ while Present (Asp) loop
+ Expr := Expression (Asp);
+
+ if Present (Expr) then
+ Save_Global_References (Expr);
+ end if;
+
+ Next (Asp);
+ end loop;
+ end if;
+ end Save_Global_References_In_Aspects;
+
--------------------------------------
-- Set_Copied_Sloc_For_Inlined_Body --
--------------------------------------
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- restored in stack-like fashion. Front-end inlining also uses these
-- structures for the management of private/full views.
+ procedure Save_Global_References_In_Aspects (N : Node_Id);
+ -- Save all global references in the aspect specifications of node N
+
procedure Set_Copied_Sloc_For_Inlined_Body (N : Node_Id; E : Entity_Id);
-- This procedure is used when a subprogram body is inlined. This process
-- shares the same circuitry as the creation of an instantiated copy of
Decl : Node_Id;
begin
- -- When the context is a library unit, the pragma is added to the
- -- Pragmas_After list.
-
- if Nkind (Parent (N)) = N_Compilation_Unit then
- Aux := Aux_Decls_Node (Parent (N));
-
- if No (Pragmas_After (Aux)) then
- Set_Pragmas_After (Aux, New_List);
- end if;
-
- Prepend (Prag, Pragmas_After (Aux));
-
- -- Pragmas associated with subprogram bodies are inserted in the
- -- declarative part.
-
- elsif Nkind (N) = N_Subprogram_Body then
+ if Nkind (N) = N_Subprogram_Body then
if Present (Declarations (N)) then
-- Skip other internally generated pragmas from aspects to find
Set_Declarations (N, New_List (Prag));
end if;
+ -- When the context is a library unit, the pragma is added to the
+ -- Pragmas_After list.
+
+ elsif Nkind (Parent (N)) = N_Compilation_Unit then
+ Aux := Aux_Decls_Node (Parent (N));
+
+ if No (Pragmas_After (Aux)) then
+ Set_Pragmas_After (Aux, New_List);
+ end if;
+
+ Prepend (Prag, Pragmas_After (Aux));
+
-- Default
else
if not Opt.Exception_Locations_Suppressed then
Append_To (Pragma_Argument_Associations (Aitem),
Make_Pragma_Argument_Association (Eloc,
- Chars => Name_Message,
+ Chars => Name_Message,
Expression =>
Make_String_Literal (Eloc,
Strval => "failed "
Comp_Expr := First (Expressions (Expr));
while Present (Comp_Expr) loop
New_Expr := Relocate_Node (Comp_Expr);
- Set_Original_Node (New_Expr, Comp_Expr);
Append_To (Args,
Make_Pragma_Argument_Association (Sloc (Comp_Expr),
Expression => New_Expr));
goto Continue;
end if;
- New_Expr := Relocate_Node (Expression (Comp_Assn));
- Set_Original_Node (New_Expr, Expression (Comp_Assn));
Append_To (Args,
Make_Pragma_Argument_Association (Sloc (Comp_Assn),
- Chars => Chars (First (Choices (Comp_Assn))),
- Expression => New_Expr));
+ Chars => Chars (First (Choices (Comp_Assn))),
+ Expression =>
+ Relocate_Node (Expression (Comp_Assn))));
Next (Comp_Assn);
end loop;
Analyze_Object_Contract (Defining_Entity (Decl));
elsif Nkind_In (Decl, N_Abstract_Subprogram_Declaration,
+ N_Generic_Subprogram_Declaration,
N_Subprogram_Declaration)
then
Analyze_Subprogram_Contract (Defining_Entity (Decl));
if Present (E) then
Set_Has_Initial_Value (Id);
end if;
-
- Set_Contract (Id, Make_Contract (Sloc (Id)));
end if;
-- Initialize alignment and size and capture alignment setting
begin
New_Subp := New_Entity (Nkind (Parent_Subp), Sloc (Derived_Type));
Set_Ekind (New_Subp, Ekind (Parent_Subp));
- Set_Contract (New_Subp, Make_Contract (Sloc (New_Subp)));
-- Check whether the inherited subprogram is a private operation that
-- should be inherited but not yet made visible. Such subprograms can
Set_Has_Private_Declaration (Prev);
Set_Has_Private_Declaration (Id);
- -- AI12-0133: Indicate whether we have a partial view with
+ -- AI12-0133: indicate whether we have a partial view with
-- unknown discriminants, in which case initialization of objects
-- of the type do not receive an invariant check.
and then Limited_Present (Type_Definition (Orig_Decl))
then
Error_Msg_N
- ("full view of non-limited extension cannot be limited", N);
+ ("full view of non-limited extension cannot be limited", N);
-- Conversely, if the partial view carries the limited keyword,
-- the full view must as well, even if it may be redundant.
and then not Limited_Present (Type_Definition (Orig_Decl))
then
Error_Msg_N
- ("full view of limited extension must be explicitly limited",
- N);
+ ("full view of limited extension must be explicitly limited",
+ N);
end if;
end if;
end;
-- Local Subprograms --
-----------------------
+ procedure Analyze_Function_Return (N : Node_Id);
+ -- Subsidiary to Analyze_Return_Statement. Called when the return statement
+ -- applies to a [generic] function.
+
+ procedure Analyze_Generic_Subprogram_Body (N : Node_Id; Gen_Id : Entity_Id);
+ -- Analyze a generic subprogram body. N is the body to be analyzed, and
+ -- Gen_Id is the defining entity Id for the corresponding spec.
+
procedure Analyze_Null_Procedure
(N : Node_Id;
Is_Completion : out Boolean);
procedure Analyze_Return_Statement (N : Node_Id);
-- Common processing for simple and extended return statements
- procedure Analyze_Function_Return (N : Node_Id);
- -- Subsidiary to Analyze_Return_Statement. Called when the return statement
- -- applies to a [generic] function.
-
procedure Analyze_Return_Type (N : Node_Id);
-- Subsidiary to Process_Formals: analyze subtype mark in function
-- specification in a context where the formals are visible and hide
-- Does all the real work of Analyze_Subprogram_Body. This is split out so
-- that we can use RETURN but not skip the debug output at the end.
- procedure Analyze_Generic_Subprogram_Body (N : Node_Id; Gen_Id : Entity_Id);
- -- Analyze a generic subprogram body. N is the body to be analyzed, and
- -- Gen_Id is the defining entity Id for the corresponding spec.
-
function Can_Override_Operator (Subp : Entity_Id) return Boolean;
-- Returns true if Subp can override a predefined operator.
Check_SPARK_05_Restriction ("abstract subprogram is not allowed", N);
Generate_Definition (Designator);
- Set_Contract (Designator, Make_Contract (Sloc (Designator)));
+
Set_Is_Abstract_Subprogram (Designator);
New_Overloaded_Entity (Designator);
Check_Delayed_Subprogram (Designator);
-- Visible generic entity is callable within its own body
Set_Ekind (Gen_Id, Ekind (Body_Id));
- Set_Contract (Body_Id, Make_Contract (Sloc (Body_Id)));
Set_Ekind (Body_Id, E_Subprogram_Body);
Set_Convention (Body_Id, Convention (Gen_Id));
Set_Is_Obsolescent (Body_Id, Is_Obsolescent (Gen_Id));
Set_Actual_Subtypes (N, Current_Scope);
- -- Deal with [refined] preconditions, postconditions, Contract_Cases,
- -- invariants and predicates associated with the body and its spec.
- -- Note that this is not pure expansion as Expand_Subprogram_Contract
- -- prepares the contract assertions for generic subprograms or for
- -- ASIS. Do not generate contract checks in SPARK mode.
-
- if not GNATprove_Mode then
- Expand_Subprogram_Contract (N, Gen_Id, Body_Id);
- end if;
-
- -- If the generic unit carries pre- or post-conditions, copy them
- -- to the original generic tree, so that they are properly added
- -- to any instantiation.
-
- declare
- Orig : constant Node_Id := Original_Node (N);
- Cond : Node_Id;
-
- begin
- Cond := First (Declarations (N));
- while Present (Cond) loop
- if Nkind (Cond) = N_Pragma
- and then Pragma_Name (Cond) = Name_Check
- then
- Prepend (New_Copy_Tree (Cond), Declarations (Orig));
-
- elsif Nkind (Cond) = N_Pragma
- and then Pragma_Name (Cond) = Name_Postcondition
- then
- Set_Ekind (Defining_Entity (Orig), Ekind (Gen_Id));
- Prepend (New_Copy_Tree (Cond), Declarations (Orig));
- else
- exit;
- end if;
-
- Next (Cond);
- end loop;
- end;
-
Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
Set_SPARK_Pragma_Inherited (Body_Id, True);
if Present (Prev) and then Is_Generic_Subprogram (Prev) then
Insert_Before (N, Null_Body);
Set_Ekind (Defining_Entity (N), Ekind (Prev));
- Set_Contract (Defining_Entity (N), Make_Contract (Loc));
Rewrite (N, Make_Null_Statement (Loc));
Analyze_Generic_Subprogram_Body (Null_Body, Prev);
--------------------------------------
procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id) is
- Body_Decl : constant Node_Id := Parent (Parent (Body_Id));
- Mode : SPARK_Mode_Type;
- Prag : Node_Id;
- Ref_Depends : Node_Id := Empty;
- Ref_Global : Node_Id := Empty;
- Spec_Id : Entity_Id;
+ Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
- begin
- -- Due to the timing of contract analysis, delayed pragmas may be
- -- subject to the wrong SPARK_Mode, usually that of the enclosing
- -- context. To remedy this, restore the original SPARK_Mode of the
- -- related subprogram body.
+ procedure Analyze_Completion_Contract (Spec_Id : Entity_Id);
+ -- Analyze all delayed pragmas chained on the contract of subprogram
+ -- body Body_Id as if they appeared at the end of a declarative region.
+ -- Spec_Id denotes the corresponding spec. The aspects in question are:
+ -- Refined_Depends
+ -- Refined_Global
+ -- Note that pragma Refined_Post is analyzed immediately
- Save_SPARK_Mode_And_Set (Body_Id, Mode);
+ ---------------------------------
+ -- Analyze_Completion_Contract --
+ ---------------------------------
- -- When a subprogram body declaration is illegal, its defining entity is
- -- left unanalyzed. There is nothing left to do in this case because the
- -- body lacks a contract, or even a proper Ekind.
+ procedure Analyze_Completion_Contract (Spec_Id : Entity_Id) is
+ Items : constant Node_Id := Contract (Body_Id);
+ Prag : Node_Id;
+ Prag_Nam : Name_Id;
+ Ref_Depends : Node_Id := Empty;
+ Ref_Global : Node_Id := Empty;
- if Ekind (Body_Id) = E_Void then
- return;
- end if;
+ begin
+ -- All subprograms carry a contract, but for some it is not
+ -- significant and should not be processed.
- if Nkind (Body_Decl) = N_Subprogram_Body_Stub then
- Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl);
- else
- Spec_Id := Corresponding_Spec (Body_Decl);
- end if;
+ if not Has_Significant_Contract (Spec_Id) then
+ return;
+
+ elsif Present (Items) then
+
+ -- Locate and store pragmas Refined_Depends and Refined_Global
+ -- since their order of analysis matters.
+
+ Prag := Classifications (Items);
+ while Present (Prag) loop
+ Prag_Nam := Pragma_Name (Prag);
- -- Locate and store pragmas Refined_Depends and Refined_Global since
- -- their order of analysis matters.
+ if Prag_Nam = Name_Refined_Depends then
+ Ref_Depends := Prag;
- Prag := Classifications (Contract (Body_Id));
- while Present (Prag) loop
- if Pragma_Name (Prag) = Name_Refined_Depends then
- Ref_Depends := Prag;
- elsif Pragma_Name (Prag) = Name_Refined_Global then
- Ref_Global := Prag;
+ elsif Prag_Nam = Name_Refined_Global then
+ Ref_Global := Prag;
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
end if;
- Prag := Next_Pragma (Prag);
- end loop;
+ -- Analyze Refined_Global first as Refined_Depends may mention items
+ -- classified in the global refinement.
- -- Analyze Refined_Global first as Refined_Depends may mention items
- -- classified in the global refinement.
+ if Present (Ref_Global) then
+ Analyze_Refined_Global_In_Decl_Part (Ref_Global);
- if Present (Ref_Global) then
- Analyze_Refined_Global_In_Decl_Part (Ref_Global);
+ -- When the corresponding Global pragma references a state with
+ -- visible refinement, the body requires Refined_Global. Such a
+ -- refinement is not required when SPARK checks are suppressed.
- -- When the corresponding Global aspect/pragma references a state with
- -- visible refinement, the body requires Refined_Global. Refinement is
- -- not required when SPARK checks are suppressed.
+ else
+ Prag := Get_Pragma (Spec_Id, Pragma_Global);
- elsif Present (Spec_Id) then
- Prag := Get_Pragma (Spec_Id, Pragma_Global);
+ if SPARK_Mode /= Off
+ and then Present (Prag)
+ and then Contains_Refined_State (Prag)
+ then
+ Error_Msg_NE
+ ("body of subprogram& requires global refinement",
+ Body_Decl, Spec_Id);
+ end if;
+ end if;
- if SPARK_Mode /= Off
- and then Present (Prag)
- and then Contains_Refined_State (Prag)
- then
- Error_Msg_NE
- ("body of subprogram& requires global refinement",
- Body_Decl, Spec_Id);
+ -- Refined_Depends must be analyzed after Refined_Global in order to
+ -- see the modes of all global refinements.
+
+ if Present (Ref_Depends) then
+ Analyze_Refined_Depends_In_Decl_Part (Ref_Depends);
+
+ -- When the corresponding Depends pragma references a state with
+ -- visible refinement, the body requires Refined_Depends. Such a
+ -- refinement is not required when SPARK checks are suppressed.
+
+ else
+ Prag := Get_Pragma (Spec_Id, Pragma_Depends);
+
+ if SPARK_Mode /= Off
+ and then Present (Prag)
+ and then Contains_Refined_State (Prag)
+ then
+ Error_Msg_NE
+ ("body of subprogram& requires dependance refinement",
+ Body_Decl, Spec_Id);
+ end if;
end if;
+ end Analyze_Completion_Contract;
+
+ -- Local variables
+
+ Mode : SPARK_Mode_Type;
+ Spec_Id : Entity_Id;
+
+ -- Start of processing for Analyze_Subprogram_Body_Contract
+
+ begin
+ -- When a subprogram body declaration is illegal, its defining entity is
+ -- left unanalyzed. There is nothing left to do in this case because the
+ -- body lacks a contract, or even a proper Ekind.
+
+ if Ekind (Body_Id) = E_Void then
+ return;
end if;
- -- Refined_Depends must be analyzed after Refined_Global in order to see
- -- the modes of all global refinements.
+ -- Due to the timing of contract analysis, delayed pragmas may be
+ -- subject to the wrong SPARK_Mode, usually that of the enclosing
+ -- context. To remedy this, restore the original SPARK_Mode of the
+ -- related subprogram body.
- if Present (Ref_Depends) then
- Analyze_Refined_Depends_In_Decl_Part (Ref_Depends);
+ Save_SPARK_Mode_And_Set (Body_Id, Mode);
- -- When the corresponding Depends aspect/pragma references a state with
- -- visible refinement, the body requires Refined_Depends. Refinement is
- -- not required when SPARK checks are suppressed.
+ if Nkind (Body_Decl) = N_Subprogram_Body_Stub then
+ Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl);
+ else
+ Spec_Id := Corresponding_Spec (Body_Decl);
+ end if;
- elsif Present (Spec_Id) then
- Prag := Get_Pragma (Spec_Id, Pragma_Depends);
+ -- The subprogram body is a completion, analyze all delayed pragmas that
+ -- apply. Note that when the body is stand alone, the pragmas are always
+ -- analyzed on the spot.
- if SPARK_Mode /= Off
- and then Present (Prag)
- and then Contains_Refined_State (Prag)
- then
- Error_Msg_NE
- ("body of subprogram& requires dependance refinement",
- Body_Decl, Spec_Id);
- end if;
+ if Present (Spec_Id) then
+ Analyze_Completion_Contract (Spec_Id);
end if;
+ -- Ensure that the contract cases or postconditions mention 'Result or
+ -- define a post-state.
+
+ Check_Result_And_Post_State (Body_Id);
+
-- Restore the SPARK_Mode of the enclosing context after all delayed
-- pragmas have been analyzed.
end if;
end if;
- -- Mark presence of postcondition procedure in current scope and mark
- -- the procedure itself as needing debug info. The latter is important
- -- when analyzing decision coverage (for example, for MC/DC coverage).
-
- if Chars (Body_Id) = Name_uPostconditions then
- Set_Has_Postconditions (Current_Scope);
- Set_Debug_Info_Needed (Body_Id);
- end if;
-
-- Place subprogram on scope stack, and make formals visible. If there
-- is a spec, the visible entity remains that of the spec.
end if;
Set_Corresponding_Body (Unit_Declaration_Node (Spec_Id), Body_Id);
- Set_Contract (Body_Id, Make_Contract (Sloc (Body_Id)));
- Set_Scope (Body_Id, Scope (Spec_Id));
Set_Is_Obsolescent (Body_Id, Is_Obsolescent (Spec_Id));
+ Set_Scope (Body_Id, Scope (Spec_Id));
-- Case of subprogram body with no previous spec
if Nkind (N) /= N_Subprogram_Body_Stub then
Set_Acts_As_Spec (N);
Generate_Definition (Body_Id);
- Set_Contract (Body_Id, Make_Contract (Sloc (Body_Id)));
Generate_Reference
(Body_Id, Body_Id, 'b', Set_Ref => False, Force => True);
Install_Formals (Body_Id);
Analyze_Aspects_On_Body_Or_Stub;
end if;
- -- Deal with [refined] preconditions, postconditions, Contract_Cases,
- -- invariants and predicates associated with the body and its spec.
- -- Note that this is not pure expansion as Expand_Subprogram_Contract
- -- prepares the contract assertions for generic subprograms or for ASIS.
- -- Do not generate contract checks in SPARK mode.
-
- if not GNATprove_Mode then
- Expand_Subprogram_Contract (N, Spec_Id, Body_Id);
- end if;
-
- -- Analyze the declarations (this call will analyze the precondition
- -- Check pragmas we prepended to the list, as well as the declaration
- -- of the _Postconditions procedure).
-
Analyze_Declarations (Declarations (N));
-- Verify that the SPARK_Mode of the body agrees with that of its spec
end if;
end if;
+ -- When a subprogram body appears inside a package, its contract is
+ -- analyzed at the end of the package body declarations. This is due
+ -- to the delay with respect of the package contract upon which the
+ -- body contract may depend. When the subprogram body is stand alone
+ -- and acts as a compilation unit, this delay is not necessary.
+
+ if Nkind (Parent (N)) = N_Compilation_Unit then
+ Analyze_Subprogram_Body_Contract (Body_Id);
+ end if;
+
+ -- Deal with preconditions, [refined] postconditions, Contract_Cases,
+ -- invariants and predicates associated with body and its spec. Since
+ -- there is no routine Expand_Declarations which would otherwise deal
+ -- with the contract expansion, generate all necessary mechanisms to
+ -- verify the contract assertions now.
+
+ Expand_Subprogram_Contract (N);
+
-- If SPARK_Mode for body is not On, disable frontend inlining for this
-- subprogram in GNATprove mode, as its body should not be analyzed.
-- Analyze_Subprogram_Contract --
---------------------------------
- procedure Analyze_Subprogram_Contract (Subp : Entity_Id) is
- Items : constant Node_Id := Contract (Subp);
- Case_Prag : Node_Id := Empty;
- Depends : Node_Id := Empty;
- Global : Node_Id := Empty;
- Mode : SPARK_Mode_Type;
- Nam : Name_Id;
- Post_Prag : Node_Id := Empty;
- Prag : Node_Id;
- Seen_In_Case : Boolean := False;
- Seen_In_Post : Boolean := False;
+ procedure Analyze_Subprogram_Contract (Subp_Id : Entity_Id) is
+ procedure Save_Global_References_In_List (First_Prag : Node_Id);
+ -- Save all global references in contract-related source pragma found in
+ -- the list starting from pragma First_Prag.
+
+ ------------------------------------
+ -- Save_Global_References_In_List --
+ ------------------------------------
+
+ procedure Save_Global_References_In_List (First_Prag : Node_Id) is
+ Prag : Node_Id;
+
+ begin
+ Prag := First_Prag;
+ while Present (Prag) loop
+ if Comes_From_Source (Prag)
+ and then Nam_In (Pragma_Name (Prag), Name_Contract_Cases,
+ Name_Depends,
+ Name_Extensions_Visible,
+ Name_Global,
+ Name_Postcondition,
+ Name_Precondition,
+ Name_Test_Case)
+ then
+ Save_Global_References (Original_Node (Prag));
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end Save_Global_References_In_List;
+
+ -- Local variables
+
+ Items : constant Node_Id := Contract (Subp_Id);
+ Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
+ Depends : Node_Id := Empty;
+ Global : Node_Id := Empty;
+ Mode : SPARK_Mode_Type;
+ Prag : Node_Id;
+ Prag_Nam : Name_Id;
+ Restore_Scope : Boolean := False;
+
+ -- Start of processing for Analyze_Subprogram_Contract
begin
+ -- All subprograms carry a contract, but for some it is not significant
+ -- and should not be processed.
+
+ if not Has_Significant_Contract (Subp_Id) then
+ return;
+ end if;
+
-- Due to the timing of contract analysis, delayed pragmas may be
-- subject to the wrong SPARK_Mode, usually that of the enclosing
-- context. To remedy this, restore the original SPARK_Mode of the
-- related subprogram body.
- Save_SPARK_Mode_And_Set (Subp, Mode);
+ Save_SPARK_Mode_And_Set (Subp_Id, Mode);
+
+ -- Ensure that the formal parameters are visible when analyzing all
+ -- contract items.
+
+ if not In_Open_Scopes (Subp_Id) then
+ Restore_Scope := True;
+ Push_Scope (Subp_Id);
+
+ if Is_Generic_Subprogram (Subp_Id) then
+ Install_Generic_Formals (Subp_Id);
+ else
+ Install_Formals (Subp_Id);
+ end if;
+ end if;
if Present (Items) then
Prag := Pre_Post_Conditions (Items);
while Present (Prag) loop
- Analyze_Pre_Post_Condition_In_Decl_Part (Prag, Subp);
-
- -- Verify whether a postcondition mentions attribute 'Result and
- -- its expression introduces a post-state.
-
- if Warn_On_Suspicious_Contract
- and then Pragma_Name (Prag) = Name_Postcondition
- then
- Post_Prag := Prag;
- Check_Result_And_Post_State (Prag, Seen_In_Post);
- end if;
-
+ Analyze_Pre_Post_Condition_In_Decl_Part (Prag);
Prag := Next_Pragma (Prag);
end loop;
Prag := Contract_Test_Cases (Items);
while Present (Prag) loop
- Nam := Pragma_Name (Prag);
+ Prag_Nam := Pragma_Name (Prag);
- if Nam = Name_Contract_Cases then
+ if Prag_Nam = Name_Contract_Cases then
Analyze_Contract_Cases_In_Decl_Part (Prag);
-
- -- Verify whether contract-cases mention attribute 'Result and
- -- its expression introduces a post-state. Perform the check
- -- only when the pragma is legal.
-
- if Warn_On_Suspicious_Contract
- and then not Error_Posted (Prag)
- then
- Case_Prag := Prag;
- Check_Result_And_Post_State (Prag, Seen_In_Case);
- end if;
-
else
- pragma Assert (Nam = Name_Test_Case);
- Analyze_Test_Case_In_Decl_Part (Prag, Subp);
+ pragma Assert (Prag_Nam = Name_Test_Case);
+ Analyze_Test_Case_In_Decl_Part (Prag);
end if;
Prag := Next_Pragma (Prag);
Prag := Classifications (Items);
while Present (Prag) loop
- Nam := Pragma_Name (Prag);
+ Prag_Nam := Pragma_Name (Prag);
- if Nam = Name_Depends then
+ if Prag_Nam = Name_Depends then
Depends := Prag;
- elsif Nam = Name_Global then
+ elsif Prag_Nam = Name_Global then
Global := Prag;
-- Note that pragma Extensions_Visible has already been analyzed
if Present (Depends) then
Analyze_Depends_In_Decl_Part (Depends);
end if;
- end if;
- -- Emit an error when neither the postconditions nor the contract-cases
- -- mention attribute 'Result in the context of a function.
+ -- Ensure that the contract cases or postconditions mention 'Result
+ -- or define a post-state.
- if Warn_On_Suspicious_Contract
- and then Ekind_In (Subp, E_Function, E_Generic_Function)
- then
- if Present (Case_Prag)
- and then not Seen_In_Case
- and then Present (Post_Prag)
- and then not Seen_In_Post
- then
- Error_Msg_N
- ("neither function postcondition nor contract cases mention "
- & "result?T?", Post_Prag);
+ Check_Result_And_Post_State (Subp_Id);
+ end if;
- elsif Present (Case_Prag) and then not Seen_In_Case then
- Error_Msg_N
- ("contract cases do not mention result?T?", Case_Prag);
+ -- The aspects and contract-related source pragmas associated with a
+ -- generic subprogram are treated separately from the declaration as
+ -- they need to be analyzed when the subprogram contract is analyzed.
+ -- Once this is done, global references can be successfully saved.
- -- OK if we have at least one IN OUT parameter
+ if Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then
- elsif Present (Post_Prag) and then not Seen_In_Post then
- declare
- F : Entity_Id;
- begin
- F := First_Formal (Subp);
- while Present (F) loop
- if Ekind (F) = E_In_Out_Parameter then
- return;
- else
- Next_Formal (F);
- end if;
- end loop;
- end;
+ -- Save all global references found in the aspect specifications of
+ -- the parameter profile of the generic subprogram.
- -- If no in-out parameters and no mention of Result, the contract
- -- is certainly suspicious.
+ Save_Global_References_In_Aspects (Original_Node (Subp_Decl));
- Error_Msg_N
- ("function postcondition does not mention result?T?", Post_Prag);
+ -- Save all global references found in contract-related source
+ -- pragmas. These pragmas usually appear after the declaration of
+ -- the generic subprogram, either in the same declarative part or
+ -- in the Pragmas_After list when the generic subprogram is a
+ -- compilation unit.
+
+ if Present (Items) then
+ Save_Global_References_In_List (Pre_Post_Conditions (Items));
+ Save_Global_References_In_List (Contract_Test_Cases (Items));
+ Save_Global_References_In_List (Classifications (Items));
end if;
end if;
+ if Restore_Scope then
+ End_Scope;
+ end if;
+
-- Restore the SPARK_Mode of the enclosing context after all delayed
-- pragmas have been analyzed.
Generate_Definition (Designator);
end if;
- Set_Contract (Designator, Make_Contract (Sloc (Designator)));
-
if Nkind (N) = N_Function_Specification then
Set_Ekind (Designator, E_Function);
Set_Mechanism (Designator, Default_Mechanism);
and then Is_Subprogram_Or_Generic_Subprogram (E)
then
declare
- Inherited : constant Subprogram_List := Inherited_Subprograms (E);
- P : Node_Id;
+ Subps : constant Subprogram_List := Inherited_Subprograms (E);
+ Items : Node_Id;
+ Prag : Node_Id;
begin
- for J in Inherited'Range loop
- P := Pre_Post_Conditions (Contract (Inherited (J)));
- while Present (P) loop
- Error_Msg_Sloc := Sloc (P);
-
- if Class_Present (P) and then not Split_PPC (P) then
- if Pragma_Name (P) = Name_Precondition then
- Error_Msg_N ("info: & inherits `Pre''Class` aspect "
- & "from #?L?", E);
- else
- Error_Msg_N ("info: & inherits `Post''Class` aspect "
- & "from #?L?", E);
+ for Index in Subps'Range loop
+ Items := Contract (Subps (Index));
+
+ if Present (Items) then
+ Prag := Pre_Post_Conditions (Items);
+ while Present (Prag) loop
+ Error_Msg_Sloc := Sloc (Prag);
+
+ if Class_Present (Prag)
+ and then not Split_PPC (Prag)
+ then
+ if Pragma_Name (Prag) = Name_Precondition then
+ Error_Msg_N
+ ("info: & inherits `Pre''Class` aspect from "
+ & "#?L?", E);
+ else
+ Error_Msg_N
+ ("info: & inherits `Post''Class` aspect from "
+ & "#?L?", E);
+ end if;
end if;
- end if;
- P := Next_Pragma (P);
- end loop;
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end if;
end loop;
end;
end if;
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id);
-- Analyze all delayed aspects chained on the contract of subprogram body
- -- Body_Id as if they appeared at the end of a declarative region. The
- -- aspects in question are:
+ -- Body_Id as if they appeared at the end of a declarative region. Aspects
+ -- in question are:
+ -- Contract_Cases (stand alone body)
+ -- Depends (stand alone body)
+ -- Global (stand alone body)
+ -- Postcondition (stand alone body)
+ -- Precondition (stand alone body)
-- Refined_Depends
-- Refined_Global
+ -- Refined_Post
+ -- Test_Case (stand alone body)
- procedure Analyze_Subprogram_Contract (Subp : Entity_Id);
- -- Analyze all delayed aspects chained on the contract of subprogram Subp
- -- as if they appeared at the end of a declarative region. The aspects in
- -- question are:
+ procedure Analyze_Subprogram_Contract (Subp_Id : Entity_Id);
+ -- Analyze all delayed aspects chained on the contract of subprogram
+ -- Subp_Id as if they appeared at the end of a declarative region. The
+ -- aspects in question are:
-- Contract_Cases
-- Depends
-- Global
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
elsif Nkind (N) = N_Attribute_Reference
and then Is_Entity_Name (Prefix (N))
+ and then Present (Entity (Prefix (N)))
and then Is_Subprogram (Entity (Prefix (N)))
then
Reference_Seen := True;
Set_Ekind (Body_Id, E_Package_Body);
Set_Body_Entity (Spec_Id, Body_Id);
Set_Spec_Entity (Body_Id, Spec_Id);
- Set_Contract (Body_Id, Make_Contract (Sloc (Body_Id)));
-- Defining name for the package body is not a visible entity: Only the
-- defining name for the declaration is visible.
Generate_Definition (Id);
Enter_Name (Id);
- Set_Ekind (Id, E_Package);
- Set_Etype (Id, Standard_Void_Type);
- Set_Contract (Id, Make_Contract (Sloc (Id)));
+ Set_Ekind (Id, E_Package);
+ Set_Etype (Id, Standard_Void_Type);
-- Set SPARK_Mode from context only for non-generic package
-- constructed later at the freeze point, so indicate that the
-- completion has not been seen yet.
- Set_Contract (New_S, Empty);
Set_Ekind (New_S, E_Subprogram_Body);
New_S := Rename_Spec;
Set_Has_Completion (Rename_Spec, False);
-- is an array type we may already have a usable subtype for it, so we
-- can use it rather than generating a new one, because the bounds
-- will be the values of the discriminants and not discriminant refs.
- -- This simplifies value tracing in GNATProve.
+ -- This simplifies value tracing in GNATProve. For consistency, both
+ -- the entity name and the subtype come from the constrained component.
function Is_Reference_In_Subunit return Boolean;
-- In a subunit, the scope depth is not a proper measure of hiding,
function Available_Subtype return Boolean is
Comp : Entity_Id;
+
begin
Comp := First_Entity (Etype (P));
while Present (Comp) loop
if Chars (Comp) = Chars (Selector_Name (N)) then
Set_Etype (N, Etype (Comp));
- Set_Etype (Selector_Name (N), Etype (Comp));
+ Set_Entity (Selector_Name (N), Comp);
+ Set_Etype (Selector_Name (N), Etype (Comp));
return True;
end if;
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
begin
Generate_Definition (Def_Id);
- Set_Contract (Def_Id, Make_Contract (Sloc (Def_Id)));
+
Tasking_Used := True;
-- Case of no discrete subtype definition
-- _Post, _Invariant, or _Type_Invariant, which are special names used
-- in identifiers to represent these attribute references.
- procedure Check_SPARK_Aspect_For_ASIS (N : Node_Id);
- -- In ASIS mode we need to analyze the original expression in the aspect
- -- specification. For Initializes, Global, and related SPARK aspects, the
- -- expression has a sui-generis syntax which may be a list, an expression,
- -- or an aggregate.
-
procedure Check_State_And_Constituent_Use
(States : Elist_Id;
Constits : Elist_Id;
-- corresponding constituent from list Constits (if any) appear in the same
-- context denoted by Context. If this is the case, emit an error.
- function Find_Related_Subprogram_Or_Body
+ procedure Duplication_Error (Prag : Node_Id; Prev : Node_Id);
+ -- Subsidiary to routines Find_Related_Package_Or_Body and
+ -- Find_Related_Subprogram_Or_Body. Emit an error on pragma Prag that
+ -- duplicates previous pragma Prev.
+
+ function Find_Related_Package_Or_Body
(Prag : Node_Id;
Do_Checks : Boolean := False) return Node_Id;
- -- Subsidiary to the analysis of pragmas Contract_Cases, Depends, Global,
- -- Refined_Depends, Refined_Global and Refined_Post. Find the declaration
- -- of the related subprogram [body or stub] subject to pragma Prag. If flag
- -- Do_Checks is set, the routine reports duplicate pragmas and detects
- -- improper use of refinement pragmas in stand alone expression functions.
- -- The returned value depends on the related pragma as follows:
- -- 1) Pragmas Contract_Cases, Depends and Global yield the corresponding
- -- N_Subprogram_Declaration node or if the pragma applies to a stand
- -- alone body, the N_Subprogram_Body node or Empty if illegal.
- -- 2) Pragmas Refined_Depends, Refined_Global and Refined_Post yield
- -- N_Subprogram_Body or N_Subprogram_Body_Stub nodes or Empty if
- -- illegal.
+ -- Subsidiary to the analysis of pragmas Abstract_State, Initial_Condition,
+ -- Initializes and Refined_State. Find the declaration of the related
+ -- package [body] subject to pragma Prag. The return value is either
+ -- N_Package_Declaration, N_Package_Body or Empty if the placement of
+ -- the pragma is illegal. If flag Do_Checks is set, the routine reports
+ -- duplicate pragmas.
+
+ function Get_Argument
+ (Prag : Node_Id;
+ Spec_Id : Entity_Id := Empty) return Node_Id;
+ -- Obtain the argument of pragma Prag depending on context and the nature
+ -- of the pragma. The argument is extracted in the following manner:
+ --
+ -- When the pragma is generated from an aspect, return the corresponding
+ -- aspect for ASIS or when Spec_Id denotes a generic subprogram.
+ --
+ -- Otherwise return the first argument of Prag
+ --
+ -- Spec_Id denotes the entity of the subprogram spec where Prag resides
function Get_Base_Subprogram (Def_Id : Entity_Id) return Entity_Id;
-- If Def_Id refers to a renamed subprogram, then the base subprogram (the
-- tagged, unconstrained array, unconstrained record or a record with at
-- least one unconstrained component.
- procedure Preanalyze_CTC_Args (N, Arg_Req, Arg_Ens : Node_Id);
- -- Preanalyze the boolean expressions in the Requires and Ensures arguments
- -- of a Test_Case pragma if present (possibly Empty). We treat these as
- -- spec expressions (i.e. similar to a default expression).
-
procedure Record_Possible_Body_Reference
(State_Id : Entity_Id;
Ref : Node_Id);
procedure Rewrite_Assertion_Kind (N : Node_Id);
-- If N is Pre'Class, Post'Class, Invariant'Class, or Type_Invariant'Class,
-- then it is rewritten as an identifier with the corresponding special
- -- name _Pre, _Post, _Invariant, or _Type_Invariant. Used by pragmas
- -- Check, Check_Policy.
+ -- name _Pre, _Post, _Invariant, or _Type_Invariant. Used by pragmas Check
+ -- and Check_Policy.
procedure Set_Elab_Unit_Name (N : Node_Id; With_Item : Node_Id);
-- Place semantic information on the argument of an Elaborate/Elaborate_All
Subp_Decl := Find_Related_Subprogram_Or_Body (N);
Subp_Id := Defining_Entity (Subp_Decl);
- All_Cases := Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
+ All_Cases := Expression (Get_Argument (N, Subp_Id));
-- 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 Assert (Nkind (All_Cases) = N_Aggregate);
- if No (Component_Associations (All_Cases)) then
- Error_Msg_N ("wrong syntax for constract cases", N);
-
- -- Individual contract cases appear as component associations
+ if Present (Component_Associations (All_Cases)) then
- else
-- Ensure that the formal parameters are visible when analyzing all
-- clauses. This falls out of the general rule of aspects pertaining
-- to subprogram declarations. Skip the installation for subprogram
if not In_Open_Scopes (Subp_Id) then
Restore_Scope := True;
Push_Scope (Subp_Id);
- Install_Formals (Subp_Id);
+
+ if Is_Generic_Subprogram (Subp_Id) then
+ Install_Generic_Formals (Subp_Id);
+ else
+ Install_Formals (Subp_Id);
+ end if;
end if;
CCase := First (Component_Associations (All_Cases));
if Restore_Scope then
End_Scope;
end if;
+ else
+ Error_Msg_N ("wrong syntax for constract cases", N);
end if;
end Analyze_Contract_Cases_In_Decl_Part;
SPARK_Msg_NE
("cannot mention state & in global refinement",
Item, Item_Id);
- SPARK_Msg_N
- ("\use its constituents instead", Item);
+ SPARK_Msg_N ("\use its constituents instead", Item);
return;
-- If the reference to the abstract state appears in
-- Local variables
- Deps : constant Node_Id :=
- Get_Pragma_Arg
- (First (Pragma_Argument_Associations (N)));
Clause : Node_Id;
+ Deps : Node_Id;
Errors : Nat;
Last_Clause : Node_Id;
Subp_Decl : Node_Id;
Subp_Decl := Find_Related_Subprogram_Or_Body (N);
Subp_Id := Defining_Entity (Subp_Decl);
+ Deps := Expression (Get_Argument (N, Subp_Id));
-- The logic in this routine is used to analyze both pragma Depends and
-- pragma Refined_Depends since they have the same syntax and base
-- semantics. Find the entity of the corresponding spec when analyzing
-- Refined_Depends.
- if Nkind (Subp_Decl) = N_Subprogram_Body
- and then Present (Corresponding_Spec (Subp_Decl))
- then
- Spec_Id := Corresponding_Spec (Subp_Decl);
-
- elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub
- and then Present (Corresponding_Spec_Of_Stub (Subp_Decl))
- then
- Spec_Id := Corresponding_Spec_Of_Stub (Subp_Decl);
-
- else
- Spec_Id := Subp_Id;
- end if;
+ Spec_Id := Corresponding_Spec_Of (Subp_Decl);
-- Empty dependency list
if not In_Open_Scopes (Spec_Id) then
Restore_Scope := True;
Push_Scope (Spec_Id);
- Install_Formals (Spec_Id);
+
+ if Is_Generic_Subprogram (Spec_Id) then
+ Install_Generic_Formals (Spec_Id);
+ else
+ Install_Formals (Spec_Id);
+ end if;
end if;
Clause := First (Component_Associations (Deps));
-- Local variables
- Items : constant Node_Id :=
- Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
+ Items : Node_Id;
Subp_Decl : Node_Id;
Restore_Scope : Boolean := False;
-- Set True if we do a Push_Scope requiring a Pop_Scope on exit
- -- Start of processing for Analyze_Global_In_Decl_List
+ -- Start of processing for Analyze_Global_In_Decl_Part
begin
Set_Analyzed (N);
- Check_SPARK_Aspect_For_ASIS (N);
Subp_Decl := Find_Related_Subprogram_Or_Body (N);
Subp_Id := Defining_Entity (Subp_Decl);
+ Items := Expression (Get_Argument (N, Subp_Id));
-- The logic in this routine is used to analyze both pragma Global and
-- pragma Refined_Global since they have the same syntax and base
-- semantics. Find the entity of the corresponding spec when analyzing
-- Refined_Global.
- if Nkind (Subp_Decl) = N_Subprogram_Body
- and then Present (Corresponding_Spec (Subp_Decl))
- then
- Spec_Id := Corresponding_Spec (Subp_Decl);
-
- elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub
- and then Present (Corresponding_Spec_Of_Stub (Subp_Decl))
- then
- Spec_Id := Corresponding_Spec_Of_Stub (Subp_Decl);
-
- else
- Spec_Id := Subp_Id;
- end if;
+ Spec_Id := Corresponding_Spec_Of (Subp_Decl);
-- There is nothing to be done for a null global list
if not In_Open_Scopes (Spec_Id) then
Restore_Scope := True;
Push_Scope (Spec_Id);
- Install_Formals (Spec_Id);
+
+ if Is_Generic_Subprogram (Spec_Id) then
+ Install_Generic_Formals (Spec_Id);
+ else
+ Install_Formals (Spec_Id);
+ end if;
end if;
Analyze_Global_List (Items);
--------------------------------------------
procedure Analyze_Initial_Condition_In_Decl_Part (N : Node_Id) is
- Expr : constant Node_Id :=
- Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
+ Expr : constant Node_Id := Expression (Get_Argument (N));
begin
Set_Analyzed (N);
-- Local variables
- Inits : constant Node_Id :=
- Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
+ Inits : constant Node_Id := Expression (Get_Argument (N));
Init : Node_Id;
-- Start of processing for Analyze_Initializes_In_Decl_Part
begin
Set_Analyzed (N);
- Check_SPARK_Aspect_For_ASIS (N);
-
-- Nothing to do when the initialization list is empty
if Nkind (Inits) = N_Null then
-- encapsulating state. Indic is the Part_Of indicator. Flag Legal is
-- set when the indicator is legal.
+ procedure Analyze_Pre_Post_Condition;
+ -- Subsidiary to the analysis of pragmas Precondition and Postcondition
+
procedure Analyze_Refined_Pragma
(Spec_Id : out Entity_Id;
Body_Id : out Entity_Id;
-- In this version of the procedure, the identifier name is given as
-- a string with lower case letters.
- procedure Check_Pre_Post;
- -- Called to perform checks for Pre, Pre_Class, Post, Post_Class
- -- pragmas. These are processed by transformation to equivalent
- -- Precondition and Postcondition pragmas, but Pre and Post need an
- -- additional check that they are not used in a subprogram body when
- -- there is a separate spec present.
-
- procedure Check_Precondition_Postcondition (In_Body : out Boolean);
- -- Called to process a precondition or postcondition pragma. There are
- -- three cases:
- --
- -- The pragma appears after a subprogram spec
- --
- -- If the corresponding check is not enabled, the pragma is analyzed
- -- but otherwise ignored and control returns with In_Body set False.
- --
- -- If the check is enabled, then the first step is to analyze the
- -- pragma, but this is skipped if the subprogram spec appears within
- -- a package specification (because this is the case where we delay
- -- analysis till the end of the spec). Then (whether or not it was
- -- analyzed), the pragma is chained to the subprogram in question
- -- (using Pre_Post_Conditions and Next_Pragma) and control returns
- -- to the caller with In_Body set False.
- --
- -- The pragma appears at the start of subprogram body declarations
- --
- -- In this case an immediate return to the caller is made with
- -- In_Body set True, and the pragma is NOT analyzed.
- --
- -- In all other cases, an error message for bad placement is given
-
procedure Check_Static_Constraint (Constr : Node_Id);
-- Constr is a constraint from an N_Subtype_Indication node from a
-- component constraint in an Unchecked_Union type. This routine checks
-- that the constraint is static as required by the restrictions for
-- Unchecked_Union.
- procedure Check_Test_Case;
- -- Called to process a test-case pragma. It starts with checking pragma
- -- arguments, and the rest of the treatment is similar to the one for
- -- pre- and postcondition in Check_Precondition_Postcondition, except
- -- the placement rules for the test-case pragma are stricter. These
- -- pragmas may only occur after a subprogram spec declared directly
- -- in a package spec unit. In this case, the pragma is chained to the
- -- subprogram in question (using Contract_Test_Cases and Next_Pragma)
- -- and analysis of the pragma is delayed till the end of the spec. In
- -- all other cases, an error message for bad placement is given.
-
procedure Check_Valid_Configuration_Pragma;
-- Legality checks for placement of a configuration pragma
-- presence of at least one component. UU_Typ is the related Unchecked_
-- Union type.
+ procedure Create_Generic_Template
+ (Prag : Node_Id;
+ Subp_Id : Entity_Id);
+ -- Subsidiary routine to the processing of pragmas Contract_Cases,
+ -- Depends, Global, Postcondition, Precondition and Test_Case. Create
+ -- a generic template for pragma Prag when Prag is a source construct
+ -- and the related context denoted by Subp_Id is a generic subprogram.
+
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.
+ -- 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.
procedure Error_Pragma (Msg : String);
pragma No_Return (Error_Pragma);
Legal := True;
end Analyze_Part_Of;
+ --------------------------------
+ -- Analyze_Pre_Post_Condition --
+ --------------------------------
+
+ procedure Analyze_Pre_Post_Condition is
+ Prag_Iden : constant Node_Id := Pragma_Identifier (N);
+ Subp_Decl : Node_Id;
+ Subp_Id : Entity_Id;
+
+ Duplicates_OK : Boolean := False;
+ -- Flag set when a pre/postcondition allows multiple pragmas of the
+ -- same kind.
+
+ In_Body_OK : Boolean := False;
+ -- Flag set when a pre/postcondition is allowed to appear on a body
+ -- even though the subprogram may have a spec.
+
+ Is_Pre_Post : Boolean := False;
+ -- Flag set when the pragma is one of Pre, Pre_Class, Post or
+ -- Post_Class.
+
+ begin
+ -- Change the name of pragmas Pre, Pre_Class, Post and Post_Class to
+ -- offer uniformity among the various kinds of pre/postconditions by
+ -- rewriting the pragma identifier. This allows the retrieval of the
+ -- original pragma name by routine Original_Aspect_Pragma_Name.
+
+ if Comes_From_Source (N) then
+ if Nam_In (Pname, Name_Pre, Name_Pre_Class) then
+ Is_Pre_Post := True;
+ Set_Class_Present (N, Pname = Name_Pre_Class);
+ Rewrite (Prag_Iden, Make_Identifier (Loc, Name_Precondition));
+
+ elsif Nam_In (Pname, Name_Post, Name_Post_Class) then
+ Is_Pre_Post := True;
+ Set_Class_Present (N, Pname = Name_Post_Class);
+ Rewrite (Prag_Iden, Make_Identifier (Loc, Name_Postcondition));
+ end if;
+ end if;
+
+ -- Determine the semantics with respect to duplicates and placement
+ -- in a body. Pragmas Precondition and Postcondition were introduced
+ -- before aspects and are not subject to the same aspect-like rules.
+
+ if Nam_In (Pname, Name_Precondition, Name_Postcondition) then
+ Duplicates_OK := True;
+ In_Body_OK := True;
+ end if;
+
+ GNAT_Pragma;
+
+ -- Pragmas Pre, Pre_Class, Post and Post_Class allow for a single
+ -- argument without an identifier.
+
+ if Is_Pre_Post then
+ Check_Arg_Count (1);
+ Check_No_Identifiers;
+
+ -- Pragmas Precondition and Postcondition have complex argument
+ -- profile.
+
+ else
+ Check_At_Least_N_Arguments (1);
+ Check_At_Most_N_Arguments (2);
+ Check_Optional_Identifier (Arg1, Name_Check);
+
+ if Present (Arg2) then
+ Check_Optional_Identifier (Arg2, Name_Message);
+ Preanalyze_Spec_Expression
+ (Get_Pragma_Arg (Arg2), Standard_String);
+ end if;
+ end if;
+
+ -- For a pragma PPC in the extended main source unit, record enabled
+ -- status in SCO.
+ -- ??? nothing checks that the pragma is in the main source unit
+
+ if Is_Checked (N) and then not Split_PPC (N) then
+ Set_SCO_Pragma_Enabled (Loc);
+ end if;
+
+ -- Ensure the proper placement of the pragma
+
+ Subp_Decl :=
+ Find_Related_Subprogram_Or_Body (N, Do_Checks => not Duplicates_OK);
+
+ -- When a pre/postcondition pragma applies to an abstract subprogram,
+ -- its original form must be an aspect with 'Class.
+
+ if Nkind (Subp_Decl) = N_Abstract_Subprogram_Declaration then
+ if not From_Aspect_Specification (N) then
+ Error_Pragma
+ ("pragma % cannot be applied to abstract subprogram");
+
+ elsif not Class_Present (N) then
+ Error_Pragma
+ ("aspect % requires ''Class for abstract subprogram");
+ end if;
+
+ -- Entry declaration
+
+ elsif Nkind (Subp_Decl) = N_Entry_Declaration then
+ null;
+
+ -- Generic subprogram declaration
+
+ elsif Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then
+ null;
+
+ -- Subprogram body
+
+ elsif Nkind (Subp_Decl) = N_Subprogram_Body
+ and then (No (Corresponding_Spec (Subp_Decl)) or In_Body_OK)
+ then
+ null;
+
+ -- Subprogram body stub
+
+ elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub
+ and then (No (Corresponding_Spec_Of_Stub (Subp_Decl)) or In_Body_OK)
+ then
+ null;
+
+ -- Subprogram declaration
+
+ elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then
+
+ -- AI05-0230: When a pre/postcondition pragma applies to a null
+ -- procedure, its original form must be an aspect with 'Class.
+
+ if Nkind (Specification (Subp_Decl)) = N_Procedure_Specification
+ and then Null_Present (Specification (Subp_Decl))
+ and then From_Aspect_Specification (N)
+ and then not Class_Present (N)
+ then
+ Error_Pragma ("aspect % requires ''Class for null procedure");
+ end if;
+
+ -- Otherwise the placement is illegal
+
+ else
+ Pragma_Misplaced;
+ return;
+ end if;
+
+ Subp_Id := Defining_Entity (Subp_Decl);
+
+ -- Construct a generic template for the pragma when the context is a
+ -- generic subprogram and the pragma is a source construct.
+
+ Create_Generic_Template (N, Subp_Id);
+
+ -- Fully analyze the pragma when it appears inside a subprogram
+ -- body because it cannot benefit from forward references.
+
+ if Nkind_In (Subp_Decl, N_Subprogram_Body,
+ N_Subprogram_Body_Stub)
+ then
+ Analyze_Pre_Post_Condition_In_Decl_Part (N);
+ end if;
+
+ -- Chain the pragma on the contract for further processing
+
+ Add_Contract_Item (N, Subp_Id);
+ end Analyze_Pre_Post_Condition;
+
----------------------------
-- Analyze_Refined_Pragma --
----------------------------
Check_Arg_Count (1);
Check_No_Identifiers;
- if Nam_In (Pname, Name_Refined_Depends,
- Name_Refined_Global,
- Name_Refined_State)
- then
- Ensure_Aggregate_Form (Arg1);
- end if;
-
-- Verify the placement of the pragma and check for duplicates. The
-- pragma must apply to a subprogram body [stub].
-- declared in the visible part of a package. Retrieve the context of
-- the subprogram declaration.
- Spec_Decl := Parent (Parent (Spec_Id));
+ Spec_Decl := Unit_Declaration_Node (Spec_Id);
if Nkind (Parent (Spec_Decl)) /= N_Package_Specification then
Error_Pragma
-- If we get here, then the pragma is legal
+ if Nam_In (Pname, Name_Refined_Depends,
+ Name_Refined_Global,
+ Name_Refined_State)
+ then
+ Ensure_Aggregate_Form (Get_Argument (N));
+ end if;
+
Legal := True;
end Analyze_Refined_Pragma;
Check_Optional_Identifier (Arg, Name_Find);
end Check_Optional_Identifier;
- --------------------
- -- Check_Pre_Post --
- --------------------
-
- procedure Check_Pre_Post is
- P : Node_Id;
- PO : Node_Id;
-
- begin
- if not Is_List_Member (N) then
- Pragma_Misplaced;
- end if;
-
- -- If we are within an inlined body, the legality of the pragma
- -- has been checked already.
+ -----------------------------
+ -- Check_Static_Constraint --
+ -----------------------------
- if In_Inlined_Body then
- return;
- end if;
+ -- Note: for convenience in writing this procedure, in addition to
+ -- the officially (i.e. by spec) allowed argument which is always a
+ -- constraint, it also allows ranges and discriminant associations.
+ -- Above is not clear ???
- -- Search prior declarations
+ procedure Check_Static_Constraint (Constr : Node_Id) is
- P := N;
- while Present (Prev (P)) loop
- P := Prev (P);
+ procedure Require_Static (E : Node_Id);
+ -- Require given expression to be static expression
- -- If the previous node is a generic subprogram, do not go to to
- -- the original node, which is the unanalyzed tree: we need to
- -- attach the pre/postconditions to the analyzed version at this
- -- point. They get propagated to the original tree when analyzing
- -- the corresponding body.
+ --------------------
+ -- Require_Static --
+ --------------------
- if Nkind (P) not in N_Generic_Declaration then
- PO := Original_Node (P);
- else
- PO := P;
+ procedure Require_Static (E : Node_Id) is
+ begin
+ if not Is_OK_Static_Expression (E) then
+ Flag_Non_Static_Expr
+ ("non-static constraint not allowed in Unchecked_Union!", E);
+ raise Pragma_Exit;
end if;
+ end Require_Static;
- -- Skip past prior pragma
+ -- Start of processing for Check_Static_Constraint
- if Nkind (PO) = N_Pragma then
- null;
+ begin
+ case Nkind (Constr) is
+ when N_Discriminant_Association =>
+ Require_Static (Expression (Constr));
- -- Skip stuff not coming from source
+ when N_Range =>
+ Require_Static (Low_Bound (Constr));
+ Require_Static (High_Bound (Constr));
- elsif not Comes_From_Source (PO) then
+ when N_Attribute_Reference =>
+ Require_Static (Type_Low_Bound (Etype (Prefix (Constr))));
+ Require_Static (Type_High_Bound (Etype (Prefix (Constr))));
- -- The condition may apply to a subprogram instantiation
+ when N_Range_Constraint =>
+ Check_Static_Constraint (Range_Expression (Constr));
- if Nkind (PO) = N_Subprogram_Declaration
- and then Present (Generic_Parent (Specification (PO)))
- then
- return;
+ when N_Index_Or_Discriminant_Constraint =>
+ declare
+ IDC : Entity_Id;
+ begin
+ IDC := First (Constraints (Constr));
+ while Present (IDC) loop
+ Check_Static_Constraint (IDC);
+ Next (IDC);
+ end loop;
+ end;
- elsif Nkind (PO) = N_Subprogram_Declaration
- and then In_Instance
- then
- return;
+ when others =>
+ null;
+ end case;
+ end Check_Static_Constraint;
- -- For all other cases of non source code, do nothing
+ --------------------------------------
+ -- Check_Valid_Configuration_Pragma --
+ --------------------------------------
- else
- null;
- end if;
+ -- A configuration pragma must appear in the context clause of a
+ -- compilation unit, and only other pragmas may precede it. Note that
+ -- the test also allows use in a configuration pragma file.
- -- Only remaining possibility is subprogram declaration
+ procedure Check_Valid_Configuration_Pragma is
+ begin
+ if not Is_Configuration_Pragma then
+ Error_Pragma ("incorrect placement for configuration pragma%");
+ end if;
+ end Check_Valid_Configuration_Pragma;
- else
- return;
- end if;
- end loop;
+ -------------------------------------
+ -- Check_Valid_Library_Unit_Pragma --
+ -------------------------------------
- -- If we fall through loop, pragma is at start of list, so see if it
- -- is at the start of declarations of a subprogram body.
+ procedure Check_Valid_Library_Unit_Pragma is
+ Plist : List_Id;
+ Parent_Node : Node_Id;
+ Unit_Name : Entity_Id;
+ Unit_Kind : Node_Kind;
+ Unit_Node : Node_Id;
+ Sindex : Source_File_Index;
- PO := Parent (N);
+ begin
+ if not Is_List_Member (N) then
+ Pragma_Misplaced;
- if Nkind (PO) = N_Subprogram_Body
- and then List_Containing (N) = Declarations (PO)
- then
- -- This is only allowed if there is no separate specification
+ else
+ Plist := List_Containing (N);
+ Parent_Node := Parent (Plist);
- if Present (Corresponding_Spec (PO)) then
- Error_Pragma
- ("pragma% must apply to subprogram specification");
- end if;
-
- return;
- end if;
- end Check_Pre_Post;
-
- --------------------------------------
- -- Check_Precondition_Postcondition --
- --------------------------------------
-
- procedure Check_Precondition_Postcondition (In_Body : out Boolean) is
- P : Node_Id;
- PO : Node_Id;
-
- procedure Chain_PPC (PO : Node_Id);
- -- If PO is an entry or a [generic] subprogram declaration node, then
- -- the precondition/postcondition applies to this subprogram and the
- -- processing for the pragma is completed. Otherwise the pragma is
- -- misplaced.
-
- ---------------
- -- Chain_PPC --
- ---------------
-
- procedure Chain_PPC (PO : Node_Id) is
- S : Entity_Id;
-
- begin
- if Nkind (PO) = N_Abstract_Subprogram_Declaration then
- if not From_Aspect_Specification (N) then
- Error_Pragma
- ("pragma% cannot be applied to abstract subprogram");
-
- elsif Class_Present (N) then
- null;
-
- else
- Error_Pragma
- ("aspect % requires ''Class for abstract subprogram");
- end if;
-
- -- AI05-0230: The same restriction applies to null procedures. For
- -- compatibility with earlier uses of the Ada pragma, apply this
- -- rule only to aspect specifications.
-
- -- The above discrepency needs documentation. Robert is dubious
- -- about whether it is a good idea ???
-
- elsif Nkind (PO) = N_Subprogram_Declaration
- and then Nkind (Specification (PO)) = N_Procedure_Specification
- and then Null_Present (Specification (PO))
- and then From_Aspect_Specification (N)
- and then not Class_Present (N)
- then
- Error_Pragma
- ("aspect % requires ''Class for null procedure");
-
- -- Pre/postconditions are legal on a subprogram body if it is not
- -- a completion of a declaration. They are also legal on a stub
- -- with no previous declarations (this is checked when processing
- -- the corresponding aspects).
-
- elsif Nkind (PO) = N_Subprogram_Body
- and then Acts_As_Spec (PO)
- then
- null;
-
- elsif Nkind (PO) = N_Subprogram_Body_Stub then
- null;
-
- elsif not Nkind_In (PO, N_Subprogram_Declaration,
- N_Expression_Function,
- N_Generic_Subprogram_Declaration,
- N_Entry_Declaration)
- then
- Pragma_Misplaced;
- end if;
-
- -- Here if we have [generic] subprogram or entry declaration
-
- if Nkind (PO) = N_Entry_Declaration then
- S := Defining_Entity (PO);
- else
- S := Defining_Unit_Name (Specification (PO));
-
- if Nkind (S) = N_Defining_Program_Unit_Name then
- S := Defining_Identifier (S);
- end if;
- end if;
-
- -- Note: we do not analyze the pragma at this point. Instead we
- -- delay this analysis until the end of the declarative part in
- -- which the pragma appears. This implements the required delay
- -- in this analysis, allowing forward references. The analysis
- -- happens at the end of Analyze_Declarations.
-
- -- Chain spec PPC pragma to list for subprogram
-
- Add_Contract_Item (N, S);
-
- -- Return indicating spec case
-
- In_Body := False;
- return;
- end Chain_PPC;
-
- -- Start of processing for Check_Precondition_Postcondition
-
- begin
- if not Is_List_Member (N) then
- Pragma_Misplaced;
- end if;
-
- -- Preanalyze message argument if present. Visibility in this
- -- argument is established at the point of pragma occurrence.
-
- if Arg_Count = 2 then
- Check_Optional_Identifier (Arg2, Name_Message);
- Preanalyze_Spec_Expression
- (Get_Pragma_Arg (Arg2), Standard_String);
- end if;
-
- -- For a pragma PPC in the extended main source unit, record enabled
- -- status in SCO.
-
- if Is_Checked (N) and then not Split_PPC (N) then
- Set_SCO_Pragma_Enabled (Loc);
- end if;
-
- -- If we are within an inlined body, the legality of the pragma
- -- has been checked already.
-
- if In_Inlined_Body then
- In_Body := True;
- return;
- end if;
-
- -- Search prior declarations
-
- P := N;
- while Present (Prev (P)) loop
- P := Prev (P);
-
- -- If the previous node is a generic subprogram, do not go to to
- -- the original node, which is the unanalyzed tree: we need to
- -- attach the pre/postconditions to the analyzed version at this
- -- point. They get propagated to the original tree when analyzing
- -- the corresponding body.
-
- if Nkind (P) not in N_Generic_Declaration then
- PO := Original_Node (P);
- else
- PO := P;
- end if;
-
- -- Skip past prior pragma
-
- if Nkind (PO) = N_Pragma then
- null;
-
- -- Skip stuff not coming from source
-
- elsif not Comes_From_Source (PO) then
-
- -- The condition may apply to a subprogram instantiation
-
- if Nkind (PO) = N_Subprogram_Declaration
- and then Present (Generic_Parent (Specification (PO)))
- then
- Chain_PPC (PO);
- return;
-
- elsif Nkind (PO) = N_Subprogram_Declaration
- and then In_Instance
- then
- Chain_PPC (PO);
- return;
-
- -- For all other cases of non source code, do nothing
-
- else
- null;
- end if;
-
- -- Only remaining possibility is subprogram declaration
-
- else
- Chain_PPC (PO);
- return;
- end if;
- end loop;
-
- -- If we fall through loop, pragma is at start of list, so see if it
- -- is at the start of declarations of a subprogram body.
-
- PO := Parent (N);
-
- if Nkind (PO) = N_Subprogram_Body
- and then List_Containing (N) = Declarations (PO)
- then
- if Operating_Mode /= Generate_Code or else Inside_A_Generic then
-
- -- Analyze pragma expression for correctness and for ASIS use
-
- Preanalyze_Assert_Expression
- (Get_Pragma_Arg (Arg1), Standard_Boolean);
-
- -- In ASIS mode, for a pragma generated from a source aspect,
- -- also analyze the original aspect expression.
-
- if ASIS_Mode and then Present (Corresponding_Aspect (N)) then
- Preanalyze_Assert_Expression
- (Expression (Corresponding_Aspect (N)), Standard_Boolean);
- end if;
- end if;
-
- -- Retain copy of the pre/postcondition pragma in GNATprove mode.
- -- The copy is needed because the pragma is expanded into other
- -- constructs which are not acceptable in the N_Contract node.
-
- if Acts_As_Spec (PO) and then GNATprove_Mode then
- declare
- Prag : constant Node_Id := New_Copy_Tree (N);
-
- begin
- -- Preanalyze the pragma
-
- Preanalyze_Assert_Expression
- (Get_Pragma_Arg
- (First (Pragma_Argument_Associations (Prag))),
- Standard_Boolean);
-
- -- Preanalyze the corresponding aspect (if any)
-
- if Present (Corresponding_Aspect (Prag)) then
- Preanalyze_Assert_Expression
- (Expression (Corresponding_Aspect (Prag)),
- Standard_Boolean);
- end if;
-
- -- Chain the copy on the contract of the body
-
- Add_Contract_Item
- (Prag, Defining_Unit_Name (Specification (PO)));
- end;
- end if;
-
- In_Body := True;
- return;
-
- -- See if it is in the pragmas after a library level subprogram
-
- elsif Nkind (PO) = N_Compilation_Unit_Aux then
-
- -- In GNATprove mode, analyze pragma expression for correctness,
- -- as it is not expanded later. Ditto in ASIS_Mode where there is
- -- no later point at which the aspect will be analyzed.
-
- if GNATprove_Mode or ASIS_Mode then
- Analyze_Pre_Post_Condition_In_Decl_Part
- (N, Defining_Entity (Unit (Parent (PO))));
- end if;
-
- Chain_PPC (Unit (Parent (PO)));
- return;
- end if;
-
- -- If we fall through, pragma was misplaced
-
- Pragma_Misplaced;
- end Check_Precondition_Postcondition;
-
- -----------------------------
- -- Check_Static_Constraint --
- -----------------------------
-
- -- Note: for convenience in writing this procedure, in addition to
- -- the officially (i.e. by spec) allowed argument which is always a
- -- constraint, it also allows ranges and discriminant associations.
- -- Above is not clear ???
-
- procedure Check_Static_Constraint (Constr : Node_Id) is
-
- procedure Require_Static (E : Node_Id);
- -- Require given expression to be static expression
-
- --------------------
- -- Require_Static --
- --------------------
-
- procedure Require_Static (E : Node_Id) is
- begin
- if not Is_OK_Static_Expression (E) then
- Flag_Non_Static_Expr
- ("non-static constraint not allowed in Unchecked_Union!", E);
- raise Pragma_Exit;
- end if;
- end Require_Static;
-
- -- Start of processing for Check_Static_Constraint
-
- begin
- case Nkind (Constr) is
- when N_Discriminant_Association =>
- Require_Static (Expression (Constr));
-
- when N_Range =>
- Require_Static (Low_Bound (Constr));
- Require_Static (High_Bound (Constr));
-
- when N_Attribute_Reference =>
- Require_Static (Type_Low_Bound (Etype (Prefix (Constr))));
- Require_Static (Type_High_Bound (Etype (Prefix (Constr))));
-
- when N_Range_Constraint =>
- Check_Static_Constraint (Range_Expression (Constr));
-
- when N_Index_Or_Discriminant_Constraint =>
- declare
- IDC : Entity_Id;
- begin
- IDC := First (Constraints (Constr));
- while Present (IDC) loop
- Check_Static_Constraint (IDC);
- Next (IDC);
- end loop;
- end;
-
- when others =>
- null;
- end case;
- end Check_Static_Constraint;
-
- ---------------------
- -- Check_Test_Case --
- ---------------------
-
- procedure Check_Test_Case is
- P : Node_Id;
- PO : Node_Id;
-
- procedure Chain_CTC (PO : Node_Id);
- -- If PO is a [generic] subprogram declaration node, then the
- -- test-case applies to this subprogram and the processing for
- -- the pragma is completed. Otherwise the pragma is misplaced.
-
- ---------------
- -- Chain_CTC --
- ---------------
-
- procedure Chain_CTC (PO : Node_Id) is
- Name : constant String_Id := Get_Name_From_CTC_Pragma (N);
- CTC : Node_Id;
- S : Entity_Id;
-
- begin
- if Nkind (PO) = N_Abstract_Subprogram_Declaration then
- Error_Pragma
- ("pragma% cannot be applied to abstract subprogram");
-
- elsif Nkind (PO) = N_Entry_Declaration then
- Error_Pragma ("pragma% cannot be applied to entry");
-
- elsif not Nkind_In (PO, N_Subprogram_Declaration,
- N_Generic_Subprogram_Declaration)
- then
- Pragma_Misplaced;
- end if;
-
- -- Here if we have [generic] subprogram declaration
-
- S := Defining_Unit_Name (Specification (PO));
-
- -- Note: we do not analyze the pragma at this point. Instead we
- -- delay this analysis until the end of the declarative part in
- -- which the pragma appears. This implements the required delay
- -- in this analysis, allowing forward references. The analysis
- -- happens at the end of Analyze_Declarations.
-
- -- There should not be another test-case with the same name
- -- associated to this subprogram.
-
- CTC := Contract_Test_Cases (Contract (S));
- while Present (CTC) loop
-
- -- Omit pragma Contract_Cases because it does not introduce
- -- a unique case name and it does not follow the syntax of
- -- Test_Case.
-
- if Pragma_Name (CTC) = Name_Contract_Cases then
- null;
-
- elsif String_Equal (Name, Get_Name_From_CTC_Pragma (CTC)) then
- Error_Msg_Sloc := Sloc (CTC);
- Error_Pragma ("name for pragma% is already used#");
- end if;
-
- CTC := Next_Pragma (CTC);
- end loop;
-
- -- Chain spec CTC pragma to list for subprogram
-
- Add_Contract_Item (N, S);
- end Chain_CTC;
-
- -- Start of processing for Check_Test_Case
-
- begin
- -- First check pragma arguments
-
- Check_At_Least_N_Arguments (2);
- Check_At_Most_N_Arguments (4);
- Check_Arg_Order
- ((Name_Name, Name_Mode, Name_Requires, Name_Ensures));
-
- Check_Optional_Identifier (Arg1, Name_Name);
- Check_Arg_Is_OK_Static_Expression (Arg1, Standard_String);
-
- -- In ASIS mode, for a pragma generated from a source aspect, also
- -- analyze the original aspect expression.
-
- if ASIS_Mode and then Present (Corresponding_Aspect (N)) then
- Check_Expr_Is_OK_Static_Expression
- (Original_Node (Get_Pragma_Arg (Arg1)), Standard_String);
- end if;
-
- Check_Optional_Identifier (Arg2, Name_Mode);
- Check_Arg_Is_One_Of (Arg2, Name_Nominal, Name_Robustness);
-
- if Arg_Count = 4 then
- Check_Identifier (Arg3, Name_Requires);
- Check_Identifier (Arg4, Name_Ensures);
-
- elsif Arg_Count = 3 then
- Check_Identifier_Is_One_Of (Arg3, Name_Requires, Name_Ensures);
- end if;
-
- -- Check pragma placement
-
- if not Is_List_Member (N) then
- Pragma_Misplaced;
- end if;
-
- -- Test-case should only appear in package spec unit
-
- if Get_Source_Unit (N) = No_Unit
- or else not Nkind_In (Sinfo.Unit (Cunit (Current_Sem_Unit)),
- N_Package_Declaration,
- N_Generic_Package_Declaration)
- then
- Pragma_Misplaced;
- end if;
-
- -- Search prior declarations
-
- P := N;
- while Present (Prev (P)) loop
- P := Prev (P);
-
- -- If the previous node is a generic subprogram, do not go to to
- -- the original node, which is the unanalyzed tree: we need to
- -- attach the test-case to the analyzed version at this point.
- -- They get propagated to the original tree when analyzing the
- -- corresponding body.
-
- if Nkind (P) not in N_Generic_Declaration then
- PO := Original_Node (P);
- else
- PO := P;
- end if;
-
- -- Skip past prior pragma
-
- if Nkind (PO) = N_Pragma then
- null;
-
- -- Skip stuff not coming from source
-
- elsif not Comes_From_Source (PO) then
- null;
-
- -- Only remaining possibility is subprogram declaration. First
- -- check that it is declared directly in a package declaration.
- -- This may be either the package declaration for the current unit
- -- being defined or a local package declaration.
-
- elsif not Present (Parent (Parent (PO)))
- or else not Present (Parent (Parent (Parent (PO))))
- or else not Nkind_In (Parent (Parent (PO)),
- N_Package_Declaration,
- N_Generic_Package_Declaration)
- then
- Pragma_Misplaced;
-
- else
- Chain_CTC (PO);
- return;
- end if;
- end loop;
-
- -- If we fall through, pragma was misplaced
-
- Pragma_Misplaced;
- end Check_Test_Case;
-
- --------------------------------------
- -- Check_Valid_Configuration_Pragma --
- --------------------------------------
-
- -- A configuration pragma must appear in the context clause of a
- -- compilation unit, and only other pragmas may precede it. Note that
- -- the test also allows use in a configuration pragma file.
-
- procedure Check_Valid_Configuration_Pragma is
- begin
- if not Is_Configuration_Pragma then
- Error_Pragma ("incorrect placement for configuration pragma%");
- end if;
- end Check_Valid_Configuration_Pragma;
-
- -------------------------------------
- -- Check_Valid_Library_Unit_Pragma --
- -------------------------------------
-
- procedure Check_Valid_Library_Unit_Pragma is
- Plist : List_Id;
- Parent_Node : Node_Id;
- Unit_Name : Entity_Id;
- Unit_Kind : Node_Kind;
- Unit_Node : Node_Id;
- Sindex : Source_File_Index;
-
- begin
- if not Is_List_Member (N) then
- Pragma_Misplaced;
-
- else
- Plist := List_Containing (N);
- Parent_Node := Parent (Plist);
-
- if Parent_Node = Empty then
- Pragma_Misplaced;
+ if Parent_Node = Empty then
+ Pragma_Misplaced;
-- Case of pragma appearing after a compilation unit. In this case
-- it must have an argument with the corresponding name and must
end loop;
end Check_Variant;
+ -----------------------------
+ -- Create_Generic_Template --
+ -----------------------------
+
+ procedure Create_Generic_Template
+ (Prag : Node_Id;
+ Subp_Id : Entity_Id)
+ is
+ begin
+ if Comes_From_Source (Prag)
+ and then Is_Generic_Subprogram (Subp_Id)
+ then
+ Rewrite
+ (Prag, Copy_Generic_Node (Prag, Empty, Instantiating => False));
+ end if;
+ end Create_Generic_Template;
+
---------------------------
-- Ensure_Aggregate_Form --
---------------------------
procedure Ensure_Aggregate_Form (Arg : Node_Id) is
- Expr : constant Node_Id := Get_Pragma_Arg (Arg);
- Loc : constant Source_Ptr := Sloc (Arg);
- Nam : constant Name_Id := Chars (Arg);
+ Expr : constant Node_Id := Expression (Arg);
+ Loc : constant Source_Ptr := Sloc (Expr);
Comps : List_Id := No_List;
Exprs : List_Id := No_List;
+ Nam : Name_Id;
CFSD : constant Boolean := Get_Comes_From_Source_Default;
-- Used to restore Comes_From_Source_Default
begin
+ if Nkind (Arg) = N_Aspect_Specification then
+ Nam := No_Name;
+ else
+ pragma Assert (Nkind (Arg) = N_Pragma_Argument_Association);
+ Nam := Chars (Arg);
+ end if;
+
-- The argument is already in aggregate form, but the presence of a
- -- name causes this to be interpreted as a named association which in
+ -- name causes this to be interpreted as named association which in
-- turn must be converted into an aggregate.
-- pragma Global (In_Out => (A, B, C))
-- Remove the pragma argument name as this information has been
-- captured in the aggregate.
- Set_Chars (Arg, No_Name);
+ if Nkind (Arg) = N_Pragma_Argument_Association then
+ Set_Chars (Arg, No_Name);
+ end if;
Set_Expression (Arg,
Make_Aggregate (Loc,
-- Get name from corresponding aspect
- Error_Msg_Name_1 := Original_Aspect_Name (N);
+ Error_Msg_Name_1 := Original_Aspect_Pragma_Name (N);
end if;
-- Return possibly modified message
-- Here to start processing for recognized pragma
Prag_Id := Get_Pragma_Id (Pname);
- Pname := Original_Aspect_Name (N);
+ Pname := Original_Aspect_Pragma_Name (N);
-- Capture setting of Opt.Uneval_Old
-- Local variables
- Context : constant Node_Id := Parent (Parent (N));
- Pack_Id : Entity_Id;
- State : Node_Id;
+ Pack_Decl : Node_Id;
+ Pack_Id : Entity_Id;
+ State : Node_Id;
-- Start of processing for Abstract_State
GNAT_Pragma;
Check_No_Identifiers;
Check_Arg_Count (1);
- Ensure_Aggregate_Form (Arg1);
+
+ Pack_Decl := Find_Related_Package_Or_Body (N, Do_Checks => True);
-- Ensure the proper placement of the pragma. Abstract states must
-- be associated with a package declaration.
- if not Nkind_In (Context, N_Generic_Package_Declaration,
- N_Package_Declaration)
+ if Nkind_In (Pack_Decl, N_Generic_Package_Declaration,
+ N_Package_Declaration)
then
+ null;
+
+ -- Otherwise the pragma is associated with an illegal construct
+
+ else
Pragma_Misplaced;
return;
end if;
- State := Expression (Arg1);
- Pack_Id := Defining_Entity (Context);
+ Ensure_Aggregate_Form (Get_Argument (N));
+ Pack_Id := Defining_Entity (Pack_Decl);
-- Mark the associated package as Ghost if it is subject to aspect
-- or pragma Ghost as this affects the declaration of an abstract
Set_Is_Ghost_Entity (Pack_Id);
end if;
+ State := Expression (Get_Argument (N));
+
-- Multiple non-null abstract states appear as an aggregate
if Nkind (State) = N_Aggregate then
when Pragma_Contract_Cases => Contract_Cases : declare
Subp_Decl : Node_Id;
+ Subp_Id : Entity_Id;
begin
GNAT_Pragma;
Check_No_Identifiers;
Check_Arg_Count (1);
- Ensure_Aggregate_Form (Arg1);
-- The pragma is analyzed at the end of the declarative part which
-- contains the related subprogram. Reset the analyzed flag.
Subp_Decl :=
Find_Related_Subprogram_Or_Body (N, Do_Checks => True);
- if Nkind (Subp_Decl) = N_Subprogram_Declaration then
+ -- Generic subprogram
+
+ if Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then
null;
-- Body acts as spec
then
null;
+ -- Subprogram
+
+ elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then
+ null;
+
else
Pragma_Misplaced;
return;
end if;
- -- When the pragma appears on a subprogram body, perform the full
- -- analysis now.
+ Subp_Id := Defining_Entity (Subp_Decl);
- if Nkind (Subp_Decl) = N_Subprogram_Body then
- Analyze_Contract_Cases_In_Decl_Part (N);
+ Ensure_Aggregate_Form (Get_Argument (N, Subp_Id));
- -- When Contract_Cases applies to a subprogram compilation unit,
- -- the corresponding pragma is placed after the unit's declaration
- -- node and needs to be analyzed immediately.
+ -- Construct a generic template for the pragma when the context is
+ -- a generic subprogram and the pragma is a source construct.
- elsif Nkind (Subp_Decl) = N_Subprogram_Declaration
- and then Nkind (Parent (Subp_Decl)) = N_Compilation_Unit
- then
+ Create_Generic_Template (N, Subp_Id);
+
+ -- Fully analyze the pragma when it appears inside a subprogram
+ -- body because it cannot benefit from forward references.
+
+ if Nkind (Subp_Decl) = N_Subprogram_Body then
Analyze_Contract_Cases_In_Decl_Part (N);
end if;
-- Chain the pragma on the contract for further processing
- Add_Contract_Item (N, Defining_Entity (Subp_Decl));
+ Add_Contract_Item (N, Subp_Id);
end Contract_Cases;
----------------
when Pragma_Depends => Depends : declare
Subp_Decl : Node_Id;
+ Subp_Id : Entity_Id;
begin
GNAT_Pragma;
Check_Arg_Count (1);
- Ensure_Aggregate_Form (Arg1);
-- Ensure the proper placement of the pragma. Depends must be
-- associated with a subprogram declaration or a body that acts
Subp_Decl :=
Find_Related_Subprogram_Or_Body (N, Do_Checks => True);
- if Nkind (Subp_Decl) = N_Subprogram_Declaration then
- null;
-
-- Body acts as spec
- elsif Nkind (Subp_Decl) = N_Subprogram_Body
+ if Nkind (Subp_Decl) = N_Subprogram_Body
and then No (Corresponding_Spec (Subp_Decl))
then
null;
then
null;
+ -- Subprogram declaration
+
+ elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then
+ null;
+
else
Pragma_Misplaced;
return;
end if;
+ Subp_Id := Defining_Entity (Subp_Decl);
+
+ Ensure_Aggregate_Form (Get_Argument (N, Subp_Id));
+
+ -- Construct a generic template for the pragma when the context is
+ -- a generic subprogram and the pragma is a source construct.
+
+ Create_Generic_Template (N, Subp_Id);
+
-- When the pragma appears on a subprogram body, perform the full
-- analysis now.
if Nkind (Subp_Decl) = N_Subprogram_Body then
Analyze_Depends_In_Decl_Part (N);
-
- -- When Depends applies to a subprogram compilation unit, the
- -- corresponding pragma is placed after the unit's declaration
- -- node and needs to be analyzed immediately.
-
- elsif Nkind (Subp_Decl) = N_Subprogram_Declaration
- and then Nkind (Parent (Subp_Decl)) = N_Compilation_Unit
- then
- Analyze_Depends_In_Decl_Part (N);
end if;
-- Chain the pragma on the contract for further processing
- Add_Contract_Item (N, Defining_Entity (Subp_Decl));
+ Add_Contract_Item (N, Subp_Id);
end Depends;
---------------------
-- gnatwl/-gnatwE (elaboration warnings enabled) switches set.
if Elab_Warnings
- and not Dynamic_Elaboration_Checks
+ and not Dynamic_Elaboration_Checks
- -- pragma Elaborate not allowed in SPARK mode anyway. We
- -- already complained about it, no point in generating any
- -- further complaint.
+ -- pragma Elaborate not allowed in SPARK mode anyway. We
+ -- already complained about it, no point in generating any
+ -- further complaint.
- and SPARK_Mode /= On
+ and SPARK_Mode /= On
then
Error_Msg_N
("?l?use of pragma Elaborate may not be safe", N);
-- pragma Extensions_Visible [ (boolean_EXPRESSION) ];
when Pragma_Extensions_Visible => Extensions_Visible : declare
- Context : constant Node_Id := Parent (N);
- Expr : Node_Id;
- Formal : Entity_Id;
- Orig_Stmt : Node_Id;
- Subp : Entity_Id;
- Stmt : Node_Id;
-
+ Expr : Node_Id;
+ Formal : Entity_Id;
Has_OK_Formal : Boolean := False;
+ Spec_Id : Entity_Id;
+ Subp_Decl : Node_Id;
+ Subp_Id : Entity_Id;
begin
GNAT_Pragma;
Check_No_Identifiers;
Check_At_Most_N_Arguments (1);
- Subp := Empty;
- 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;
-
- -- Skip internally generated code
-
- elsif not Comes_From_Source (Stmt) then
- Orig_Stmt := Original_Node (Stmt);
+ Subp_Decl :=
+ Find_Related_Subprogram_Or_Body (N, Do_Checks => True);
- -- When pragma Ghost applies to an expression function, the
- -- expression function is transformed into a subprogram.
+ -- Generic subprogram declaration
- if Nkind (Stmt) = N_Subprogram_Declaration
- and then Comes_From_Source (Orig_Stmt)
- and then Nkind (Orig_Stmt) = N_Expression_Function
- then
- Subp := Defining_Entity (Stmt);
- exit;
- end if;
+ if Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then
+ null;
- -- The associated [generic] subprogram declaration has been
- -- found, stop the search.
+ -- Body acts as spec
- elsif Nkind_In (Stmt, N_Generic_Subprogram_Declaration,
- N_Subprogram_Declaration)
- then
- Subp := Defining_Entity (Stmt);
- exit;
+ elsif Nkind (Subp_Decl) = N_Subprogram_Body
+ and then No (Corresponding_Spec (Subp_Decl))
+ then
+ null;
- -- The pragma does not apply to a legal construct, issue an
- -- error and stop the analysis.
+ -- Body stub acts as spec
- else
- Error_Pragma ("pragma % must apply to a subprogram");
- return;
- end if;
+ elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub
+ and then No (Corresponding_Spec_Of_Stub (Subp_Decl))
+ then
+ null;
- Stmt := Prev (Stmt);
- end loop;
+ -- Subprogram declaration
- -- When the pragma applies to a stand alone subprogram body, it
- -- appears within the declarations of the body. In that case the
- -- enclosing construct is the proper context. This check is done
- -- after the traversal above to allow for duplicate detection.
+ elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then
+ null;
- if No (Subp)
- and then Nkind (Context) = N_Subprogram_Body
- and then No (Corresponding_Spec (Context))
- then
- Subp := Defining_Entity (Context);
- end if;
+ -- Otherwise the pragma is associated with an illegal construct
- if No (Subp) then
+ else
Error_Pragma ("pragma % must apply to a subprogram");
return;
end if;
+ Spec_Id := Corresponding_Spec_Of (Subp_Decl);
+ Subp_Id := Defining_Entity (Subp_Decl);
+
-- Examine the formals of the related subprogram
- Formal := First_Formal (Subp);
+ Formal := First_Formal (Spec_Id);
while Present (Formal) loop
-- At least one of the formals is of a specific tagged type,
Error_Msg_N (Fix_Error ("incorrect placement of pragma %"), N);
Error_Msg_NE
("\subprogram & lacks parameter of specific tagged or "
- & "generic private type", N, Subp);
+ & "generic private type", N, Spec_Id);
return;
end if;
+ -- Construct a generic template for the pragma when the context is
+ -- a generic subprogram and the pragma is a source construct.
+
+ Create_Generic_Template (N, Subp_Id);
+
-- Analyze the Boolean expression (if any)
if Present (Arg1) then
- Expr := Get_Pragma_Arg (Arg1);
+ Expr := Expression (Get_Argument (N));
Analyze_And_Resolve (Expr, Standard_Boolean);
-- Chain the pragma on the contract for further processing
- Add_Contract_Item (N, Subp);
+ Add_Contract_Item (N, Subp_Id);
end Extensions_Visible;
--------------
when Pragma_Global => Global : declare
Subp_Decl : Node_Id;
+ Subp_Id : Entity_Id;
begin
GNAT_Pragma;
Check_Arg_Count (1);
- Ensure_Aggregate_Form (Arg1);
-- Ensure the proper placement of the pragma. Global must be
-- associated with a subprogram declaration or a body that acts
Subp_Decl :=
Find_Related_Subprogram_Or_Body (N, Do_Checks => True);
- if Nkind (Subp_Decl) = N_Subprogram_Declaration then
- null;
-
-- Body acts as spec
- elsif Nkind (Subp_Decl) = N_Subprogram_Body
+ if Nkind (Subp_Decl) = N_Subprogram_Body
and then No (Corresponding_Spec (Subp_Decl))
then
null;
then
null;
+ -- Subprogram declaration
+
+ elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then
+ null;
+
else
Pragma_Misplaced;
return;
end if;
+ Subp_Id := Defining_Entity (Subp_Decl);
+
+ Ensure_Aggregate_Form (Get_Argument (N, Subp_Id));
+
+ -- Construct a generic template for the pragma when the context is
+ -- a generic subprogram and the pragma is a source construct.
+
+ Create_Generic_Template (N, Subp_Id);
+
-- When the pragma appears on a subprogram body, perform the full
-- analysis now.
if Nkind (Subp_Decl) = N_Subprogram_Body then
Analyze_Global_In_Decl_Part (N);
-
- -- When Global applies to a subprogram compilation unit, the
- -- corresponding pragma is placed after the unit's declaration
- -- node and needs to be analyzed immediately.
-
- elsif Nkind (Subp_Decl) = N_Subprogram_Declaration
- and then Nkind (Parent (Subp_Decl)) = N_Compilation_Unit
- then
- Analyze_Global_In_Decl_Part (N);
end if;
-- Chain the pragma on the contract for further processing
- Add_Contract_Item (N, Defining_Entity (Subp_Decl));
+ Add_Contract_Item (N, Subp_Id);
end Global;
-----------
-- pragma Initial_Condition (boolean_EXPRESSION);
when Pragma_Initial_Condition => Initial_Condition : declare
- Context : constant Node_Id := Parent (Parent (N));
- Pack_Id : Entity_Id;
- Stmt : Node_Id;
+ Pack_Decl : Node_Id;
+ Pack_Id : Entity_Id;
begin
GNAT_Pragma;
Check_No_Identifiers;
Check_Arg_Count (1);
+ Pack_Decl := Find_Related_Package_Or_Body (N, Do_Checks => True);
+
-- Ensure the proper placement of the pragma. Initial_Condition
-- must be associated with a package declaration.
- if not Nkind_In (Context, N_Generic_Package_Declaration,
- N_Package_Declaration)
+ if Nkind_In (Pack_Decl, N_Generic_Package_Declaration,
+ N_Package_Declaration)
then
+ null;
+
+ -- Otherwise the pragma is associated with an illegal context
+
+ else
Pragma_Misplaced;
return;
end if;
- 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;
-
- -- 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;
-
-- The pragma must be analyzed at the end of the visible
-- declarations of the related package. Save the pragma for later
-- (see Analyze_Initial_Condition_In_Decl_Part) by adding it to
-- the contract of the package.
- Pack_Id := Defining_Entity (Context);
+ Pack_Id := Defining_Entity (Pack_Decl);
Add_Contract_Item (N, Pack_Id);
-- Verify the declaration order of pragma Initial_Condition with
-- INPUT ::= name
when Pragma_Initializes => Initializes : declare
- Context : constant Node_Id := Parent (Parent (N));
- Pack_Id : Entity_Id;
- Stmt : Node_Id;
+ Pack_Decl : Node_Id;
+ Pack_Id : Entity_Id;
begin
GNAT_Pragma;
Check_No_Identifiers;
Check_Arg_Count (1);
- Ensure_Aggregate_Form (Arg1);
+
+ Pack_Decl := Find_Related_Package_Or_Body (N, Do_Checks => True);
-- Ensure the proper placement of the pragma. Initializes must be
-- associated with a package declaration.
- if not Nkind_In (Context, N_Generic_Package_Declaration,
- N_Package_Declaration)
+ if Nkind_In (Pack_Decl, N_Generic_Package_Declaration,
+ N_Package_Declaration)
then
+ null;
+
+ -- Otherwise the pragma is associated with an illegal construc
+
+ else
Pragma_Misplaced;
return;
end if;
- 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;
-
- -- 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;
+ Ensure_Aggregate_Form (Get_Argument (N));
-- The pragma must be analyzed at the end of the visible
-- declarations of the related package. Save the pragma for later
-- (see Analyze_Initializes_In_Decl_Part) by adding it to the
-- contract of the package.
- Pack_Id := Defining_Entity (Context);
+ Pack_Id := Defining_Entity (Pack_Decl);
Add_Contract_Item (N, Pack_Id);
-- Verify the declaration order of pragmas Abstract_State and
Check_Arg_Is_One_Of (Arg1, Name_On, Name_Off);
Polling_Required := (Chars (Get_Pragma_Arg (Arg1)) = Name_On);
- ------------------
- -- Post[_Class] --
- ------------------
+ -----------------------------------
+ -- Post/Post_Class/Postcondition --
+ -----------------------------------
-- pragma Post (Boolean_EXPRESSION);
-- pragma Post_Class (Boolean_EXPRESSION);
-
- when Pragma_Post | Pragma_Post_Class => Post : declare
- PC_Pragma : Node_Id;
-
- begin
- GNAT_Pragma;
- Check_Arg_Count (1);
- Check_No_Identifiers;
- Check_Pre_Post;
-
- -- Rewrite Post[_Class] pragma as Postcondition pragma setting the
- -- flag Class_Present to True for the Post_Class case.
-
- Set_Class_Present (N, Prag_Id = Pragma_Post_Class);
- PC_Pragma := New_Copy (N);
- Set_Pragma_Identifier
- (PC_Pragma, Make_Identifier (Loc, Name_Postcondition));
- Rewrite (N, PC_Pragma);
- Set_Analyzed (N, False);
- Analyze (N);
- end Post;
-
- -------------------
- -- Postcondition --
- -------------------
-
-- pragma Postcondition ([Check =>] Boolean_EXPRESSION
-- [,[Message =>] String_EXPRESSION]);
- when Pragma_Postcondition => Postcondition : declare
- In_Body : Boolean;
-
- begin
- GNAT_Pragma;
- Check_At_Least_N_Arguments (1);
- Check_At_Most_N_Arguments (2);
- Check_Optional_Identifier (Arg1, Name_Check);
-
- -- Verify the proper placement of the pragma. The remainder of the
- -- processing is found in Sem_Ch6/Sem_Ch7.
-
- Check_Precondition_Postcondition (In_Body);
-
- -- When the pragma is a source construct appearing inside a body,
- -- preanalyze the boolean_expression to detect illegal forward
- -- references:
-
- -- procedure P is
- -- pragma Postcondition (X'Old ...);
- -- X : ...
-
- if Comes_From_Source (N) and then In_Body then
- Preanalyze_Spec_Expression (Expression (Arg1), Any_Boolean);
- end if;
- end Postcondition;
+ when Pragma_Post |
+ Pragma_Post_Class |
+ Pragma_Postcondition =>
+ Analyze_Pre_Post_Condition;
- -----------------
- -- Pre[_Class] --
- -----------------
+ --------------------------------
+ -- Pre/Pre_Class/Precondition --
+ --------------------------------
-- pragma Pre (Boolean_EXPRESSION);
-- pragma Pre_Class (Boolean_EXPRESSION);
-
- when Pragma_Pre | Pragma_Pre_Class => Pre : declare
- PC_Pragma : Node_Id;
-
- begin
- GNAT_Pragma;
- Check_Arg_Count (1);
- Check_No_Identifiers;
- Check_Pre_Post;
-
- -- Rewrite Pre[_Class] pragma as Precondition pragma setting the
- -- flag Class_Present to True for the Pre_Class case.
-
- Set_Class_Present (N, Prag_Id = Pragma_Pre_Class);
- PC_Pragma := New_Copy (N);
- Set_Pragma_Identifier
- (PC_Pragma, Make_Identifier (Loc, Name_Precondition));
- Rewrite (N, PC_Pragma);
- Set_Analyzed (N, False);
- Analyze (N);
- end Pre;
-
- ------------------
- -- Precondition --
- ------------------
-
-- pragma Precondition ([Check =>] Boolean_EXPRESSION
-- [,[Message =>] String_EXPRESSION]);
- when Pragma_Precondition => Precondition : declare
- In_Body : Boolean;
-
- begin
- GNAT_Pragma;
- Check_At_Least_N_Arguments (1);
- Check_At_Most_N_Arguments (2);
- Check_Optional_Identifier (Arg1, Name_Check);
- Check_Precondition_Postcondition (In_Body);
-
- -- If in spec, nothing more to do. If in body, then we convert
- -- the pragma to an equivalent pragma Check. That works fine since
- -- pragma Check will analyze the condition in the proper context.
-
- -- The form of the pragma Check is either:
-
- -- pragma Check (Precondition, cond [, msg])
- -- or
- -- pragma Check (Pre, cond [, msg])
-
- -- We use the Pre form if this pragma derived from a Pre aspect.
- -- This is needed to make sure that the right set of Policy
- -- pragmas are checked.
-
- if In_Body then
-
- -- Rewrite as Check pragma
-
- 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))))));
-
- if Arg_Count = 2 then
- Append_To (Pragma_Argument_Associations (N),
- Make_Pragma_Argument_Association (Sloc (Arg2),
- Expression =>
- Relocate_Node (Get_Pragma_Arg (Arg2))));
- end if;
-
- Analyze (N);
- end if;
- end Precondition;
+ when Pragma_Pre |
+ Pragma_Pre_Class |
+ Pragma_Precondition =>
+ Analyze_Pre_Post_Condition;
---------------
-- Predicate --
-- pragma Refined_Post (boolean_EXPRESSION);
when Pragma_Refined_Post => Refined_Post : declare
- Body_Id : Entity_Id;
- Legal : Boolean;
- Result_Seen : Boolean := False;
- Spec_Id : Entity_Id;
+ Body_Id : Entity_Id;
+ Legal : Boolean;
+ Spec_Id : Entity_Id;
begin
Analyze_Refined_Pragma (Spec_Id, Body_Id, Legal);
- -- Analyze the boolean expression as a "spec expression"
+ -- Fully analyze the pragma when it appears inside a subprogram
+ -- body because it cannot benefit from forward references.
if Legal then
- Analyze_Pre_Post_Condition_In_Decl_Part (N, Spec_Id);
-
- -- Verify that the refined postcondition mentions attribute
- -- 'Result and its expression introduces a post-state.
-
- if Warn_On_Suspicious_Contract
- and then Ekind_In (Spec_Id, E_Function, E_Generic_Function)
- then
- Check_Result_And_Post_State (N, Result_Seen);
-
- if not Result_Seen then
- Error_Pragma
- ("pragma % does not mention function result?T?");
- end if;
- end if;
+ Analyze_Pre_Post_Condition_In_Decl_Part (N);
-- Chain the pragma on the contract for easy retrieval
-- CONSTITUENT ::= object_NAME | state_NAME
- when Pragma_Refined_State => Refined_State : declare
- Context : constant Node_Id := Parent (N);
- Spec_Id : Entity_Id;
- Stmt : Node_Id;
-
- begin
- GNAT_Pragma;
- Check_No_Identifiers;
- Check_Arg_Count (1);
-
- -- Ensure the proper placement of the pragma. Refined states must
- -- be associated with a package body.
-
- if Nkind (Context) /= N_Package_Body then
- Pragma_Misplaced;
- return;
- end if;
-
- 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;
+ when Pragma_Refined_State => Refined_State : declare
+ Pack_Decl : Node_Id;
+ Spec_Id : Entity_Id;
- -- Skip internally generated code
+ begin
+ GNAT_Pragma;
+ Check_No_Identifiers;
+ Check_Arg_Count (1);
- elsif not Comes_From_Source (Stmt) then
- null;
+ Pack_Decl := Find_Related_Package_Or_Body (N, Do_Checks => True);
- -- The pragma does not apply to a legal construct, issue an
- -- error and stop the analysis.
+ -- Ensure the proper placement of the pragma. Refined states must
+ -- be associated with a package body.
- else
- Pragma_Misplaced;
- return;
- end if;
+ if Nkind (Pack_Decl) = N_Package_Body then
+ null;
- Stmt := Prev (Stmt);
- end loop;
+ -- Otherwise the pragma is associated with an illegal construct
- Spec_Id := Corresponding_Spec (Context);
+ else
+ Pragma_Misplaced;
+ return;
+ end if;
+
+ Spec_Id := Corresponding_Spec (Pack_Decl);
-- State refinement is allowed only when the corresponding package
-- declaration has non-null pragma Abstract_State. Refinement not
-- The pragma must be analyzed at the end of the declarations as
-- it has visibility over the whole declarative region. Save the
- -- pragma for later (see Analyze_Refined_Depends_In_Decl_Part) by
+ -- pragma for later (see Analyze_Refined_State_In_Decl_Part) by
-- adding it to the contract of the package body.
- Add_Contract_Item (N, Defining_Entity (Context));
+ Add_Contract_Item (N, Defining_Entity (Pack_Decl));
end Refined_State;
-----------------------
-- MODE_TYPE ::= Nominal | Robustness
- when Pragma_Test_Case =>
+ when Pragma_Test_Case => Test_Case : declare
+ procedure Check_Distinct_Name (Subp_Id : Entity_Id);
+ -- Ensure that the contract of subprogram Subp_Id does not contain
+ -- another Test_Case pragma with the same Name as the current one.
+
+ -------------------------
+ -- Check_Distinct_Name --
+ -------------------------
+
+ procedure Check_Distinct_Name (Subp_Id : Entity_Id) is
+ Items : constant Node_Id := Contract (Subp_Id);
+ Name : constant String_Id := Get_Name_From_CTC_Pragma (N);
+ Prag : Node_Id;
+
+ begin
+ -- Inspect all Test_Case pragma of the related subprogram
+ -- looking for one with a duplicate "Name" argument.
+
+ if Present (Items) then
+ Prag := Contract_Test_Cases (Items);
+ while Present (Prag) loop
+ if Pragma_Name (Prag) = Name_Test_Case
+ and then String_Equal
+ (Name, Get_Name_From_CTC_Pragma (Prag))
+ then
+ Error_Msg_Sloc := Sloc (Prag);
+ Error_Pragma ("name for pragma % is already used #");
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end if;
+ end Check_Distinct_Name;
+
+ -- Local variables
+
+ Pack_Decl : constant Node_Id := Unit (Cunit (Current_Sem_Unit));
+ Asp_Arg : Node_Id;
+ Context : Node_Id;
+ Subp_Decl : Node_Id;
+ Subp_Id : Entity_Id;
+
+ -- Start of processing for Test_Case
+
+ begin
GNAT_Pragma;
- Check_Test_Case;
+ Check_At_Least_N_Arguments (2);
+ Check_At_Most_N_Arguments (4);
+ Check_Arg_Order
+ ((Name_Name, Name_Mode, Name_Requires, Name_Ensures));
+
+ -- Argument "Name"
+
+ Check_Optional_Identifier (Arg1, Name_Name);
+ Check_Arg_Is_OK_Static_Expression (Arg1, Standard_String);
+
+ -- Argument "Mode"
+
+ Check_Optional_Identifier (Arg2, Name_Mode);
+ Check_Arg_Is_One_Of (Arg2, Name_Nominal, Name_Robustness);
+
+ -- Arguments "Requires" and "Ensures"
+
+ if Present (Arg3) then
+ if Present (Arg4) then
+ Check_Identifier (Arg3, Name_Requires);
+ Check_Identifier (Arg4, Name_Ensures);
+ else
+ Check_Identifier_Is_One_Of
+ (Arg3, Name_Requires, Name_Ensures);
+ end if;
+ end if;
+
+ -- Pragma Test_Case must be associated with a subprogram declared
+ -- in a library-level package. First determine whether the current
+ -- compilation unit is a legal context.
+
+ if Nkind_In (Pack_Decl, N_Package_Declaration,
+ N_Generic_Package_Declaration)
+ then
+ null;
+
+ -- Otherwise the placement is illegal
+
+ else
+ Pragma_Misplaced;
+ return;
+ end if;
+
+ Subp_Decl := Find_Related_Subprogram_Or_Body (N);
+
+ -- Find the enclosing context
+
+ Context := Parent (Subp_Decl);
+
+ if Present (Context) then
+ Context := Parent (Context);
+ end if;
+
+ -- Verify the placement of the pragma
+
+ if Nkind (Subp_Decl) = N_Abstract_Subprogram_Declaration then
+ Error_Pragma
+ ("pragma % cannot be applied to abstract subprogram");
+ return;
+
+ elsif Nkind (Subp_Decl) = N_Entry_Declaration then
+ Error_Pragma ("pragma % cannot be applied to entry");
+ return;
+
+ -- The context is a [generic] subprogram declared at the top level
+ -- of the [generic] package unit.
+
+ elsif Nkind_In (Subp_Decl, N_Generic_Subprogram_Declaration,
+ N_Subprogram_Declaration)
+ and then Present (Context)
+ and then Nkind_In (Context, N_Generic_Package_Declaration,
+ N_Package_Declaration)
+ then
+ Subp_Id := Defining_Entity (Subp_Decl);
+
+ -- Otherwise the placement is illegal
+
+ else
+ Pragma_Misplaced;
+ return;
+ end if;
+
+ -- Preanalyze the original aspect argument "Name" for ASIS or for
+ -- a generic subprogram to properly capture global references.
+
+ if ASIS_Mode or else Is_Generic_Subprogram (Subp_Id) then
+ Asp_Arg := Test_Case_Arg (N, Name_Name, From_Aspect => True);
+
+ if Present (Asp_Arg) then
+
+ -- The argument appears with an identifier in association
+ -- form.
+
+ if Nkind (Asp_Arg) = N_Component_Association then
+ Asp_Arg := Expression (Asp_Arg);
+ end if;
+
+ Check_Expr_Is_OK_Static_Expression
+ (Asp_Arg, Standard_String);
+ end if;
+ end if;
+
+ -- Ensure that the all Test_Case pragmas of the related subprogram
+ -- have distinct names.
+
+ Check_Distinct_Name (Subp_Id);
+
+ -- Construct a generic template for the pragma when the context is
+ -- a generic subprogram and the pragma is a source construct.
+
+ Create_Generic_Template (N, Subp_Id);
+
+ -- Fully analyze the pragma when it appears inside a subprogram
+ -- body because it cannot benefit from forward references.
+
+ if Nkind_In (Subp_Decl, N_Subprogram_Body,
+ N_Subprogram_Body_Stub)
+ then
+ Analyze_Test_Case_In_Decl_Part (N);
+ end if;
+
+ -- Chain the pragma on the contract for further processing
+
+ Add_Contract_Item (N, Subp_Id);
+ end Test_Case;
--------------------------
-- Thread_Local_Storage --
raise Program_Error;
end if;
- Rewrite (N, Make_Pragma (Loc,
- Chars => Name_Warnings,
- Pragma_Argument_Associations => Shifted_Args));
+ Rewrite (N,
+ Make_Pragma (Loc,
+ Chars => Name_Warnings,
+ Pragma_Argument_Associations => Shifted_Args));
Analyze (N);
raise Pragma_Exit;
end if;
-- Analyze_Pre_Post_Condition_In_Decl_Part --
---------------------------------------------
- procedure Analyze_Pre_Post_Condition_In_Decl_Part
- (Prag : Node_Id;
- Subp_Id : Entity_Id)
- is
- Arg1 : constant Node_Id := First (Pragma_Argument_Associations (Prag));
- Nam : constant Name_Id := Original_Aspect_Name (Prag);
- Expr : Node_Id;
+ procedure Analyze_Pre_Post_Condition_In_Decl_Part (N : Node_Id) is
+ procedure Process_Class_Wide_Condition
+ (Expr : Node_Id;
+ Spec_Id : Entity_Id;
+ Subp_Decl : Node_Id);
+ -- Replace the type of all references to the controlling formal of
+ -- subprogram Spec_Id found in expression Expr with the corresponding
+ -- class-wide type. Subp_Decl is the subprogram [body] declaration
+ -- where the pragma resides.
- Restore_Scope : Boolean := False;
- -- Gets set True if we do a Push_Scope needing a Pop_Scope on exit
+ ----------------------------------
+ -- Process_Class_Wide_Condition --
+ ----------------------------------
- begin
- -- Ensure that the subprogram and its formals are visible when analyzing
- -- the expression of the pragma.
+ procedure Process_Class_Wide_Condition
+ (Expr : Node_Id;
+ Spec_Id : Entity_Id;
+ Subp_Decl : Node_Id)
+ is
+ Disp_Typ : constant Entity_Id := Find_Dispatching_Type (Spec_Id);
+
+ ACW : Entity_Id := Empty;
+ -- Access to Disp_Typ'Class, created if there is a controlling formal
+ -- that is an access parameter.
+
+ function Access_Class_Wide_Type return Entity_Id;
+ -- If expression Expr contains a reference to a controlling access
+ -- parameter, create an access to Disp_Typ'Class for the necessary
+ -- conversions if one does not exist.
+
+ function Replace_Type (N : Node_Id) return Traverse_Result;
+ -- ARM 6.1.1: Within the expression for a Pre'Class or Post'Class
+ -- aspect for a primitive subprogram of a tagged type Disp_Typ, a
+ -- name that denotes a formal parameter of type Disp_Typ is treated
+ -- as having type Disp_Typ'Class. Similarly, a name that denotes a
+ -- formal access parameter of type access-to-Disp_Typ is interpreted
+ -- as with type access-to-Disp_Typ'Class. This ensures the expression
+ -- is well defined for a primitive subprogram of a type descended
+ -- from Disp_Typ.
- if not In_Open_Scopes (Subp_Id) then
- Restore_Scope := True;
- Push_Scope (Subp_Id);
- Install_Formals (Subp_Id);
- end if;
+ ----------------------------
+ -- Access_Class_Wide_Type --
+ ----------------------------
- -- Preanalyze the boolean expression, we treat this as a spec expression
- -- (i.e. similar to a default expression).
+ function Access_Class_Wide_Type return Entity_Id is
+ Loc : constant Source_Ptr := Sloc (N);
- Expr := Get_Pragma_Arg (Arg1);
+ begin
+ if No (ACW) then
+ ACW := Make_Temporary (Loc, 'T');
- -- In ASIS mode, for a pragma generated from a source aspect, analyze
- -- the original aspect expression, which is shared with the generated
- -- pragma.
+ Insert_Before_And_Analyze (Subp_Decl,
+ Make_Full_Type_Declaration (Loc,
+ Defining_Identifier => ACW,
+ Type_Definition =>
+ Make_Access_To_Object_Definition (Loc,
+ Subtype_Indication =>
+ New_Occurrence_Of (Class_Wide_Type (Disp_Typ), Loc),
+ All_Present => True)));
- if ASIS_Mode and then Present (Corresponding_Aspect (Prag)) then
- Expr := Expression (Corresponding_Aspect (Prag));
- end if;
+ Freeze_Before (Subp_Decl, ACW);
+ end if;
- Preanalyze_Assert_Expression (Expr, Standard_Boolean);
+ return ACW;
+ end Access_Class_Wide_Type;
- -- For a class-wide condition, a reference to a controlling formal must
- -- be interpreted as having the class-wide type (or an access to such)
- -- so that the inherited condition can be properly applied to any
- -- overriding operation (see ARM12 6.6.1 (7)).
+ ------------------
+ -- Replace_Type --
+ ------------------
- if Class_Present (Prag) then
- Class_Wide_Condition : declare
- T : constant Entity_Id := Find_Dispatching_Type (Subp_Id);
-
- ACW : Entity_Id := Empty;
- -- Access to T'class, created if there is a controlling formal
- -- that is an access parameter.
-
- function Get_ACW return Entity_Id;
- -- If the expression has a reference to an controlling access
- -- parameter, create an access to T'class for the necessary
- -- conversions if one does not exist.
-
- function Process (N : Node_Id) return Traverse_Result;
- -- ARM 6.1.1: Within the expression for a Pre'Class or Post'Class
- -- aspect for a primitive subprogram of a tagged type T, a name
- -- that denotes a formal parameter of type T is interpreted as
- -- having type T'Class. Similarly, a name that denotes a formal
- -- accessparameter of type access-to-T is interpreted as having
- -- type access-to-T'Class. This ensures the expression is well-
- -- defined for a primitive subprogram of a type descended from T.
- -- Note that this replacement is not done for selector names in
- -- parameter associations. These carry an entity for reference
- -- purposes, but semantically they are just identifiers.
-
- -------------
- -- Get_ACW --
- -------------
-
- function Get_ACW return Entity_Id is
- Loc : constant Source_Ptr := Sloc (Prag);
- Decl : Node_Id;
+ function Replace_Type (N : Node_Id) return Traverse_Result is
+ Context : constant Node_Id := Parent (N);
+ Loc : constant Source_Ptr := Sloc (N);
+ CW_Typ : Entity_Id := Empty;
+ Ent : Entity_Id;
+ Typ : Entity_Id;
- begin
- if No (ACW) then
- Decl :=
- Make_Full_Type_Declaration (Loc,
- Defining_Identifier => Make_Temporary (Loc, 'T'),
- Type_Definition =>
- Make_Access_To_Object_Definition (Loc,
- Subtype_Indication =>
- New_Occurrence_Of (Class_Wide_Type (T), Loc),
- All_Present => True));
+ begin
+ if Is_Entity_Name (N)
+ and then Present (Entity (N))
+ and then Is_Formal (Entity (N))
+ then
+ Ent := Entity (N);
+ Typ := Etype (Ent);
- Insert_Before (Unit_Declaration_Node (Subp_Id), Decl);
- Analyze (Decl);
- ACW := Defining_Identifier (Decl);
- Freeze_Before (Unit_Declaration_Node (Subp_Id), ACW);
- end if;
+ -- Do not perform the type replacement for selector names in
+ -- parameter associations. These carry an entity for reference
+ -- purposes, but semantically they are just identifiers.
- return ACW;
- end Get_ACW;
+ if Nkind (Context) = N_Type_Conversion then
+ null;
- -------------
- -- Process --
- -------------
+ elsif Nkind (Context) = N_Parameter_Association
+ and then Selector_Name (Context) = N
+ then
+ null;
- function Process (N : Node_Id) return Traverse_Result is
- Loc : constant Source_Ptr := Sloc (N);
- Typ : Entity_Id;
+ elsif Typ = Disp_Typ then
+ CW_Typ := Class_Wide_Type (Typ);
- begin
- if Is_Entity_Name (N)
- and then Present (Entity (N))
- and then Is_Formal (Entity (N))
- and then Nkind (Parent (N)) /= N_Type_Conversion
- and then
- (Nkind (Parent (N)) /= N_Parameter_Association
- or else N /= Selector_Name (Parent (N)))
+ elsif Is_Access_Type (Typ)
+ and then Designated_Type (Typ) = Disp_Typ
then
- if Etype (Entity (N)) = T then
- Typ := Class_Wide_Type (T);
-
- elsif Is_Access_Type (Etype (Entity (N)))
- and then Designated_Type (Etype (Entity (N))) = T
- then
- Typ := Get_ACW;
- else
- Typ := Empty;
- end if;
+ CW_Typ := Access_Class_Wide_Type;
+ end if;
- if Present (Typ) then
- Rewrite (N,
- Make_Type_Conversion (Loc,
- Subtype_Mark =>
- New_Occurrence_Of (Typ, Loc),
- Expression => New_Occurrence_Of (Entity (N), Loc)));
- Set_Etype (N, Typ);
- end if;
+ if Present (CW_Typ) then
+ Rewrite (N,
+ Make_Type_Conversion (Loc,
+ Subtype_Mark => New_Occurrence_Of (CW_Typ, Loc),
+ Expression => New_Occurrence_Of (Ent, Loc)));
+ Set_Etype (N, CW_Typ);
end if;
+ end if;
- return OK;
- end Process;
+ return OK;
+ end Replace_Type;
- procedure Replace_Type is new Traverse_Proc (Process);
+ procedure Replace_Types is new Traverse_Proc (Replace_Type);
- -- Start of processing for Class_Wide_Condition
+ -- Local variables
- begin
- if not Present (T) then
+ Prag_Nam : constant Name_Id := Original_Aspect_Pragma_Name (N);
- -- Pre'Class/Post'Class aspect cases
+ -- Start of processing for Process_Class_Wide_Condition
- if From_Aspect_Specification (Prag) then
- Error_Msg_Name_1 := Nam;
- Error_Msg_N
- ("aspect% can only be specified for a primitive "
- & "operation of a tagged type",
- Corresponding_Aspect (Prag));
+ begin
+ -- The subprogram subject to Pre'Class/Post'Class does not have a
+ -- dispatching type, therefore the aspect/pragma is illegal.
- -- Pre_Class, Post_Class pragma cases
+ if No (Disp_Typ) then
+ if From_Aspect_Specification (N) then
+ Error_Msg_Name_1 := Prag_Nam;
+ Error_Msg_N
+ ("aspect % can only be specified for a primitive operation "
+ & "of a tagged type", Corresponding_Aspect (N));
- else
- if Nam = Name_uPre then
- Error_Msg_Name_1 := Name_Pre_Class;
- else
- Error_Msg_Name_1 := Name_Post_Class;
- end if;
+ -- The pragma is a source construct
- Error_Msg_N
- ("pragma% can only be specified for a primitive "
- & "operation of a tagged type",
- Corresponding_Aspect (Prag));
+ else
+ if Prag_Nam = Name_Precondition then
+ Error_Msg_Name_1 := Name_Pre_Class;
+ else
+ Error_Msg_Name_1 := Name_Post_Class;
end if;
+
+ Error_Msg_N
+ ("pragma % can only be specified for a primitive operation "
+ & "of a tagged type", N);
end if;
+ end if;
+
+ Replace_Types (Expr);
+ end Process_Class_Wide_Condition;
+
+ -- Local variables
+
+ Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
+ Expr : constant Node_Id :=
+ Expression (Get_Argument (N, Defining_Entity (Subp_Decl)));
+ Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl);
+
+ Restore_Scope : Boolean := False;
+ -- Gets set True if we do a Push_Scope needing a Pop_Scope on exit
+
+ -- Start of processing for Analyze_Pre_Post_Condition_In_Decl_Part
+
+ begin
+ -- 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;
+ 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;
+
+ Preanalyze_Assert_Expression (Expr, Standard_Boolean);
+
+ -- For a class-wide condition, a reference to a controlling formal must
+ -- be interpreted as having the class-wide type (or an access to such)
+ -- so that the inherited condition can be properly applied to any
+ -- overriding operation (see ARM12 6.6.1 (7)).
- Replace_Type (Get_Pragma_Arg (Arg1));
- end Class_Wide_Condition;
+ if Class_Present (N) then
+ Process_Class_Wide_Condition (Expr, Spec_Id, Subp_Decl);
end if;
-- Remove the subprogram from the scope stack now that the pre-analysis
Body_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
Body_Id : constant Entity_Id := Defining_Entity (Body_Decl);
Errors : constant Nat := Serious_Errors_Detected;
- Refs : constant Node_Id :=
- Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
+ Refs : constant Node_Id := Expression (Get_Argument (N));
Clause : Node_Id;
Deps : Node_Id;
Dummy : Boolean;
return;
end if;
- Deps := Get_Pragma_Arg (First (Pragma_Argument_Associations (Depends)));
+ Deps := Expression (Get_Argument (Depends));
-- A null dependency relation renders the refinement useless because it
-- cannot possibly mention abstract states with visible refinement. Note
-- Start of processing for Collect_Global_Items
begin
- Process_Global_List
- (Get_Pragma_Arg (First (Pragma_Argument_Associations (Prag))));
+ Process_Global_List (Expression (Get_Argument (Prag)));
end Collect_Global_Items;
-------------------------
Body_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
Errors : constant Nat := Serious_Errors_Detected;
- Items : constant Node_Id :=
- Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
+ Items : constant Node_Id := Expression (Get_Argument (N));
Spec_Id : Entity_Id;
-- Start of processing for Analyze_Refined_Global_In_Decl_Part
-- Local declarations
Body_Decl : constant Node_Id := Parent (N);
- Clauses : constant Node_Id :=
- Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
+ Clauses : constant Node_Id := Expression (Get_Argument (N));
Clause : Node_Id;
-- Start of processing for Analyze_Refined_State_In_Decl_Part
-- Analyze_Test_Case_In_Decl_Part --
------------------------------------
- procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id; S : Entity_Id) is
+ procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id) is
+ procedure Preanalyze_Test_Case_Arg
+ (Arg_Nam : Name_Id;
+ Subp_Id : Entity_Id);
+ -- Preanalyze one of the optional arguments "Requires" or "Ensures"
+ -- denoted by Arg_Nam. Subp_Id is the entity of the subprogram subject
+ -- to pragma Test_Case.
+
+ ------------------------------
+ -- Preanalyze_Test_Case_Arg --
+ ------------------------------
+
+ procedure Preanalyze_Test_Case_Arg
+ (Arg_Nam : Name_Id;
+ Subp_Id : Entity_Id)
+ is
+ Arg : Node_Id;
+
+ begin
+ -- Preanalyze the original aspect argument for ASIS or for a generic
+ -- subprogram to properly capture global references.
+
+ if ASIS_Mode or else Is_Generic_Subprogram (Subp_Id) then
+ Arg :=
+ Test_Case_Arg
+ (Prag => N,
+ Arg_Nam => Arg_Nam,
+ From_Aspect => True);
+
+ if Present (Arg) then
+ Preanalyze_Assert_Expression
+ (Expression (Arg), Standard_Boolean);
+ end if;
+ end if;
+
+ Arg := Test_Case_Arg (N, Arg_Nam);
+
+ if Present (Arg) then
+ Preanalyze_Assert_Expression (Expression (Arg), Standard_Boolean);
+ end if;
+ end Preanalyze_Test_Case_Arg;
+
+ -- Local variables
+
+ Subp_Decl : Node_Id;
+ Subp_Id : Entity_Id;
+
+ Restore_Scope : Boolean := False;
+ -- Gets set True if we do a Push_Scope needing a Pop_Scope on exit
+
+ -- Start of processing for Analyze_Test_Case_In_Decl_Part
+
begin
- -- Install formals and push subprogram spec onto scope stack so that we
- -- can see the formals from the pragma.
+ Subp_Decl := Find_Related_Subprogram_Or_Body (N);
+ Subp_Id := Defining_Entity (Subp_Decl);
- Push_Scope (S);
- Install_Formals (S);
+ -- Ensure that the formal parameters are visible when analyzing all
+ -- clauses. This falls out of the general rule of aspects pertaining
+ -- to subprogram declarations.
- -- Preanalyze the boolean expressions, we treat these as spec
- -- expressions (i.e. similar to a default expression).
+ if not In_Open_Scopes (Subp_Id) then
+ Restore_Scope := True;
+ Push_Scope (Subp_Id);
- if Pragma_Name (N) = Name_Test_Case then
- Preanalyze_CTC_Args
- (N,
- Get_Requires_From_CTC_Pragma (N),
- Get_Ensures_From_CTC_Pragma (N));
+ if Is_Generic_Subprogram (Subp_Id) then
+ Install_Generic_Formals (Subp_Id);
+ else
+ Install_Formals (Subp_Id);
+ end if;
end if;
- -- Remove the subprogram from the scope stack now that the pre-analysis
- -- of the expressions in the contract case or test case is done.
+ Preanalyze_Test_Case_Arg (Name_Requires, Subp_Id);
+ Preanalyze_Test_Case_Arg (Name_Ensures, Subp_Id);
- End_Scope;
+ if Restore_Scope then
+ End_Scope;
+ end if;
end Analyze_Test_Case_In_Decl_Part;
----------------
PP : Node_Id;
Policy : Name_Id;
- Ename : constant Name_Id := Original_Aspect_Name (N);
+ Ename : constant Name_Id := Original_Aspect_Pragma_Name (N);
begin
-- No effect if not valid assertion kind name
and then Is_Generic_Instance (Pack_Id)
and then not Has_Visible_State (Pack_Id)
then
- null;
-
- -- All other cases require Part_Of
-
- else
- Error_Msg_N
- ("indicator Part_Of is required in this context "
- & "(SPARK RM 7.2.6(2))", Item_Id);
- Error_Msg_Name_1 := Chars (Pack_Id);
- Error_Msg_N
- ("\& is declared in the private part of package %", Item_Id);
- end if;
- end if;
- end Check_Missing_Part_Of;
-
- ---------------------------------
- -- Check_SPARK_Aspect_For_ASIS --
- ---------------------------------
-
- procedure Check_SPARK_Aspect_For_ASIS (N : Node_Id) is
- Expr : Node_Id;
-
- begin
- if ASIS_Mode and then From_Aspect_Specification (N) then
- Expr := Expression (Corresponding_Aspect (N));
- if Nkind (Expr) /= N_Aggregate then
- Preanalyze_And_Resolve (Expr);
-
- else
- declare
- Comps : constant List_Id := Component_Associations (Expr);
- Exprs : constant List_Id := Expressions (Expr);
- C : Node_Id;
- E : Node_Id;
+ null;
- begin
- E := First (Exprs);
- while Present (E) loop
- Analyze (E);
- Next (E);
- end loop;
+ -- All other cases require Part_Of
- C := First (Comps);
- while Present (C) loop
- Analyze (Expression (C));
- Next (C);
- end loop;
- end;
+ else
+ Error_Msg_N
+ ("indicator Part_Of is required in this context "
+ & "(SPARK RM 7.2.6(2))", Item_Id);
+ Error_Msg_Name_1 := Chars (Pack_Id);
+ Error_Msg_N
+ ("\& is declared in the private part of package %", Item_Id);
end if;
end if;
- end Check_SPARK_Aspect_For_ASIS;
+ end Check_Missing_Part_Of;
-------------------------------------
-- Check_State_And_Constituent_Use --
-- Local variables
- Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
+ Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
+ Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl);
Clause : Node_Id;
Clauses : Node_Id;
Depends : Node_Id;
Formal : Entity_Id;
Global : Node_Id;
List : Node_Id;
- Spec_Id : Entity_Id;
-- Start of processing for Collect_Subprogram_Inputs_Outputs
begin
Global_Seen := False;
- -- Find the entity of the corresponding spec when processing a body
-
- if Nkind (Subp_Decl) = N_Subprogram_Body
- and then Present (Corresponding_Spec (Subp_Decl))
- then
- Spec_Id := Corresponding_Spec (Subp_Decl);
-
- elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub
- and then Present (Corresponding_Spec_Of_Stub (Subp_Decl))
- then
- Spec_Id := Corresponding_Spec_Of_Stub (Subp_Decl);
-
- else
- Spec_Id := Subp_Id;
- end if;
-
-- Process all formal parameters
Formal := First_Formal (Spec_Id);
if Present (Global) then
Global_Seen := True;
- List := Expression (First (Pragma_Argument_Associations (Global)));
+ List := Expression (Get_Argument (Global, Spec_Id));
-- The pragma may not have been analyzed because of the arbitrary
-- declaration order of aspects. Make sure that it is analyzed for
-- the inputs and outputs from [Refined_]Depends.
elsif Synthesize and then Present (Depends) then
- Clauses :=
- Get_Pragma_Arg (First (Pragma_Argument_Associations (Depends)));
+ Clauses := Expression (Get_Argument (Depends, Spec_Id));
-- Multiple dependency clauses appear as an aggregate
Name_Priority_Specific_Dispatching);
end Delay_Config_Pragma_Analyze;
+ -----------------------
+ -- Duplication_Error --
+ -----------------------
+
+ procedure Duplication_Error (Prag : Node_Id; Prev : Node_Id) is
+ Prag_From_Asp : constant Boolean := From_Aspect_Specification (Prag);
+ Prag_Nam : constant Name_Id := Original_Aspect_Pragma_Name (Prag);
+ Prev_From_Asp : constant Boolean := From_Aspect_Specification (Prev);
+
+ begin
+ Error_Msg_Sloc := Sloc (Prev);
+
+ -- Emit a precise message to distinguish between source pragmas and
+ -- pragmas generated from aspects. The ordering of the two pragmas is
+ -- the following:
+
+ -- Prev -- ok
+ -- Prag -- duplicate
+
+ -- No error is emitted when both pragmas come from aspects because this
+ -- is already detected by the general aspect analysis mechanism.
+
+ if Prag_Nam = Name_uPre then
+ Error_Msg_Name_1 := Name_Pre;
+ elsif Prag_Nam = Name_uPost then
+ Error_Msg_Name_1 := Name_Post;
+ else
+ Error_Msg_Name_1 := Prag_Nam;
+ end if;
+
+ -- The item appears as aspect XXX'Class or pragma XXX_Class
+
+ if Class_Present (Prag) then
+ if Prag_From_Asp and Prev_From_Asp then
+ null;
+ elsif Prag_From_Asp then
+ Error_Msg_N
+ ("aspect `%'Class` duplicates pragma declared #", Prag);
+ elsif Prev_From_Asp then
+ Error_Msg_N
+ ("pragma `%_Class` duplicates aspect declared #", Prag);
+ else
+ Error_Msg_N
+ ("pragma `%_Class` duplicates pragma declared #", Prag);
+ end if;
+
+ -- Otherwise the pragma appears in its normal form
+
+ else
+ if Prag_From_Asp and Prev_From_Asp then
+ null;
+ elsif Prag_From_Asp then
+ Error_Msg_N ("aspect % duplicates pragma declared #", Prag);
+ elsif Prev_From_Asp then
+ Error_Msg_N ("pragma % duplicates aspect declared #", Prag);
+ else
+ Error_Msg_N ("pragma % duplicates pragma declared #", Prag);
+ end if;
+ end if;
+ end Duplication_Error;
+
+ ----------------------------------
+ -- Find_Related_Package_Or_Body --
+ ----------------------------------
+
+ function Find_Related_Package_Or_Body
+ (Prag : Node_Id;
+ Do_Checks : Boolean := False) return Node_Id
+ is
+ Context : constant Node_Id := Parent (Prag);
+ Prag_Nam : constant Name_Id := Pragma_Name (Prag);
+ Stmt : Node_Id;
+
+ begin
+ Stmt := Prev (Prag);
+ while Present (Stmt) loop
+
+ -- Skip prior pragmas, but check for duplicates
+
+ if Nkind (Stmt) = N_Pragma then
+ if Do_Checks and then Pragma_Name (Stmt) = Prag_Nam then
+ Duplication_Error
+ (Prag => Prag,
+ Prev => Stmt);
+ end if;
+
+ -- Skip internally generated code
+
+ elsif not Comes_From_Source (Stmt) then
+ if Nkind (Stmt) = N_Subprogram_Declaration then
+
+ -- The subprogram declaration is an internally generated spec
+ -- for an expression function.
+
+ if Nkind (Original_Node (Stmt)) = N_Expression_Function then
+ return Stmt;
+
+ -- The subprogram is actually an instance housed within an
+ -- anonymous wrapper package.
+
+ elsif Present (Generic_Parent (Specification (Stmt))) then
+ return Stmt;
+ end if;
+ end if;
+
+ -- Return the current source construct which is illegal
+
+ else
+ return Stmt;
+ end if;
+
+ Prev (Stmt);
+ end loop;
+
+ -- If we fall through, then the pragma was either the first declaration
+ -- or it was preceded by other pragmas and no source constructs.
+
+ -- The pragma is associated with a package. The immediate context in
+ -- this case is the specification of the package.
+
+ if Nkind (Context) = N_Package_Specification then
+ return Parent (Context);
+
+ -- The pragma appears in the declarations of a package body
+
+ elsif Nkind (Context) = N_Package_Body then
+ return Context;
+
+ -- The pragma appears in the statements of a package body
+
+ elsif Nkind (Context) = N_Handled_Sequence_Of_Statements
+ and then Nkind (Parent (Context)) = N_Package_Body
+ then
+ return Parent (Context);
+
+ -- The pragma is a byproduct of aspect expansion, return the related
+ -- context of the original aspect. This case has a lower priority as
+ -- the above circuitry pinpoints precisely the related context.
+
+ elsif Present (Corresponding_Aspect (Prag)) then
+ return Parent (Corresponding_Aspect (Prag));
+
+ -- No candidate packge [body] found
+
+ else
+ return Empty;
+ end if;
+ end Find_Related_Package_Or_Body;
+
-------------------------------------
-- Find_Related_Subprogram_Or_Body --
-------------------------------------
(Prag : Node_Id;
Do_Checks : Boolean := False) return Node_Id
is
- Context : constant Node_Id := Parent (Prag);
- Nam : constant Name_Id := Pragma_Name (Prag);
- Stmt : Node_Id;
+ Prag_Nam : constant Name_Id := Original_Aspect_Pragma_Name (Prag);
- Look_For_Body : constant Boolean :=
- Nam_In (Nam, Name_Refined_Depends,
- Name_Refined_Global,
- Name_Refined_Post);
- -- Refinement pragmas must be associated with a subprogram body [stub]
+ procedure Expression_Function_Error;
+ -- Emit an error concerning pragma Prag that illegaly applies to an
+ -- expression function.
- begin
- pragma Assert (Nkind (Prag) = N_Pragma);
+ -------------------------------
+ -- Expression_Function_Error --
+ -------------------------------
+
+ procedure Expression_Function_Error is
+ begin
+ Error_Msg_Name_1 := Prag_Nam;
- -- If the pragma is a byproduct of aspect expansion, return the related
- -- context of the original aspect.
+ -- Emit a precise message to distinguish between source pragmas and
+ -- pragmas generated from aspects.
- if Present (Corresponding_Aspect (Prag)) then
- return Parent (Corresponding_Aspect (Prag));
- end if;
+ if From_Aspect_Specification (Prag) then
+ Error_Msg_N
+ ("aspect % cannot apply to a stand alone expression function",
+ Prag);
+ else
+ Error_Msg_N
+ ("pragma % cannot apply to a stand alone expression function",
+ Prag);
+ end if;
+ end Expression_Function_Error;
+
+ -- Local variables
- -- Otherwise the pragma is a source construct, most likely part of a
- -- declarative list. Skip preceding declarations while looking for a
- -- proper subprogram declaration.
+ Context : constant Node_Id := Parent (Prag);
+ Stmt : Node_Id;
+
+ Look_For_Body : constant Boolean :=
+ Nam_In (Prag_Nam, Name_Refined_Depends,
+ Name_Refined_Global,
+ Name_Refined_Post);
+ -- Refinement pragmas must be associated with a subprogram body [stub]
- pragma Assert (Is_List_Member (Prag));
+ -- Start of processing for Find_Related_Subprogram_Or_Body
+ begin
Stmt := Prev (Prag);
while Present (Stmt) loop
- -- Skip prior pragmas, but check for duplicates
+ -- Skip prior pragmas, but check for duplicates. Pragmas produced
+ -- by splitting a complex pre/postcondition are not considered to
+ -- be duplicates.
if Nkind (Stmt) = N_Pragma then
- if Do_Checks and then Pragma_Name (Stmt) = Nam then
- Error_Msg_Name_1 := Nam;
- Error_Msg_Sloc := Sloc (Stmt);
- Error_Msg_N ("pragma % duplicates pragma declared #", Prag);
+ if Do_Checks
+ and then not Split_PPC (Stmt)
+ and then Original_Aspect_Pragma_Name (Stmt) = Prag_Nam
+ then
+ Duplication_Error
+ (Prag => Prag,
+ Prev => Stmt);
end if;
-- Emit an error when a refinement pragma appears on an expression
and then Nkind (Original_Node (Stmt)) = N_Expression_Function
and then not Has_Completion (Defining_Entity (Stmt))
then
- Error_Msg_Name_1 := Nam;
- Error_Msg_N
- ("pragma % cannot apply to a stand alone expression function",
- Prag);
-
+ Expression_Function_Error;
return Empty;
-- The refinement pragma applies to a subprogram body stub
-- Skip internally generated code
elsif not Comes_From_Source (Stmt) then
- null;
+ if Nkind (Stmt) = N_Subprogram_Declaration then
+
+ -- The subprogram declaration is an internally generated spec
+ -- for an expression function.
+
+ if Nkind (Original_Node (Stmt)) = N_Expression_Function then
+ return Stmt;
+
+ -- The subprogram is actually an instance housed within an
+ -- anonymous wrapper package.
+
+ elsif Present (Generic_Parent (Specification (Stmt))) then
+ return Stmt;
+ end if;
+ end if;
-- Return the current construct which is either a subprogram body,
-- a subprogram declaration or is illegal.
if Nkind (Context) = N_Compilation_Unit_Aux then
return Unit (Parent (Context));
+ -- The pragma appears inside the statements of a subprogram body. This
+ -- placement is the result of subprogram contract expansion.
+
+ elsif Nkind (Context) = N_Handled_Sequence_Of_Statements then
+ return Parent (Context);
+
-- The pragma appears inside the declarative part of a subprogram body
elsif Nkind (Context) = N_Subprogram_Body then
return Context;
+ -- The pragma is a byproduct of aspect expansion, return the related
+ -- context of the original aspect. This case has a lower priority as
+ -- the above circuitry pinpoints precisely the related context.
+
+ elsif Present (Corresponding_Aspect (Prag)) then
+ return Parent (Corresponding_Aspect (Prag));
+
-- No candidate subprogram [body] found
else
end if;
end Find_Related_Subprogram_Or_Body;
+ ------------------
+ -- Get_Argument --
+ ------------------
+
+ function Get_Argument
+ (Prag : Node_Id;
+ Spec_Id : Entity_Id := Empty) return Node_Id
+ is
+ Args : constant List_Id := Pragma_Argument_Associations (Prag);
+
+ begin
+ -- Use the expression of the original aspect if possible when compiling
+ -- for ASIS or when analyzing the template of a generic subprogram. In
+ -- both cases the aspect's tree must be decorated to allow for ASIS
+ -- queries or to save all global references in the generic context.
+
+ if From_Aspect_Specification (Prag)
+ and then
+ (ASIS_Mode or else (Present (Spec_Id)
+ and then Is_Generic_Subprogram (Spec_Id)))
+ then
+ return Corresponding_Aspect (Prag);
+
+ -- Otherwise use the expression of the pragma
+
+ elsif Present (Args) then
+ return First (Args);
+
+ else
+ return Empty;
+ end if;
+ end Get_Argument;
+
-------------------------
-- Get_Base_Subprogram --
-------------------------
end case;
end Is_Valid_Assertion_Kind;
- -----------------------------------------
- -- Make_Aspect_For_PPC_In_Gen_Sub_Decl --
- -----------------------------------------
-
- procedure Make_Aspect_For_PPC_In_Gen_Sub_Decl (Decl : Node_Id) is
- Aspects : constant List_Id := New_List;
- Loc : constant Source_Ptr := Sloc (Decl);
- Or_Decl : constant Node_Id := Original_Node (Decl);
-
- Original_Aspects : List_Id;
- -- To capture global references, a copy of the created aspects must be
- -- inserted in the original tree.
-
- Prag : Node_Id;
- Prag_Arg_Ass : Node_Id;
- Prag_Id : Pragma_Id;
-
- begin
- -- Check for any PPC pragmas that appear within Decl
-
- Prag := Next (Decl);
- while Nkind (Prag) = N_Pragma loop
- Prag_Id := Get_Pragma_Id (Chars (Pragma_Identifier (Prag)));
-
- case Prag_Id is
- when Pragma_Postcondition | Pragma_Precondition =>
- Prag_Arg_Ass := First (Pragma_Argument_Associations (Prag));
-
- -- Make an aspect from any PPC pragma
-
- Append_To (Aspects,
- Make_Aspect_Specification (Loc,
- Identifier =>
- Make_Identifier (Loc, Chars (Pragma_Identifier (Prag))),
- Expression =>
- Copy_Separate_Tree (Expression (Prag_Arg_Ass))));
-
- -- Generate the analysis information in the pragma expression
- -- and then set the pragma node analyzed to avoid any further
- -- analysis.
-
- Analyze (Expression (Prag_Arg_Ass));
- Set_Analyzed (Prag, True);
-
- when others => null;
- end case;
-
- Next (Prag);
- end loop;
-
- -- Set all new aspects into the generic declaration node
-
- if Is_Non_Empty_List (Aspects) then
-
- -- Create the list of aspects to be inserted in the original tree
-
- Original_Aspects := Copy_Separate_List (Aspects);
-
- -- Check if Decl already has aspects
-
- -- Attach the new lists of aspects to both the generic copy and the
- -- original tree.
-
- if Has_Aspects (Decl) then
- Append_List (Aspects, Aspect_Specifications (Decl));
- Append_List (Original_Aspects, Aspect_Specifications (Or_Decl));
-
- else
- Set_Parent (Aspects, Decl);
- Set_Aspect_Specifications (Decl, Aspects);
- Set_Parent (Original_Aspects, Or_Decl);
- Set_Aspect_Specifications (Or_Decl, Original_Aspects);
- end if;
- end if;
- end Make_Aspect_For_PPC_In_Gen_Sub_Decl;
-
- -------------------------
- -- Preanalyze_CTC_Args --
- -------------------------
-
- procedure Preanalyze_CTC_Args (N, Arg_Req, Arg_Ens : Node_Id) is
- begin
- -- Preanalyze the boolean expressions, we treat these as spec
- -- expressions (i.e. similar to a default expression).
-
- if Present (Arg_Req) then
- Preanalyze_Assert_Expression
- (Get_Pragma_Arg (Arg_Req), Standard_Boolean);
-
- -- In ASIS mode, for a pragma generated from a source aspect, also
- -- analyze the original aspect expression.
-
- if ASIS_Mode and then Present (Corresponding_Aspect (N)) then
- Preanalyze_Assert_Expression
- (Original_Node (Get_Pragma_Arg (Arg_Req)), Standard_Boolean);
- end if;
- end if;
-
- if Present (Arg_Ens) then
- Preanalyze_Assert_Expression
- (Get_Pragma_Arg (Arg_Ens), Standard_Boolean);
-
- -- In ASIS mode, for a pragma generated from a source aspect, also
- -- analyze the original aspect expression.
-
- if ASIS_Mode and then Present (Corresponding_Aspect (N)) then
- Preanalyze_Assert_Expression
- (Original_Node (Get_Pragma_Arg (Arg_Ens)), Standard_Boolean);
- end if;
- end if;
- end Preanalyze_CTC_Args;
-
--------------------------------------
-- Process_Compilation_Unit_Pragmas --
--------------------------------------
Generate_Reference (Entity (With_Item), N, Set_Ref => False);
end Set_Elab_Unit_Name;
+ -------------------
+ -- Test_Case_Arg --
+ -------------------
+
+ function Test_Case_Arg
+ (Prag : Node_Id;
+ Arg_Nam : Name_Id;
+ From_Aspect : Boolean := False) return Node_Id
+ is
+ Aspect : constant Node_Id := Corresponding_Aspect (Prag);
+ Arg : Node_Id;
+ Args : Node_Id;
+
+ begin
+ pragma Assert (Nam_In (Arg_Nam, Name_Ensures,
+ Name_Mode,
+ Name_Name,
+ Name_Requires));
+
+ -- The caller requests the aspect argument
+
+ if From_Aspect then
+ if Present (Aspect)
+ and then Nkind (Expression (Aspect)) = N_Aggregate
+ then
+ Args := Expression (Aspect);
+
+ -- "Name" and "Mode" may appear without an identifier as a
+ -- positional association.
+
+ if Present (Expressions (Args)) then
+ Arg := First (Expressions (Args));
+
+ if Present (Arg) and then Arg_Nam = Name_Name then
+ return Arg;
+ end if;
+
+ -- Skip "Name"
+
+ Arg := Next (Arg);
+
+ if Present (Arg) and then Arg_Nam = Name_Mode then
+ return Arg;
+ end if;
+ end if;
+
+ -- Some or all arguments may appear as component associatons
+
+ if Present (Component_Associations (Args)) then
+ Arg := First (Component_Associations (Args));
+ while Present (Arg) loop
+ if Chars (First (Choices (Arg))) = Arg_Nam then
+ return Arg;
+ end if;
+
+ Next (Arg);
+ end loop;
+ end if;
+ end if;
+
+ -- Otherwise retrieve the argument directly from the pragma
+
+ else
+ Arg := First (Pragma_Argument_Associations (Prag));
+
+ if Present (Arg) and then Arg_Nam = Name_Name then
+ return Arg;
+ end if;
+
+ -- Skip argument "Name"
+
+ Arg := Next (Arg);
+
+ if Present (Arg) and then Arg_Nam = Name_Mode then
+ return Arg;
+ end if;
+
+ -- Skip argument "Mode"
+
+ Arg := Next (Arg);
+
+ -- Arguments "Requires" and "Ensures" are optional and may not be
+ -- present at all.
+
+ while Present (Arg) loop
+ if Chars (Arg) = Arg_Nam then
+ return Arg;
+ end if;
+
+ Next (Arg);
+ end loop;
+ end if;
+
+ return Empty;
+ end Test_Case_Arg;
+
end Sem_Prag;
procedure Analyze_Initializes_In_Decl_Part (N : Node_Id);
-- Perform full analysis of delayed pragma Initializes
- procedure Analyze_Pre_Post_Condition_In_Decl_Part
- (Prag : Node_Id;
- Subp_Id : Entity_Id);
- -- Perform preanalysis of a [refined] precondition or postcondition that
- -- appears on a subprogram declaration or body [stub]. Prag denotes the
- -- pragma, Subp_Id is the entity of the related subprogram. The preanalysis
- -- of the expression is done as "spec expression" (see section "Handling
- -- of Default and Per-Object Expressions in Sem).
+ procedure Analyze_Pre_Post_Condition_In_Decl_Part (N : Node_Id);
+ -- Perform preanalysis of [refined] precondition or postcondition pragma
+ -- N that appears on a subprogram declaration or body [stub].
procedure Analyze_Refined_Depends_In_Decl_Part (N : Node_Id);
-- Preform full analysis of delayed pragma Refined_Depends. This routine
procedure Analyze_Refined_State_In_Decl_Part (N : Node_Id);
-- Perform full analysis of delayed pragma Refined_State
- procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id; S : Entity_Id);
- -- Perform preanalysis of pragma Test_Case that applies to a subprogram
- -- declaration. Parameter N denotes the pragma, S is the entity of the
- -- related subprogram. The preanalysis of the expression is done as "spec
- -- expression" (see section "Handling of Default and Per-Object Expressions
- -- in Sem).
+ procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id);
+ -- Perform preanalysis of pragma Test_Case
procedure Check_Applicable_Policy (N : Node_Id);
-- N is either an N_Aspect or an N_Pragma node. There are two cases. If
-- True have their analysis delayed until after the main program is parsed
-- and analyzed.
+ function Find_Related_Subprogram_Or_Body
+ (Prag : Node_Id;
+ Do_Checks : Boolean := False) return Node_Id;
+ -- Subsidiary to the analysis of pragmas Contract_Cases, Depends, Global,
+ -- Refined_Depends, Refined_Global and Refined_Post and attribute 'Result.
+ -- Find the declaration of the related subprogram [body or stub] subject
+ -- to pragma Prag. If flag Do_Checks is set, the routine reports duplicate
+ -- pragmas and detects improper use of refinement pragmas in stand alone
+ -- expression functions. The returned value depends on the related pragma
+ -- as follows:
+ -- 1) Pragmas Contract_Cases, Depends and Global yield the corresponding
+ -- N_Subprogram_Declaration node or if the pragma applies to a stand
+ -- alone body, the N_Subprogram_Body node or Empty if illegal.
+ -- 2) Pragmas Refined_Depends, Refined_Global and Refined_Post yield
+ -- N_Subprogram_Body or N_Subprogram_Body_Stub nodes or Empty if
+ -- illegal.
+
function Get_SPARK_Mode_From_Pragma (N : Node_Id) return SPARK_Mode_Type;
-- Given a pragma SPARK_Mode node, return corresponding mode id
-- Name_uInvariant, and Name_uType_Invariant (_Pre, _Post, _Invariant,
-- and _Type_Invariant).
- procedure Make_Aspect_For_PPC_In_Gen_Sub_Decl (Decl : Node_Id);
- -- This routine makes aspects from precondition or postcondition pragmas
- -- that appear within a generic subprogram declaration. Decl is the generic
- -- subprogram declaration node. Note that the aspects are attached to the
- -- generic copy and also to the orginal tree.
-
procedure Process_Compilation_Unit_Pragmas (N : Node_Id);
-- Called at the start of processing compilation unit N to deal with any
-- special issues regarding pragmas. In particular, we have to deal with
-- the value of the Interface_Name. Otherwise it is encoded as needed by
-- particular operating systems. See the body for details of the encoding.
+ function Test_Case_Arg
+ (Prag : Node_Id;
+ Arg_Nam : Name_Id;
+ From_Aspect : Boolean := False) return Node_Id;
+ -- Obtain argument "Name", "Mode", "Ensures" or "Requires" from Test_Case
+ -- pragma Prag as denoted by Arg_Nam. When From_Aspect is set, an attempt
+ -- is made to retrieve the argument from the corresponding aspect if there
+ -- is one. The returned argument has several formats:
+ --
+ -- N_Pragma_Argument_Association if retrieved directly from the pragma
+ --
+ -- N_Component_Association if retrieved from the corresponding aspect and
+ -- the argument appears in a named association form.
+ --
+ -- An arbitrary expression if retrieved from the corresponding aspect and
+ -- the argument appears in positional form.
+ --
+ -- Empty if there is no such argument
+
end Sem_Prag;
with Sem; use Sem;
with Sem_Aux; use Sem_Aux;
with Sem_Attr; use Sem_Attr;
+with Sem_Ch6; use Sem_Ch6;
with Sem_Ch8; use Sem_Ch8;
with Sem_Ch13; use Sem_Ch13;
with Sem_Disp; use Sem_Disp;
-----------------------
procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id) is
- Items : constant Node_Id := Contract (Id);
+ Items : Node_Id := Contract (Id);
procedure Add_Classification;
-- Prepend Prag to the list of classifications
-- Local variables
- Nam : Name_Id;
- PPC : Node_Id;
+ Prag_Nam : Name_Id;
-- Start of processing for Add_Contract_Item
begin
- -- The related context must have a contract and the item to be added
- -- must be a pragma.
+ -- A contract must contain only pragmas
- pragma Assert (Present (Items));
pragma Assert (Nkind (Prag) = N_Pragma);
+ Prag_Nam := Pragma_Name (Prag);
- Nam := Original_Aspect_Name (Prag);
+ -- Create a new contract when adding the first item
+
+ if No (Items) then
+ Items := Make_Contract (Sloc (Id));
+ Set_Contract (Id, Items);
+ end if;
-- Contract items related to [generic] packages or instantiations. The
-- applicable pragmas are:
-- Part_Of (instantiation only)
if Ekind_In (Id, E_Generic_Package, E_Package) then
- if Nam_In (Nam, Name_Abstract_State,
- Name_Initial_Condition,
- Name_Initializes)
+ if Nam_In (Prag_Nam, Name_Abstract_State,
+ Name_Initial_Condition,
+ Name_Initializes)
then
Add_Classification;
-- Indicator Part_Of must be associated with a package instantiation
- elsif Nam = Name_Part_Of and then Is_Generic_Instance (Id) then
+ elsif Prag_Nam = Name_Part_Of and then Is_Generic_Instance (Id) then
Add_Classification;
-- The pragma is not a proper contract item
-- Refined_States
elsif Ekind (Id) = E_Package_Body then
- if Nam = Name_Refined_State then
+ if Prag_Nam = Name_Refined_State then
Add_Classification;
-- The pragma is not a proper contract item
-- Depends
-- Extensions_Visible
-- Global
- -- Post
-- Postcondition
- -- Pre
-- Precondition
-- Test_Case
or else Is_Generic_Subprogram (Id)
or else Is_Subprogram (Id)
then
- if Nam_In (Nam, Name_Pre,
- Name_Precondition,
- Name_uPre,
- Name_Post,
- Name_Postcondition,
- Name_uPost)
- then
- -- Before we add a precondition or postcondition to the list, make
- -- sure we do not have a disallowed duplicate, which can happen if
- -- we use a pragma for Pre[_Class] or Post[_Class] instead of the
- -- corresponding aspect.
-
- if not From_Aspect_Specification (Prag)
- and then Nam_In (Nam, Name_Pre,
- Name_uPre,
- Name_Post,
- Name_Post_Class)
- then
- PPC := Pre_Post_Conditions (Items);
- while Present (PPC) loop
- if not Split_PPC (PPC)
- and then Original_Aspect_Name (PPC) = Nam
- then
- Error_Msg_Sloc := Sloc (PPC);
- Error_Msg_NE
- ("duplication of aspect for & given#", Prag, Id);
- return;
- end if;
-
- PPC := Next_Pragma (PPC);
- end loop;
- end if;
-
+ if Nam_In (Prag_Nam, Name_Postcondition, Name_Precondition) then
Add_Pre_Post_Condition;
- elsif Nam_In (Nam, Name_Contract_Cases, Name_Test_Case) then
+ elsif Nam_In (Prag_Nam, Name_Contract_Cases, Name_Test_Case) then
Add_Contract_Test_Case;
- elsif Nam_In (Nam, Name_Depends,
- Name_Extensions_Visible,
- Name_Global)
+ elsif Nam_In (Prag_Nam, Name_Depends,
+ Name_Extensions_Visible,
+ Name_Global)
then
Add_Classification;
end if;
-- Contract items related to subprogram bodies. Applicable pragmas are:
+ -- Postcondition
+ -- Precondition
-- Refined_Depends
-- Refined_Global
-- Refined_Post
elsif Ekind (Id) = E_Subprogram_Body then
- if Nam_In (Nam, Name_Refined_Depends, Name_Refined_Global) then
+ if Nam_In (Prag_Nam, Name_Refined_Depends, Name_Refined_Global) then
Add_Classification;
- elsif Nam = Name_Refined_Post then
+ elsif Nam_In (Prag_Nam, Name_Postcondition,
+ Name_Precondition,
+ Name_Refined_Post)
+ then
Add_Pre_Post_Condition;
-- The pragma is not a proper contract item
-- Part_Of
elsif Ekind (Id) = E_Variable then
- if Nam_In (Nam, Name_Async_Readers,
- Name_Async_Writers,
- Name_Effective_Reads,
- Name_Effective_Writes,
- Name_Part_Of)
+ if Nam_In (Prag_Nam, Name_Async_Readers,
+ Name_Async_Writers,
+ Name_Effective_Reads,
+ Name_Effective_Writes,
+ Name_Part_Of)
then
Add_Classification;
-- Check_Result_And_Post_State --
---------------------------------
- procedure Check_Result_And_Post_State
- (Prag : Node_Id;
- Result_Seen : in out Boolean)
- is
- procedure Check_Expression (Expr : Node_Id);
- -- Perform the 'Result and post-state checks on a given expression
+ procedure Check_Result_And_Post_State (Subp_Id : Entity_Id) is
+ procedure Check_Result_And_Post_State_In_Pragma
+ (Prag : Node_Id;
+ Result_Seen : in out Boolean);
+ -- Determine whether pragma Prag mentions attribute 'Result and whether
+ -- the pragma contains an expression that evaluates differently in pre-
+ -- and post-state. Prag is a [refined] postcondition or a contract-cases
+ -- pragma. Result_Seen is set when the pragma mentions attribute 'Result
+
+ function Has_In_Out_Parameter (Subp_Id : Entity_Id) return Boolean;
+ -- Determine whether subprogram Subp_Id contains at least one IN OUT
+ -- formal parameter.
+
+ -------------------------------------------
+ -- Check_Result_And_Post_State_In_Pragma --
+ -------------------------------------------
+
+ procedure Check_Result_And_Post_State_In_Pragma
+ (Prag : Node_Id;
+ Result_Seen : in out Boolean)
+ is
+ procedure Check_Expression (Expr : Node_Id);
+ -- Perform the 'Result and post-state checks on a given expression
- function Is_Function_Result (N : Node_Id) return Traverse_Result;
- -- Attempt to find attribute 'Result in a subtree denoted by N
+ function Is_Function_Result (N : Node_Id) return Traverse_Result;
+ -- Attempt to find attribute 'Result in a subtree denoted by N
- function Is_Trivial_Boolean (N : Node_Id) return Boolean;
- -- Determine whether source node N denotes "True" or "False"
+ function Is_Trivial_Boolean (N : Node_Id) return Boolean;
+ -- Determine whether source node N denotes "True" or "False"
- function Mentions_Post_State (N : Node_Id) return Boolean;
- -- Determine whether a subtree denoted by N mentions any construct that
- -- denotes a post-state.
+ function Mentions_Post_State (N : Node_Id) return Boolean;
+ -- Determine whether a subtree denoted by N mentions any construct
+ -- that denotes a post-state.
- procedure Check_Function_Result is
- new Traverse_Proc (Is_Function_Result);
+ procedure Check_Function_Result is
+ new Traverse_Proc (Is_Function_Result);
- ----------------------
- -- Check_Expression --
- ----------------------
+ ----------------------
+ -- Check_Expression --
+ ----------------------
- procedure Check_Expression (Expr : Node_Id) is
- begin
- if not Is_Trivial_Boolean (Expr) then
- Check_Function_Result (Expr);
+ procedure Check_Expression (Expr : Node_Id) is
+ begin
+ if not Is_Trivial_Boolean (Expr) then
+ Check_Function_Result (Expr);
- if not Mentions_Post_State (Expr) then
- if Pragma_Name (Prag) = Name_Contract_Cases then
- Error_Msg_N
- ("contract case refers only to pre-state?T?", Expr);
+ if not Mentions_Post_State (Expr) then
+ if Pragma_Name (Prag) = Name_Contract_Cases then
+ Error_Msg_NE
+ ("contract case does not check the outcome of calling "
+ & "&?T?", Expr, Subp_Id);
- elsif Pragma_Name (Prag) = Name_Refined_Post then
- Error_Msg_N
- ("refined postcondition refers only to pre-state?T?",
- Prag);
+ elsif Pragma_Name (Prag) = Name_Refined_Post then
+ Error_Msg_NE
+ ("refined postcondition does not check the outcome of "
+ & "calling &?T?", Prag, Subp_Id);
- else
- Error_Msg_N
- ("postcondition refers only to pre-state?T?", Prag);
+ else
+ Error_Msg_NE
+ ("postcondition does not check the outcome of calling "
+ & "&?T?", Prag, Subp_Id);
+ end if;
end if;
end if;
- end if;
- end Check_Expression;
+ end Check_Expression;
- ------------------------
- -- Is_Function_Result --
- ------------------------
+ ------------------------
+ -- Is_Function_Result --
+ ------------------------
- function Is_Function_Result (N : Node_Id) return Traverse_Result is
- begin
- if Is_Attribute_Result (N) then
- Result_Seen := True;
- return Abandon;
+ function Is_Function_Result (N : Node_Id) return Traverse_Result is
+ begin
+ if Is_Attribute_Result (N) then
+ Result_Seen := True;
+ return Abandon;
- -- Continue the traversal
+ -- Continue the traversal
- else
- return OK;
- end if;
- end Is_Function_Result;
+ else
+ return OK;
+ end if;
+ end Is_Function_Result;
- ------------------------
- -- Is_Trivial_Boolean --
- ------------------------
+ ------------------------
+ -- Is_Trivial_Boolean --
+ ------------------------
- function Is_Trivial_Boolean (N : Node_Id) return Boolean is
- begin
- return
- Comes_From_Source (N)
- and then Is_Entity_Name (N)
- and then (Entity (N) = Standard_True
- or else
- Entity (N) = Standard_False);
- end Is_Trivial_Boolean;
+ function Is_Trivial_Boolean (N : Node_Id) return Boolean is
+ begin
+ return
+ Comes_From_Source (N)
+ and then Is_Entity_Name (N)
+ and then (Entity (N) = Standard_True
+ or else
+ Entity (N) = Standard_False);
+ end Is_Trivial_Boolean;
- -------------------------
- -- Mentions_Post_State --
- -------------------------
+ -------------------------
+ -- Mentions_Post_State --
+ -------------------------
- function Mentions_Post_State (N : Node_Id) return Boolean is
- Post_State_Seen : Boolean := False;
+ function Mentions_Post_State (N : Node_Id) return Boolean is
+ Post_State_Seen : Boolean := False;
- function Is_Post_State (N : Node_Id) return Traverse_Result;
- -- Attempt to find a construct that denotes a post-state. If this is
- -- the case, set flag Post_State_Seen.
+ function Is_Post_State (N : Node_Id) return Traverse_Result;
+ -- Attempt to find a construct that denotes a post-state. If this
+ -- is the case, set flag Post_State_Seen.
- -------------------
- -- Is_Post_State --
- -------------------
+ -------------------
+ -- Is_Post_State --
+ -------------------
- function Is_Post_State (N : Node_Id) return Traverse_Result is
- Ent : Entity_Id;
+ function Is_Post_State (N : Node_Id) return Traverse_Result is
+ Ent : Entity_Id;
- begin
- if Nkind_In (N, N_Explicit_Dereference, N_Function_Call) then
- Post_State_Seen := True;
- return Abandon;
+ begin
+ if Nkind_In (N, N_Explicit_Dereference, N_Function_Call) then
+ Post_State_Seen := True;
+ return Abandon;
- elsif Nkind_In (N, N_Expanded_Name, N_Identifier) then
- Ent := Entity (N);
+ elsif Nkind_In (N, N_Expanded_Name, N_Identifier) then
+ Ent := Entity (N);
- -- The entity may be modifiable through an implicit dereference
+ -- The entity may be modifiable through an implicit
+ -- dereference.
- if No (Ent)
- or else Ekind (Ent) in Assignable_Kind
- or else (Is_Access_Type (Etype (Ent))
- and then Nkind (Parent (N)) = N_Selected_Component)
- then
- Post_State_Seen := True;
- return Abandon;
- end if;
+ if No (Ent)
+ or else Ekind (Ent) in Assignable_Kind
+ or else (Is_Access_Type (Etype (Ent))
+ and then Nkind (Parent (N)) =
+ N_Selected_Component)
+ then
+ Post_State_Seen := True;
+ return Abandon;
+ end if;
- elsif Nkind (N) = N_Attribute_Reference then
- if Attribute_Name (N) = Name_Old then
- return Skip;
+ elsif Nkind (N) = N_Attribute_Reference then
+ if Attribute_Name (N) = Name_Old then
+ return Skip;
- elsif Attribute_Name (N) = Name_Result then
- Post_State_Seen := True;
- return Abandon;
+ elsif Attribute_Name (N) = Name_Result then
+ Post_State_Seen := True;
+ return Abandon;
+ end if;
end if;
- end if;
- return OK;
- end Is_Post_State;
+ return OK;
+ end Is_Post_State;
+
+ procedure Find_Post_State is new Traverse_Proc (Is_Post_State);
- procedure Find_Post_State is new Traverse_Proc (Is_Post_State);
+ -- Start of processing for Mentions_Post_State
- -- Start of processing for Mentions_Post_State
+ begin
+ Find_Post_State (N);
+
+ return Post_State_Seen;
+ end Mentions_Post_State;
+
+ -- Local variables
+
+ Expr : constant Node_Id :=
+ Get_Pragma_Arg
+ (First (Pragma_Argument_Associations (Prag)));
+ Nam : constant Name_Id := Pragma_Name (Prag);
+ CCase : Node_Id;
+
+ -- Start of processing for Check_Result_And_Post_State_In_Pragma
begin
- Find_Post_State (N);
+ -- Examine all consequences
- return Post_State_Seen;
- end Mentions_Post_State;
+ if Nam = Name_Contract_Cases then
+ CCase := First (Component_Associations (Expr));
+ while Present (CCase) loop
+ Check_Expression (Expression (CCase));
+
+ Next (CCase);
+ end loop;
+
+ -- Examine the expression of a postcondition
+
+ else pragma Assert (Nam_In (Nam, Name_Postcondition,
+ Name_Refined_Post));
+ Check_Expression (Expr);
+ end if;
+ end Check_Result_And_Post_State_In_Pragma;
+
+ --------------------------
+ -- Has_In_Out_Parameter --
+ --------------------------
+
+ function Has_In_Out_Parameter (Subp_Id : Entity_Id) return Boolean is
+ Formal : Entity_Id;
+
+ begin
+ -- Traverse the formals looking for an IN OUT parameter
+
+ Formal := First_Formal (Subp_Id);
+ while Present (Formal) loop
+ if Ekind (Formal) = E_In_Out_Parameter then
+ return True;
+ end if;
+
+ Next_Formal (Formal);
+ end loop;
+
+ return False;
+ end Has_In_Out_Parameter;
-- Local variables
- Expr : constant Node_Id :=
- Get_Pragma_Arg (First (Pragma_Argument_Associations (Prag)));
- Nam : constant Name_Id := Pragma_Name (Prag);
- CCase : Node_Id;
+ Items : constant Node_Id := Contract (Subp_Id);
+ Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
+ Case_Prag : Node_Id := Empty;
+ Post_Prag : Node_Id := Empty;
+ Prag : Node_Id;
+ Seen_In_Case : Boolean := False;
+ Seen_In_Post : Boolean := False;
+ Spec_Id : Entity_Id;
-- Start of processing for Check_Result_And_Post_State
begin
- -- Examine all consequences
+ -- The lack of attribute 'Result or a post-state is classified as a
+ -- suspicious contract. Do not perform the check if the corresponding
+ -- swich is not set.
- if Nam = Name_Contract_Cases then
- CCase := First (Component_Associations (Expr));
- while Present (CCase) loop
- Check_Expression (Expression (CCase));
+ if not Warn_On_Suspicious_Contract then
+ return;
- Next (CCase);
- end loop;
+ -- Nothing to do if there is no contract
+
+ elsif No (Items) then
+ return;
+ end if;
+
+ -- Retrieve the entity of the subprogram spec (if any)
+
+ if Nkind (Subp_Decl) = N_Subprogram_Body
+ and then Present (Corresponding_Spec (Subp_Decl))
+ then
+ Spec_Id := Corresponding_Spec (Subp_Decl);
- -- Examine the expression of a postcondition
+ elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub
+ and then Present (Corresponding_Spec_Of_Stub (Subp_Decl))
+ then
+ Spec_Id := Corresponding_Spec_Of_Stub (Subp_Decl);
- else pragma Assert (Nam_In (Nam, Name_Postcondition, Name_Refined_Post));
- Check_Expression (Expr);
+ else
+ Spec_Id := Subp_Id;
+ end if;
+
+ -- Examine all postconditions for attribute 'Result and a post-state
+
+ Prag := Pre_Post_Conditions (Items);
+ while Present (Prag) loop
+ if Nam_In (Pragma_Name (Prag), Name_Postcondition,
+ Name_Refined_Post)
+ and then not Error_Posted (Prag)
+ then
+ Post_Prag := Prag;
+ Check_Result_And_Post_State_In_Pragma (Prag, Seen_In_Post);
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+
+ -- Examine the contract cases of the subprogram for attribute 'Result
+ -- and a post-state.
+
+ Prag := Contract_Test_Cases (Items);
+ while Present (Prag) loop
+ if Pragma_Name (Prag) = Name_Contract_Cases
+ and then not Error_Posted (Prag)
+ then
+ Case_Prag := Prag;
+ Check_Result_And_Post_State_In_Pragma (Prag, Seen_In_Case);
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+
+ -- Do not emit any errors if the subprogram is not a function
+
+ if not Ekind_In (Spec_Id, E_Function, E_Generic_Function) then
+ null;
+
+ -- Regardless of whether the function has postconditions or contract
+ -- cases, or whether they mention attribute 'Result, an IN OUT formal
+ -- parameter is always treated as a result.
+
+ elsif Has_In_Out_Parameter (Spec_Id) then
+ null;
+
+ -- The function has both a postcondition and contract cases and they do
+ -- not mention attribute 'Result.
+
+ elsif Present (Case_Prag)
+ and then not Seen_In_Case
+ and then Present (Post_Prag)
+ and then not Seen_In_Post
+ then
+ Error_Msg_N
+ ("neither postcondition nor contract cases mention function "
+ & "result?T?", Post_Prag);
+
+ -- The function has contract cases only and they do not mention
+ -- attribute 'Result.
+
+ elsif Present (Case_Prag) and then not Seen_In_Case then
+ Error_Msg_N ("contract cases do not mention result?T?", Case_Prag);
+
+ -- The function has postconditions only and they do not mention
+ -- attribute 'Result.
+
+ elsif Present (Post_Prag) and then not Seen_In_Post then
+ Error_Msg_N
+ ("postcondition does not mention function result?T?", Post_Prag);
end if;
end Check_Result_And_Post_State;
end if;
end Corresponding_Generic_Type;
+ ---------------------------
+ -- Corresponding_Spec_Of --
+ ---------------------------
+
+ function Corresponding_Spec_Of (Subp_Decl : Node_Id) return Entity_Id is
+ begin
+ if Nkind (Subp_Decl) = N_Subprogram_Body
+ and then Present (Corresponding_Spec (Subp_Decl))
+ then
+ return Corresponding_Spec (Subp_Decl);
+
+ elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub
+ and then Present (Corresponding_Spec_Of_Stub (Subp_Decl))
+ then
+ return Corresponding_Spec_Of_Stub (Subp_Decl);
+
+ else
+ return Defining_Entity (Subp_Decl);
+ end if;
+ end Corresponding_Spec_Of;
+
--------------------
-- Current_Entity --
--------------------
end if;
end Get_Enum_Lit_From_Pos;
- ---------------------------------
- -- Get_Ensures_From_CTC_Pragma --
- ---------------------------------
-
- function Get_Ensures_From_CTC_Pragma (N : Node_Id) return Node_Id is
- Args : constant List_Id := Pragma_Argument_Associations (N);
- Res : Node_Id;
-
- begin
- if List_Length (Args) = 4 then
- Res := Pick (Args, 4);
-
- elsif List_Length (Args) = 3 then
- Res := Pick (Args, 3);
-
- if Chars (Res) /= Name_Ensures then
- Res := Empty;
- end if;
-
- else
- Res := Empty;
- end if;
-
- return Res;
- end Get_Ensures_From_CTC_Pragma;
-
------------------------
-- Get_Generic_Entity --
------------------------
return R;
end Get_Renamed_Entity;
- ----------------------------------
- -- Get_Requires_From_CTC_Pragma --
- ----------------------------------
-
- function Get_Requires_From_CTC_Pragma (N : Node_Id) return Node_Id is
- Args : constant List_Id := Pragma_Argument_Associations (N);
- Res : Node_Id;
-
- begin
- if List_Length (Args) >= 3 then
- Res := Pick (Args, 3);
-
- if Chars (Res) /= Name_Requires then
- Res := Empty;
- end if;
-
- else
- Res := Empty;
- end if;
-
- return Res;
- end Get_Requires_From_CTC_Pragma;
-
-------------------------
-- Get_Subprogram_Body --
-------------------------
return Is_Floating_Point_Type (E) and then Signed_Zeros_On_Target;
end Has_Signed_Zeros;
+ ------------------------------
+ -- Has_Significant_Contract --
+ ------------------------------
+
+ function Has_Significant_Contract (Subp_Id : Entity_Id) return Boolean is
+ Subp_Nam : constant Name_Id := Chars (Subp_Id);
+
+ begin
+ -- _Finalizer procedure
+
+ if Subp_Nam = Name_uFinalizer then
+ return False;
+
+ -- _Postconditions procedure
+
+ elsif Subp_Nam = Name_uPostconditions then
+ return False;
+
+ -- Predicate function
+
+ elsif Ekind (Subp_Id) = E_Function
+ and then Is_Predicate_Function (Subp_Id)
+ then
+ return False;
+
+ -- TSS subprogram
+
+ elsif Get_TSS_Name (Subp_Id) /= TSS_Null then
+ return False;
+
+ else
+ return True;
+ end if;
+ end Has_Significant_Contract;
+
-----------------------------
-- Has_Static_Array_Bounds --
-----------------------------
if Is_Subprogram_Or_Generic_Subprogram (Subp)
and then Is_Subprogram_Or_Generic_Subprogram (From_Subp)
- and then Present (Contract (Subp))
and then Present (Contract (From_Subp))
then
Inherit_Pragma (Pragma_Extensions_Visible);
end loop;
end Inspect_Deferred_Constant_Completion;
+ -----------------------------
+ -- Install_Generic_Formals --
+ -----------------------------
+
+ procedure Install_Generic_Formals (Subp_Id : Entity_Id) is
+ E : Entity_Id;
+
+ begin
+ pragma Assert (Is_Generic_Subprogram (Subp_Id));
+
+ E := First_Entity (Subp_Id);
+ while Present (E) loop
+ Install_Entity (E);
+ Next_Entity (E);
+ end loop;
+ end Install_Generic_Formals;
+
-----------------------------
-- Is_Actual_Out_Parameter --
-----------------------------
end if;
end Object_Access_Level;
- --------------------------
- -- Original_Aspect_Name --
- --------------------------
+ ---------------------------------
+ -- Original_Aspect_Pragma_Name --
+ ---------------------------------
- function Original_Aspect_Name (N : Node_Id) return Name_Id is
- Pras : Node_Id;
- Name : Name_Id;
+ function Original_Aspect_Pragma_Name (N : Node_Id) return Name_Id is
+ Item : Node_Id;
+ Item_Nam : Name_Id;
begin
pragma Assert (Nkind_In (N, N_Aspect_Specification, N_Pragma));
- Pras := N;
- if Is_Rewrite_Substitution (Pras)
- and then Nkind (Original_Node (Pras)) = N_Pragma
- then
- Pras := Original_Node (Pras);
- end if;
+ Item := N;
- -- Case where we came from aspect specication
+ -- The pragma was generated to emulate an aspect, use the original
+ -- aspect specification.
- if Nkind (Pras) = N_Pragma and then From_Aspect_Specification (Pras) then
- Pras := Corresponding_Aspect (Pras);
+ if Nkind (Item) = N_Pragma and then From_Aspect_Specification (Item) then
+ Item := Corresponding_Aspect (Item);
end if;
- -- Get name from aspect or pragma
+ -- Retrieve the name of the aspect/pragma. Note that Pre, Pre_Class,
+ -- Post and Post_Class rewrite their pragma identifier to preserve the
+ -- original name.
+ -- ??? this is kludgey
+
+ if Nkind (Item) = N_Pragma then
+ Item_Nam := Chars (Original_Node (Pragma_Identifier (Item)));
- if Nkind (Pras) = N_Pragma then
- Name := Pragma_Name (Pras);
else
- Name := Chars (Identifier (Pras));
+ pragma Assert (Nkind (Item) = N_Aspect_Specification);
+ Item_Nam := Chars (Identifier (Item));
end if;
- -- Deal with 'Class
-
- if Class_Present (Pras) then
- case Name is
+ -- Deal with 'Class by converting the name to its _XXX form
- -- Names that need converting to special _xxx form
+ if Class_Present (Item) then
+ if Item_Nam = Name_Invariant then
+ Item_Nam := Name_uInvariant;
- when Name_Pre |
- Name_Pre_Class =>
- Name := Name_uPre;
+ elsif Nam_In (Item_Nam, Name_Post, Name_Post_Class) then
+ Item_Nam := Name_uPost;
- when Name_Post |
- Name_Post_Class =>
- Name := Name_uPost;
+ elsif Nam_In (Item_Nam, Name_Pre, Name_Pre_Class) then
+ Item_Nam := Name_uPre;
- when Name_Invariant =>
- Name := Name_uInvariant;
+ elsif Item_Nam = Name_Invariant then
+ Item_Nam := Name_uInvariant;
- when Name_Type_Invariant |
- Name_Type_Invariant_Class =>
- Name := Name_uType_Invariant;
+ elsif Nam_In (Item_Nam, Name_Type_Invariant,
+ Name_Type_Invariant_Class)
+ then
+ Item_Nam := Name_uType_Invariant;
- -- Nothing to do for other cases (e.g. a Check that derived
- -- from Pre_Class and has the flag set). Also we do nothing
- -- if the name is already in special _xxx form.
+ -- Nothing to do for other cases (e.g. a Check that derived from
+ -- Pre_Class and has the flag set). Also we do nothing if the name
+ -- is already in special _xxx form.
- when others =>
- null;
- end case;
+ end if;
end if;
- return Name;
- end Original_Aspect_Name;
+ return Item_Nam;
+ end Original_Aspect_Pragma_Name;
--------------------------------------
-- Original_Corresponding_Operation --
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- N is one of the statement forms that is a potentially blocking
-- operation. If it appears within a protected action, emit warning.
- procedure Check_Result_And_Post_State
- (Prag : Node_Id;
- Result_Seen : in out Boolean);
- -- Determine whether pragma Prag mentions attribute 'Result and whether
- -- the pragma contains an expression that evaluates differently in pre-
- -- and post-state. Prag is a [refined] postcondition or a contract-cases
- -- pragma. Result_Seen is set when the pragma mentions attribute 'Result.
+ procedure Check_Result_And_Post_State (Subp_Id : Entity_Id);
+ -- Determine whether the contract of subprogram Subp_Id mentions attribute
+ -- 'Result and it contains an expression that evaluates differently in pre-
+ -- and post-state.
procedure Check_Unprotected_Access
(Context : Node_Id;
-- attribute, except in the case of formal private and derived types.
-- Possible optimization???
+ function Corresponding_Spec_Of (Subp_Decl : Node_Id) return Entity_Id;
+ -- Return the corresponding spec of Subp_Decl when it denotes a body [stub]
+ -- or the defining entity of subprogram declaration Subp_Decl in all other
+ -- cases.
+
function Current_Entity (N : Node_Id) return Entity_Id;
pragma Inline (Current_Entity);
-- Find the currently visible definition for a given identifier, that is to
-- If expression N references a part of an object, return this object.
-- Otherwise return Empty. Expression N should have been resolved already.
- function Get_Ensures_From_CTC_Pragma (N : Node_Id) return Node_Id;
- -- Return the Ensures component of Test_Case pragma N, or Empty otherwise
- -- Bad name now that this no longer applies to Contract_Case ???
-
function Get_Generic_Entity (N : Node_Id) return Entity_Id;
-- Returns the true generic entity in an instantiation. If the name in the
-- instantiation is a renaming, the function returns the renamed generic.
-- not a renamed entity, returns its argument. It is an error to call this
-- with any other kind of entity.
- function Get_Requires_From_CTC_Pragma (N : Node_Id) return Node_Id;
- -- Return the Requires component of Test_Case pragma N, or Empty otherwise
- -- Bad name now that this no longer applies to Contract_Case ???
-
function Get_Subprogram_Entity (Nod : Node_Id) return Entity_Id;
-- Nod is either a procedure call statement, or a function call, or an
-- accept statement node. This procedure finds the Entity_Id of the related
-- Determines if the floating-point type E supports signed zeros.
-- Returns False if E is not a floating-point type.
+ function Has_Significant_Contract (Subp_Id : Entity_Id) return Boolean;
+ -- Determine whether subprogram [body] Subp_Id has a significant contract.
+ -- All subprograms have a N_Contract node, but this does not mean that the
+ -- contract is useful.
+
function Has_Static_Array_Bounds (Typ : Node_Id) return Boolean;
-- Return whether an array type has static bounds
-- whether they have been completed by a full constant declaration or an
-- Import pragma. Emit the error message if that is not the case.
+ procedure Install_Generic_Formals (Subp_Id : Entity_Id);
+ -- Install both the generic formal parameters and the formal parameters of
+ -- generic subprogram Subp_Id into visibility.
+
function Is_Actual_Out_Parameter (N : Node_Id) return Boolean;
-- Determines if N is an actual parameter of out mode in a subprogram call
-- corresponding operation of S is the original corresponding operation of
-- S2. Otherwise, it is S itself.
- function Original_Aspect_Name (N : Node_Id) return Name_Id;
- -- N is a pragma node or aspect specification node. This function returns
- -- the name of the pragma or aspect in original source form, taking into
- -- account possible rewrites, and also cases where a pragma comes from an
- -- aspect (in such cases, the name can be different from the pragma name,
- -- e.g. a Pre aspect generates a Precondition pragma). This also deals with
- -- the presence of 'Class, which results in one of the special names
- -- Name_uPre, Name_uPost, Name_uInvariant, or Name_uType_Invariant being
- -- returned to represent the corresponding aspects with x'Class names.
+ function Original_Aspect_Pragma_Name (N : Node_Id) return Name_Id;
+ -- Retrieve the name of aspect or pragma N taking into account a possible
+ -- rewrite and whether the pragma is generated from an aspect as the names
+ -- may be different. The routine also deals with 'Class in which case it
+ -- returns the following values:
+ --
+ -- Invariant -> Name_uInvariant
+ -- Post -> Name_uPost
+ -- Post'Class -> Name_uPost
+ -- Pre -> Name_uPre
+ -- Pre'Class -> Name_uPre
+ -- Type_Invariant -> Name_uType_Invariant
+ -- Type_Invariant'Class -> Name_uType_Invariant
function Policy_In_Effect (Policy : Name_Id) return Name_Id;
-- Given a policy, return the policy identifier associated with it. If no
with Sem_Ch8; use Sem_Ch8;
with Sem_Aux; use Sem_Aux;
with Sem_Eval; use Sem_Eval;
+with Sem_Prag; use Sem_Prag;
with Sem_Util; use Sem_Util;
with Sinfo; use Sinfo;
with Sinput; use Sinput;
if Nkind (P) = N_Pragma
and then Pragma_Name (P) = Name_Test_Case
- and then Nod = Get_Ensures_From_CTC_Pragma (P)
+ and then Nod = Test_Case_Arg (P, Name_Ensures)
then
return True;
end if;
projects / gcc.git / commitdiff