From 78d432da45406aaeb97b7485f548d07fc3ca7049 Mon Sep 17 00:00:00 2001 From: Hristian Kirtchev Date: Mon, 8 Jul 2013 08:19:20 +0000 Subject: [PATCH] einfo.adb (Get_Pragma): Handle the retrieval of delayed pragmas stored in N_Contract nodes. 2013-07-08 Hristian Kirtchev * 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. From-SVN: r200774 --- gcc/ada/ChangeLog | 9 +++++++ gcc/ada/einfo.adb | 59 ++++++++++++++++++++++++++++++++++++-------- gcc/ada/einfo.ads | 4 ++- gcc/ada/sem_prag.adb | 51 ++++++++++++++++++++++++++++++++------ 4 files changed, 104 insertions(+), 19 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index b5089150855..9178fc86714 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,12 @@ +2013-07-08 Hristian Kirtchev + + * 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 * rtsfind.adb: Minor comment fix. diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index bca20443bed..0ed05608afb 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -6280,19 +6280,58 @@ package body Einfo is -- 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 - then - return N; + -- 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 - Next_Rep_Item (N); + 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 Item; + + -- All nodes in N_Contract are chained using Next_Pragma + + elsif Delayed then + Item := Next_Pragma (Item); + + -- Regular pragmas + + else + Next_Rep_Item (Item); end if; end loop; diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index a99812117b8..24bb12cf797 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -7375,7 +7375,9 @@ package Einfo is 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 diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index a18b874fbe1..4fe6c57a5bd 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -3565,12 +3565,13 @@ package body Sem_Prag is -- 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 @@ -3585,22 +3586,56 @@ package body Sem_Prag is 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;