* einfo.adb (Get_Pragma): Handle the retrieval of delayed
pragmas stored in N_Contract nodes.
* einfo.ads (Get_Pragma): Update the comment on usage.
* sem_prag.adb (Check_Precondition_Postcondition): Retain a copy
of the pragma when it applies to a body that acts as a spec. The
copy is preanalyzed and chained on the contract of the body.
git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@200774
138bc75d-0d04-0410-961f-
82ee72b054a4
+2013-07-08 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * einfo.adb (Get_Pragma): Handle the retrieval of delayed
+ pragmas stored in N_Contract nodes.
+ * einfo.ads (Get_Pragma): Update the comment on usage.
+ * sem_prag.adb (Check_Precondition_Postcondition): Retain a copy
+ of the pragma when it applies to a body that acts as a spec. The
+ copy is preanalyzed and chained on the contract of the body.
+
2013-07-08 Robert Dewar <dewar@adacore.com>
* rtsfind.adb: Minor comment fix.
-- Get_Pragma --
----------------
- function Get_Pragma (E : Entity_Id; Id : Pragma_Id) return Node_Id
- is
- N : Node_Id;
+ function Get_Pragma (E : Entity_Id; Id : Pragma_Id) return Node_Id is
+ Is_CDG : constant Boolean :=
+ Id = Pragma_Depends or else Id = Pragma_Global;
+ Is_CTC : constant Boolean :=
+ Id = Pragma_Contract_Cases or else Id = Pragma_Test_Case;
+ Is_PPC : constant Boolean :=
+ Id = Pragma_Precondition or else Id = Pragma_Postcondition;
+ Delayed : constant Boolean := Is_CDG or else Is_CTC or else Is_PPC;
+ Item : Node_Id;
+ Items : Node_Id;
begin
- N := First_Rep_Item (E);
- while Present (N) loop
- if Nkind (N) = N_Pragma
- and then Get_Pragma_Id (Pragma_Name (N)) = Id
+ -- Handle delayed pragmas that appear in N_Contract nodes. Those have to
+ -- be extracted from their specialized list.
+
+ if Delayed then
+ Items := Contract (E);
+
+ if No (Items) then
+ return Empty;
+
+ elsif Is_CDG then
+ Item := Classifications (Items);
+
+ elsif Is_CTC then
+ Item := Contract_Test_Cases (Items);
+
+ else
+ Item := Pre_Post_Conditions (Items);
+ end if;
+
+ -- Regular pragmas
+
+ else
+ Item := First_Rep_Item (E);
+ end if;
+
+ while Present (Item) loop
+ if Nkind (Item) = N_Pragma
+ and then Get_Pragma_Id (Pragma_Name (Item)) = Id
then
- return N;
+ return Item;
+
+ -- All nodes in N_Contract are chained using Next_Pragma
+
+ elsif Delayed then
+ Item := Next_Pragma (Item);
+
+ -- Regular pragmas
+
else
- Next_Rep_Item (N);
+ Next_Rep_Item (Item);
end if;
end loop;
function Get_Pragma (E : Entity_Id; Id : Pragma_Id) return Node_Id;
-- Searches the Rep_Item chain for a given entity E, for an instance of
-- a pragma with the given pragma Id. If found, the value returned is the
- -- N_Pragma node, otherwise Empty is returned.
+ -- N_Pragma node, otherwise Empty is returned. Delayed pragmas such as
+ -- Precondition, Postcondition, Contract_Cases, Depends and Global appear
+ -- in the N_Contract node of entity E and are also handled by this routine.
function Get_Record_Representation_Clause (E : Entity_Id) return Node_Id;
-- Searches the Rep_Item chain for a given entity E, for a record
-- 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.
- if Nkind (Parent (N)) = N_Subprogram_Body
- and then List_Containing (N) = Declarations (Parent (N))
+ 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
+ if Operating_Mode /= Generate_Code or else Inside_A_Generic then
+
-- Analyze pragma expression for correctness and for ASIS use
Preanalyze_Assert_Expression
end if;
end if;
+ -- Retain a copy of the pre- or postcondition pragma for formal
+ -- verification purposes. 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 (SPARK_Mode or else Formal_Extensions)
+ 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 (Parent (N)) = N_Compilation_Unit_Aux then
+ elsif Nkind (PO) = N_Compilation_Unit_Aux then
-- In formal verification mode, analyze pragma expression for
-- correctness, as it is not expanded later.
if SPARK_Mode then
Analyze_PPC_In_Decl_Part
- (N, Defining_Entity (Unit (Parent (Parent (N)))));
+ (N, Defining_Entity (Unit (Parent (PO))));
end if;
- Chain_PPC (Unit (Parent (Parent (N))));
+ Chain_PPC (Unit (Parent (PO)));
return;
end if;