[Ada] Initial implementation of aspect Ghost

This patch provides the initial implementation of aspect Ghost. This construct
is intended for formal verification proofs.

Aspect Ghost is a boolean aspect with the following semantics:

A function with a Ghost aspect_mark in the aspect_specification of its
declaration may only be called from within an assertion expression, excluding
subtype predicates, or from within another ghost function.

The patch also corrects several issues found in aspect/pragma Loop_Invariant
and Loop_Variant.

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

--  gen.ads

generic
   type Element is private;
   with function Formal_Func (Val : Element) return Element;
package Gen is
end Gen;

--  illegal usage.ads

with Gen;

package Illegal_Usage is
   function Ghost_Func (Val : Integer) return Integer
     with Ghost;

   function Ren_GF_1 (Val : Integer) return Integer renames Ghost_Func;
   function Ren_GF_2 (Val : Integer) return Integer renames Ren_GF_1;

   subtype Nat_Subtype_1 is Natural
     with Dynamic_Predicate => Ghost_Func (Nat_Subtype_1) > 1;
   subtype Nat_Subtype_2 is Natural
     with Dynamic_Predicate => Ren_GF_1 (Nat_Subtype_2) > 1;
   subtype Nat_Subtype_3 is Natural
     with Dynamic_Predicate => Ren_GF_2 (Nat_Subtype_3) > 1;

   package Inst is new Gen (Integer, Ghost_Func);

   type Iface is interface;
   function Func_1 return Iface is abstract;
   function Func_2 return Iface is abstract;

   type Impl_Type is new Iface with null record;
   overriding function Func_1 return Impl_Type
     with Ghost;
   function Func_2 return Impl_Type
     with Ghost;

   procedure Proc;
end Illegal_Usage;

--  illegal_usage.adb

package body Illegal_Usage is
   overriding function Func_1 return Impl_Type is
      Result : Impl_Type;
   begin
      return Result;
   end Func_1;

   function Func_2 return Impl_Type is
   begin
      return Func_1;
   end Func_2;

   function Ghost_Func (Val : Integer) return Integer is
   begin
      return Val + 1;
   end Ghost_Func;

   procedure Proc is
      type Ghost_Func_Ptr is access function (Val : Integer) return Integer;
      Ptr : constant Ghost_Func_Ptr := Ghost_Func'Access;
      Var : Integer;
   begin
      Var := Ghost_Func (1);
      Var := Ren_GF_1 (2);
      Var := Ren_GF_2 (3);
   end Proc;
end Illegal_Usage;

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

$ gcc -c -gnat12 -gnata -gnatd.V illegal_usage.adb
illegal_usage.adb:20:40: prefix of "Access" attribute cannot be a ghost
  function
illegal_usage.adb:23:14: call to ghost function must appear in assertion
  expression or another ghost function
illegal_usage.adb:24:14: call to ghost function must appear in assertion
  expression or another ghost function
illegal_usage.adb:25:14: call to ghost function must appear in assertion
  expression or another ghost function
illegal_usage.ads:11:32: call to ghost function must appear in assertion
  expression or another ghost function
illegal_usage.ads:13:32: call to ghost function must appear in assertion
  expression or another ghost function
illegal_usage.ads:15:32: call to ghost function must appear in assertion
  expression or another ghost function
illegal_usage.ads:17:38: ghost function "Ghost_Func" cannot act as generic
  actual
illegal_usage.ads:17:38: instantiation abandoned
illegal_usage.ads:24:24: ghost function "Func_1" cannot be overriding
illegal_usage.ads:26:13: ghost function "Func_2" cannot be overriding

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

2013-04-12  Hristian Kirtchev  <kirtchev@adacore.com>

	* aspects.adb: Alphabetize subprogram bodies in this unit. Add
	an entry for Aspect_Ghost in the table of canonical aspects.
	(Has_Aspect): New routine.
	* aspects.ads: Add Aspect_Ghost to all relevant
	tables. Alphabetize subprograms in this unit.
	(Has_Aspect): New routine.
	* einfo.adb: Add with and use clauses for Aspects.
	(Is_Ghost_Function): New routine.
	* einfo.ads: Add new synthesized attribute Is_Ghost_Function and
	update the structure of the related nodes.
	(Is_Ghost_Function): New routine.
	* exp_ch4.adb (Find_Enclosing_Context): Use routine
	Is_Body_Or_Package_Declaration to terminate a search.
	(Is_Body_Or_Unit): Removed.
	* exp_util.adb (Within_Case_Or_If_Expression): Use routine
	Is_Body_Or_Package_Declaration to terminate a search.
	* par-prag.adb: Add pragma Ghost to the list of pragmas that do
	not need special processing by the parser.
	* sem_attr.adb (Analyze_Access_Attribute): Detect an
	illegal use of 'Access where the prefix is a ghost function.
	(Analyze_Attribute): Use routine Is_Body_Or_Package_Declaration
	to terminate a search.	(Check_References_In_Prefix): Use routine
	Is_Body_Or_Package_Declaration to terminate a search.
	* sem_ch4.adb (Analyze_Call): Mark a function when it appears
	inside an assertion expression.  Verify the legality of a call
	to a ghost function.
	(Check_Ghost_Function_Call): New routine.
	* sem_ch6.adb (Analyze_Function_Call): Code reformatting. Move
	the setting of attribute In_Assertion_Expression to Analyze_Call.
	(Check_Overriding_Indicator): Detect an illegal attempt to
	override a function with a ghost function.
	* sem_ch12.adb (Preanalyze_Actuals): Detect an illegal use of
	a ghost function as a generic actual.
	* sem_elab.adb (Check_Internal_Call_Continue): Update the call
	to In_Assertion.
	* sem_prag.adb: Add an entry for pragma Ghost in the table
	of significant arguments.
	(Analyze_Pragma): Do not analyze
	an "others" case guard. Add processing for pragma Ghost. Use
	Preanalyze_Assert_Expression when analyzing the expression of
	pragmas Loop_Invariant and Loop_Variant.
	* sem_util.adb (Get_Subprogram_Entity): Reimplemented.
	(Is_Body_Or_Package_Declaration): New routine.
	* sem_util.ads: Alphabetize subprotrams in this unit.
	(Is_Body_Or_Package_Declaration): New routine.
	* sinfo.adb (In_Assertion): Rename to In_Assertion_Expression.
	(Set_In_Assertion): Rename to Set_In_Assertion_Expression.
	* sinfo.ads: Rename flag In_Assertion to In_Assertion_Expression
	to better reflect its use.  Update all places that mention the flag.
	(In_Assertion): Rename to In_Assertion_Expression. Update
	related pragma Inline.	(Set_In_Assertion): Rename to
	Set_In_Assertion_Expression. Update related pragma Inline.
	* snames.ads-tmpl: Add new predefined name Ghost. Add new pragma
	id Pragma_Ghost.

[Ada] Initial implementation of aspect Ghost

Commit Message

Patch