[Ada] Detection of lingering ignored Ghost code

This patch updates the generation of external symbol names to add a special
prefix for ignored Ghost entities. The prefix aids in the detection of leaking
ignored Ghost code in object/binary files. The reproducer showcases the usage.

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

--  pack_pre.ads

package Pack_Pre is
   procedure Proc (Val : Natural)
     with Pre => Is_Zero (Val);

   procedure Proc2 (Val : Natural)
     with Pre => Is_Zero (Val),
          Ghost;

   function Is_Zero (Val : Natural) return Boolean
     with Ghost;
end Pack_Pre

--  pack_pre.adb

package body Pack_Pre is
   procedure Proc (Val : Natural) is begin null; end Proc;
   procedure Proc2 (Val : Natural) is begin null; end Proc2;

   function Is_Zero (Val : Natural) return Boolean is
   begin
      return Val = 0;
   end Is_Zero;
end Pack_Pre;

--  test_pre.adb

with Ada.Text_IO; use Ada.Text_IO;
with Pack_Pre;    use Pack_Pre;

procedure Test_Pre is
begin
   --  Assertion expression with Ghost function call

   begin
      Proc (10);
      Put_Line ("OK");

   exception
      when others => Put_Line ("ERROR 1: policy Pre is Ignore");
   end;

   --  Ghost assertion expression

   begin
      Proc2 (10);
      Put_Line ("OK");

   exception
      when others => Put_Line ("ERROR 2: policy Pre is Ignore");
   end;
end Test_Pre;

--  check_ghost.adc

pragma Assertion_Policy (Ghost => Check, Pre => Check);

--  ignore_ghost.adc

pragma Assertion_Policy (Ghost => Ignore, Pre => Ignore);

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

$ gnatmake -f -q -gnatec=check_ghost.adc -gnatd.5 test_pre.adb
$ objdump -x *.o > checked_ghost.txt
$ grep "ghost" checked_ghost.txt | wc -l
6
$ gnatmake -f -q -gnatec=ignore_ghost.adc test_pre.adb
$ objdump -x *.o > error_ghosts.txt
$ grep "ghost" error_ghosts.txt | wc -l
0
$ ./test_pre
OK
OK

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

2015-10-23  Hristian Kirtchev  <kirtchev@adacore.com>

	* debug.adb: Document the use of debug switch -gnatd.5.
	* einfo.adb: Code reformatting.	(Is_Ghost_Entity): Moved from ghost.adb.
	* einfo.ads New synthesized attribute Is_Ghost_Enity along
	with usage in nodes and pragma Inline.
	(Is_Ghost_Entity: Moved from ghost.ads.
	* exp_ch3.adb Code reformatting.
	(Expand_Freeze_Array_Type): Capture, set and restore the Ghost mode.
	(Expand_Freeze_Class_Wide_Type): Capture, set and restore the
	Ghost mode.
	(Expand_Freeze_Enumeration_Type): Capture, set and
	restore the Ghost mode.
	(Expand_Freeze_Record_Type): Capture, set and restore the Ghost mode.
	* exp_ch6.adb (Expand_Subprogram_Contract): Do not expand the
	contract of an ignored Ghost subprogram.
	* exp_ch13.adb Add with and use clauses for Ghost.
	(Expand_N_Freeze_Entity): Capture, set and restore the Ghost mode.
	* exp_dbug.adb (Get_External_Name): Code reformatting. Add a
	special prefix for ignored Ghost entities or when requested by
	-gnatd.5 for any Ghost entity.
	* exp_dbug.ads Document the use of prefix "_ghost_" for ignored
	Ghost entities.
	* exp_prag.adb (Expand_Pragma_Check): Capture, set and restore the
	Ghost mode.
	(Expand_Pragma_Loop_Variant): Use In_Assertion_Expr
	to signal the original context.
	* ghost.adb (Check_Ghost_Overriding): Code cleanup.
	(Is_Ghost_Entity): Moved to einfo.adb.	(Is_OK_Declaration):
	Move the assertion expression check to the outer level.
	(Is_OK_Ghost_Context): An assertion expression is a valid Ghost
	context.
	* ghost.ads (Is_Ghost_Entity): Moved to einfo.ads.
	* sem_ch3.adb (Analyze_Object_Contract): A source Ghost object
	cannot be imported or exported. Mark internally generated objects
	as Ghost when applicable.
	(Make_Class_Wide_Type): Inherit the ghostness of the root tagged type.
	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Mark
	a stand alone subprogram body as Ghost when applicable.
	(Analyze_Subprogram_Declaration): Mark internally generated
	subprograms as Ghost when applicable.
	* sem_ch7.adb: Code cleanup.
	* sem_ch13.adb (Add_Invariants): Add various formal
	parameters to break dependency on global variables.
	(Build_Invariant_Procedure): Code cleanup. Capture, set and
	restore the Ghost mode.
	* sem_res.adb (Resolve_Actuals): The actual parameter of a source
	Ghost subprogram whose formal is of mode IN OUT or OUT must be
	a Ghost variable.

[Ada] Detection of lingering ignored Ghost code

Commit Message

Patch