This patch implements context clauses for Ghost compilation units. It is now possible to "with" and "use" a Ghost unit. If the Assertion_Policy for Ghost is set to "Ignore", the Ghost compilation units do not generate ALI or object files, and no cross-referencing information is present in living ALI files.
------------ -- Source -- ------------ -- checked.adc pragma Assertion_Policy (Ghost => Check); -- ignored.adc pragma Assertion_Policy (Ghost => Ignore); -- g.ads package G with Ghost is G_Obj : Integer := 1; procedure Force_Body; end G; with Ada.Text_IO; use Ada.Text_IO; package body G is procedure Force_Body is G_Obj_2 : constant Integer := 2; begin null; end Force_Body; begin Put_Line ("G"); end G; -- gp.ads procedure GP with Ghost; -- gp.adb with Ada.Text_IO; use Ada.Text_IO; procedure GP is begin Put_Line ("GP"); end GP; -- gparent.ads package Gparent with Ghost is procedure Force_Body; end Gparent; -- gparent.adb with Ada.Text_IO; use Ada.Text_IO; package body Gparent is procedure Force_Body is begin null; end Force_Body; begin Put_Line ("Gparent"); end Gparent; -- gparent-lchild.ads package Gparent.Lchild is procedure Force_Body; end Gparent.Lchild; -- gparent-lchild.adb with Ada.Text_IO; use Ada.Text_IO; package body Gparent.Lchild is procedure Force_Body is begin null; end Force_Body; begin Put_Line ("Gparent.Lchild"); end Gparent.Lchild; -- g_withs_g.ads with G; use G; with GP; package G_Withs_G with Ghost is GWG_Obj : Integer := G_Obj; procedure Force_Body; end G_Withs_G; -- g_withs_g.adb with Ada.Text_IO; use Ada.Text_IO; package body G_Withs_G is procedure Force_Body is begin G_Obj := G_Obj + 1; end Force_Body; begin Put_Line ("G_Withs_G"); GP; end G_Withs_G; -- g_withs_g_withs_g.ads with G_Withs_G; use G_Withs_G; package G_Withs_G_Withs_G with Ghost is GWGWG_Obj : Integer := GWG_Obj; procedure Force_Body; end G_Withs_G_Withs_G; -- g_withs_g_withs_g.adb with Ada.Text_IO; use Ada.Text_IO; package body G_Withs_G_Withs_G is procedure Force_Body is begin GWG_Obj := GWG_Obj + 1; end Force_Body; begin Put_Line ("G_Withs_G_Withs_G"); end G_Withs_G_Withs_G; -- g_withs_g_withs_l.ads with G_Withs_L; use G_Withs_L; package G_Withs_G_Withs_L with Ghost is GWGWL_Obj : Integer := GWL_Obj; procedure Force_Body; end G_Withs_G_Withs_L; -- g_withs_g_withs_l.adb with Ada.Text_IO; use Ada.Text_IO; package body G_Withs_G_Withs_L is procedure Force_Body is begin GWL_Obj := GWL_Obj + 1; end Force_Body; begin Put_Line ("G_Withs_G_Withs_L"); end G_Withs_G_Withs_L; -- g_withs_l.ads with L; use L; with LP; package G_Withs_L with Ghost is GWL_Obj : Integer := L_Obj; procedure Force_Body; end G_Withs_L; -- g_withs_l.adb with Ada.Text_IO; use Ada.Text_IO; package body G_Withs_L is procedure Force_Body is begin L_Obj := L_Obj + 1; end Force_Body; begin Put_Line ("G_Withs_L"); LP; end G_Withs_L; -- g_withs_l_withs_g.ads with L_Withs_G; use L_Withs_G; package G_Withs_L_Withs_G with Ghost is GWLWG_Obj : Integer := LWG_Obj; procedure Force_Body; end G_Withs_L_Withs_G; -- g_withs_l_withs_g.adb with Ada.Text_IO; use Ada.Text_IO; package body G_Withs_L_Withs_G is procedure Force_Body is begin LWG_Obj := LWG_Obj + 1; end Force_Body; begin Put_Line ("G_Withs_L_Withs_G"); end G_Withs_L_Withs_G; -- g_withs_l_withs_l.ads with L_Withs_L; use L_Withs_L; package G_Withs_L_Withs_L with Ghost is GWLWL_Obj : Integer := LWL_Obj; procedure Force_Body; end G_Withs_L_Withs_L; -- g_withs_l_withs_l.adb with Ada.Text_IO; use Ada.Text_IO; package body G_Withs_L_Withs_L is procedure Force_Body is begin LWL_Obj := LWL_Obj + 1; end Force_Body; begin Put_Line ("G_Withs_L_Withs_L"); end G_Withs_L_Withs_L; -- l.ads package L is L_Obj : Integer := 1; procedure Force_Body; end L; -- l.adb with Ada.Text_IO; use Ada.Text_IO; package body L is procedure Force_Body is L_Obj_2 : constant Integer := 2; begin null; end Force_Body; begin Put_Line ("L"); end L; -- lp.ads procedure LP; -- lp.adb with Ada.Text_IO; use Ada.Text_IO; procedure LP is begin Put_Line ("LP"); end LP; -- l_withs_g.ads with G; use G; with GP; package L_Withs_G is LWG_Obj : Integer := G_Obj with Ghost; procedure Force_Body; end L_Withs_G; -- l_withs_g.adb with Ada.Text_IO; use Ada.Text_IO; package body L_Withs_G is procedure Force_Body is begin G_Obj := G_Obj + 1; end Force_Body; begin Put_Line ("L_Withs_G"); GP; end L_Withs_G; -- l_withs_g_withs_g.ads with G_Withs_G; use G_Withs_G; package L_Withs_G_Withs_G is LWGWG_Obj : Integer := GWG_Obj with Ghost; procedure Force_Body; end L_Withs_G_Withs_G; -- l_withs_g_withs_g.adb with Ada.Text_IO; use Ada.Text_IO; package body L_Withs_G_Withs_G is procedure Force_Body is begin GWG_Obj := GWG_Obj + 1; end Force_Body; begin Put_Line ("L_Withs_G_Withs_G"); end L_Withs_G_Withs_G; -- l_withs_g_withs_l.ads with G_Withs_L; use G_Withs_L; package L_Withs_G_Withs_L is LWGWL_Obj : Integer := GWL_Obj with Ghost; procedure Force_Body; end L_Withs_G_Withs_L; -- l_withs_g_withs_l.adb with Ada.Text_IO; use Ada.Text_IO; package body L_Withs_G_Withs_L is procedure Force_Body is begin GWL_Obj := GWL_Obj + 1; end Force_Body; begin Put_Line ("L_Withs_G_Withs_L"); end L_Withs_G_Withs_L; -- l_withs_l.ads with L; use L; with LP; package L_Withs_L is LWL_Obj : Integer := L_Obj; procedure Force_Body; end L_Withs_L; -- l_withs_l.adb with Ada.Text_IO; use Ada.Text_IO; package body L_Withs_L is procedure Force_Body is begin L_Obj := L_Obj + 1; end Force_Body; begin Put_Line ("L_Withs_L"); LP; end L_Withs_L; -- l_withs_l_withs_g.ads with L_Withs_G; use L_Withs_G; package L_Withs_L_Withs_G is LWLWG_Obj : Integer := LWG_Obj with Ghost; procedure Force_Body; end L_Withs_L_Withs_G; -- l_withs_l_withs_g.adb with Ada.Text_IO; use Ada.Text_IO; package body L_Withs_L_Withs_G is procedure Force_Body is begin LWG_Obj := LWG_Obj + 1; end Force_Body; begin Put_Line ("L_Withs_L_Withs_G"); end L_Withs_L_Withs_G; -- with_main.adb with G; with G_Withs_G; with G_Withs_L; with G_Withs_G_Withs_G; with G_Withs_G_Withs_L; with G_Withs_L_Withs_G; with G_Withs_L_Withs_L; with L; with L_Withs_G; with L_Withs_G_Withs_G; with L_Withs_G_Withs_L; with L_Withs_L_Withs_G; with Gparent; with Gparent.Lchild; procedure With_Main is begin null; end With_Main; ---------------------------- -- Compilation and output -- ---------------------------- $ gnatmake -q -f -gnatec=checked.adc with_main.adb $ echo "-- Checked output ---" $ ./with_main $ echo "--- Checked object files ---" $ ls *.o $ echo "--- Checked ALI files ---" $ ls *.ali $ rm *.o *.ali $ gnatmake -q -f -gnatec=ignored.adc with_main.adb $ echo "--- Ignored output ---" $ ./with_main $ echo "--- Ignored object files ---" $ ls *.o $ echo "--- Ignored ALI files ---" $ ls *.ali -- Checked output --- G G_Withs_G GP G_Withs_G_Withs_G Gparent Gparent.Lchild L L_Withs_G GP G_Withs_L_Withs_G L_Withs_G_Withs_G L_Withs_L_Withs_G G_Withs_L LP G_Withs_G_Withs_L L_Withs_G_Withs_L L_Withs_L LP G_Withs_L_Withs_L --- Checked object files --- g.o gparent-lchild.o gparent.o gp.o g_withs_g.o g_withs_g_withs_g.o g_withs_g_withs_l.o g_withs_l.o g_withs_l_withs_g.o g_withs_l_withs_l.o l.o lp.o l_withs_g.o l_withs_g_withs_g.o l_withs_g_withs_l.o l_withs_l.o l_withs_l_withs_g.o with_main.o --- Checked ALI files --- g.ali gp.ali gparent.ali gparent-lchild.ali g_withs_g.ali g_withs_g_withs_g.ali g_withs_g_withs_l.ali g_withs_l.ali g_withs_l_withs_g.ali g_withs_l_withs_l.ali l.ali lp.ali l_withs_g.ali l_withs_g_withs_g.ali l_withs_g_withs_l.ali l_withs_l.ali l_withs_l_withs_g.ali with_main.ali --- Ignored output --- L L_Withs_G L_Withs_G_Withs_G L_Withs_G_Withs_L L_Withs_L_Withs_G --- Ignored object files --- l.o l_withs_g.o l_withs_g_withs_g.o l_withs_g_withs_l.o l_withs_l_withs_g.o with_main.o --- Ignored ALI files --- l.ali l_withs_g.ali l_withs_g_withs_g.ali l_withs_g_withs_l.ali l_withs_l_withs_g.ali with_main.ali Tested on x86_64-pc-linux-gnu, committed on trunk 2016-04-19 Hristian Kirtchev <kirtc...@adacore.com> * lib-writ.adb (Write_With_Lines): Code cleanup. Do not generate a with line for an ignored Ghost unit. * sem_ch7.adb (Analyze_Package_Declaration): Add local constant Par. A child package is Ghost when its parent is Ghost. * sem_prag.adb (Analyze_Pragma): Pragma Ghost can now apply to a subprogram declaration that acts as a compilation unit.
Index: sem_ch7.adb =================================================================== --- sem_ch7.adb (revision 235116) +++ sem_ch7.adb (working copy) @@ -937,7 +937,8 @@ --------------------------------- procedure Analyze_Package_Declaration (N : Node_Id) is - Id : constant Node_Id := Defining_Entity (N); + Id : constant Node_Id := Defining_Entity (N); + Par : constant Node_Id := Parent_Spec (N); Body_Required : Boolean; -- True when this package declaration requires a corresponding body @@ -972,10 +973,13 @@ Set_SPARK_Aux_Pragma_Inherited (Id); end if; - -- A package declared within a Ghost refion is automatically Ghost - -- (SPARK RM 6.9(2)). + -- A package declared within a Ghost refion is automatically Ghost. A + -- child package is Ghost when its parent is Ghost (SPARK RM 6.9(2)). - if Ghost_Mode > None then + if Ghost_Mode > None + or else (Present (Par) + and then Is_Ghost_Entity (Defining_Entity (Unit (Par)))) + then Set_Is_Ghost_Entity (Id); end if; Index: lib-writ.adb =================================================================== --- lib-writ.adb (revision 235093) +++ lib-writ.adb (working copy) @@ -747,16 +747,16 @@ ---------------------- procedure Write_With_Lines is - With_Table : Unit_Ref_Table (1 .. Pos (Last_Unit - Units.First + 1)); - Num_Withs : Int := 0; - Unum : Unit_Number_Type; - Cunit : Node_Id; - Uname : Unit_Name_Type; - Fname : File_Name_Type; Pname : constant Unit_Name_Type := Get_Parent_Spec_Name (Unit_Name (Main_Unit)); Body_Fname : File_Name_Type; Body_Index : Nat; + Cunit : Node_Id; + Fname : File_Name_Type; + Num_Withs : Int := 0; + Unum : Unit_Number_Type; + Uname : Unit_Name_Type; + With_Table : Unit_Ref_Table (1 .. Pos (Last_Unit - Units.First + 1)); procedure Write_With_File_Names (Nam : in out File_Name_Type; @@ -814,11 +814,19 @@ Sort (With_Table (1 .. Num_Withs)); for J in 1 .. Num_Withs loop - Unum := With_Table (J); - Cunit := Units.Table (Unum).Cunit; - Uname := Units.Table (Unum).Unit_Name; - Fname := Units.Table (Unum).Unit_File_Name; + Unum := With_Table (J); + -- Do not generate a with line for an ignored Ghost unit because + -- the unit does not have an ALI file. + + if Is_Ignored_Ghost_Entity (Cunit_Entity (Unum)) then + goto Next_With_Line; + end if; + + Cunit := Units.Table (Unum).Cunit; + Uname := Units.Table (Unum).Unit_Name; + Fname := Units.Table (Unum).Unit_File_Name; + if Implicit_With (Unum) = Yes then Write_Info_Initiate ('Z'); @@ -914,6 +922,9 @@ end if; Write_Info_EOL; + + <<Next_With_Line>> + null; end loop; -- Finally generate the special lines for cases of Restriction_Set @@ -932,7 +943,7 @@ for U in 0 .. Last_Unit loop if Unit_Name (U) = Unam then - goto Continue; + goto Next_Restriction_Set; end if; end loop; @@ -943,7 +954,7 @@ Write_Info_Name (Unam); Write_Info_EOL; - <<Continue>> + <<Next_Restriction_Set>> null; end loop; end; @@ -996,8 +1007,8 @@ end if; end if; - -- Otherwise acquire compilation arguments and prepare to write - -- out a new ali file. + -- Otherwise acquire compilation arguments and prepare to write out a + -- new ali file. Create_Output_Library_Info; Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 235146) +++ sem_prag.adb (working copy) @@ -15063,6 +15063,12 @@ and then No (Corresponding_Spec (Context)) then Id := Defining_Entity (Context); + + -- Pragma Ghost applies to a subprogram declaration that acts + -- as a compilation unit. + + elsif Nkind (Context) = N_Subprogram_Declaration then + Id := Defining_Entity (Context); end if; end if;