OpenE2K/gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

einfo.adb (Get_Pragma): Handle the retrieval of delayed pragmas stored in N_Contract nodes.

Browse Source 
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.

From-SVN: r200774
This commit is contained in:
Hristian Kirtchev 2013-07-08 08:19:20 +00:00 committed by Arnaud Charlet
parent 5884c23204
commit 78d432da45
4 changed files with 104 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
gcc/ada/ChangeLog
View File

@ -1,3 +1,12 @@
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.

59
gcc/ada/einfo.adb
View File

@ -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;

4
gcc/ada/einfo.ads
View File

@ -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

51
gcc/ada/sem_prag.adb
View File

@ -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;