[Ada] Spurious error on withed Ghost unit

This patch modifies the front end to prevent the generation of ALI and object
files as well as bypass the back end and suppress any errors related to code
generation when the compilation unit is ignored Ghost.

------------
-- Source --
------------

--  ignore.adc

pragma Assertion_Policy (Ghost => Ignore);

--  ghost_gen.adb

with Ada.Text_IO; use Ada.Text_IO;

package body Ghost_Gen is
   procedure Ghost_Proc (Formal : T) is
   begin
      if Formal = Ghost_Obj then
         null;
      end if;
      Put_Line ("ERROR: Ghost_Gen");
   end Ghost_Proc;
end Ghost_Gen;

--  ghost_gen.ads

generic
   type T is private;
   Ghost_Obj : T;

package Ghost_Gen with Ghost is
   procedure Ghost_Proc (Formal : T);
end Ghost_Gen;

--  ghost_pack_spec.ads

package Ghost_Pack_Spec with Ghost is
   Ghost_Obj : constant Integer := 1;
end Ghost_Pack_Spec;

--  ghost_pack_spec_and_body.adb

with Ada.Text_IO; use Ada.Text_IO;

package body Ghost_Pack_Spec_And_Body is
   procedure Ghost_Proc (Formal : Integer) is
   begin
      if Ghost_Obj = Formal then
         null;
      end if;
      Put_Line ("ERROR: Ghost_Pack_Spec_And_Body");
   end Ghost_Proc;
end Ghost_Pack_Spec_And_Body;

--  ghost_pack_spec_and_body.ads

package Ghost_Pack_Spec_And_Body with Ghost is
   Ghost_Obj : constant Integer := 1;

   procedure Ghost_Proc (Formal : Integer);
end Ghost_Pack_Spec_And_Body;

--  ghost_subp_body.adb

with Ada.Text_IO; use Ada.Text_IO;

procedure Ghost_Subp_Body (Formal : Integer) with Ghost is
   Ghost_Obj : Integer := 1;
begin
   if Ghost_Obj = Formal then
      null;
   end if;
   Put_Line ("ERROR: Ghost_Subp_Body");
end Ghost_Subp_Body;

--  ghost_subp_spec_and_body.adb

with Ada.Text_IO; use Ada.Text_IO;

procedure Ghost_Subp_Spec_And_Body (Formal : Integer) is
begin
   Put_Line ("ERROR: Ghost_Subp_Spec_And_Body");
end Ghost_Subp_Spec_And_Body;

--  ghost_subp_spec_and_body.ads

procedure Ghost_Subp_Spec_And_Body (Formal : Integer) with Ghost;

--  living_with_1.adb

with Ghost_Gen;

procedure Living_With_1 is
   package Ghost_Inst is new Ghost_Gen (Integer, 1);
begin
   Ghost_Inst.Ghost_Proc (2);
end Living_With_1;

--  living_with_2.adb

with Ghost_Pack_Spec; use Ghost_Pack_Spec;

procedure Living_With_2 is
   Local_Ghost_Obj : constant Integer := Ghost_Obj with Ghost;
begin
   null;
end Living_With_2;

--  living_with_3.adb

with Ghost_Pack_Spec_And_Body; use Ghost_Pack_Spec_And_Body;

procedure Living_With_3 is
   Local_Ghost_Obj : constant Integer := Ghost_Obj with Ghost;
begin
   Ghost_Proc (Local_Ghost_Obj);
end Living_With_3;

--  living_with_4.adb

with Ghost_Subp_Body;

procedure Living_With_4 is
   Local_Ghost_Obj : constant Integer := 1 with Ghost;
begin
   Ghost_Subp_Body (Local_Ghost_Obj);
end Living_With_4;

--  living_with_5.adb

with Ghost_Subp_Spec_And_Body;

procedure Living_With_5 is
   Local_Ghost_Obj : constant Integer := 1 with Ghost;
begin
   Ghost_Subp_Spec_And_Body (Local_Ghost_Obj);
end Living_With_5;

----------------------------
-- Compilation and output --
----------------------------

$ echo "checked Ghost code, withs from living untis"
$ gcc -c -gnatec=check.adc ghost_gen.adb
$ gcc -c -gnatec=check.adc ghost_pack_spec.ads
$ gcc -c -gnatec=check.adc ghost_pack_spec_and_body.adb
$ gcc -c -gnatec=check.adc ghost_subp_body.adb
$ gcc -c -gnatec=check.adc ghost_subp_spec_and_body.adb
$ gcc -c -gnatec=check.adc living_with_1.adb
$ gcc -c -gnatec=check.adc living_with_2.adb
$ gcc -c -gnatec=check.adc living_with_3.adb
$ gcc -c -gnatec=check.adc living_with_4.adb
$ gcc -c -gnatec=check.adc living_with_5.adb
$ ls *.o *.ali > objects_and_ali.txt
$ grep -n "ghost" objects_and_ali.txt | wc -l
$ rm -rf *.o *.ali
$ echo "ignored Ghost code, withs from living units"
$ gcc -c -gnatec=ignore.adc ghost_gen.adb
$ gcc -c -gnatec=ignore.adc ghost_pack_spec.ads
$ gcc -c -gnatec=ignore.adc ghost_pack_spec_and_body.adb
$ gcc -c -gnatec=ignore.adc ghost_subp_body.adb
$ gcc -c -gnatec=ignore.adc ghost_subp_spec_and_body.adb
$ gcc -c -gnatec=ignore.adc living_with_1.adb
$ gcc -c -gnatec=ignore.adc living_with_2.adb
$ gcc -c -gnatec=ignore.adc living_with_3.adb
$ gcc -c -gnatec=ignore.adc living_with_4.adb
$ gcc -c -gnatec=ignore.adc living_with_5.adb
$ ls *.o *.ali > objects_and_ali.txt
$ grep "ghost" objects_and_ali.txt | wc -l
$ rm -rf *.o *.ali
$ gnatmake -f -q -gnatec=ignore.adc living_with_1.adb
$ gnatmake -f -q -gnatec=ignore.adc living_with_2.adb
$ gnatmake -f -q -gnatec=ignore.adc living_with_3.adb
$ gnatmake -f -q -gnatec=ignore.adc living_with_4.adb
$ gnatmake -f -q -gnatec=ignore.adc living_with_5.adb
$ ./living_with_1
$ ./living_with_2
$ ./living_with_3
$ ./living_with_4
$ ./living_with_5
checked Ghost code, withs from living untis
10
ignored Ghost code, withs from living units
0

Tested on x86_64-pc-linux-gnu, committed on trunk

2016-07-06  Hristian Kirtchev  <kirtchev@adacore.com>

	* gnat1drv.adb: Code clean up. Do not emit any
	code generation errors when the unit is ignored Ghost.

[Ada] Spurious error on withed Ghost unit

Commit Message

Patch