[Ada] Withing Ghost units

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