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;
