2014-10-31 Hristian Kirtchev <kirtchev@adacore.com>

	* aspects.adb Add an entry for aspect Ghost in table
	Canonical_Aspect.
	* aspects.ads Add an entry for aspect Ghost in tables
	Aspect_Argument, Aspect_Delay, Aspect_Id, Aspect_Names and
	Implementation_Defined_Aspect.
	* einfo.adb: Flags 277 and 278 are now in use.
	(Is_Checked_Ghost_Entity): New routine.
	(Is_Ghost_Entity): Removed.
	(Is_Ghost_Subprogram): Removed.
	(Is_Ignored_Ghost_Entity): New routine.
	(Set_Is_Checked_Ghost_Entity): New routine.
	(Set_Is_Ignored_Ghost_Entity): New routine.
	(Write_Entity_Flags): Output flags Is_Checked_Ghost_Entity and
	Is_Ignored_Ghost_Entity.
	* einfo.ads: Add new flags Is_Checked_Ghost_Entity
	and Is_Ignored_Ghost_Entity along with usage in nodes.
	(Is_Checked_Ghost_Entity): New routine and pragma Inline.
	(Is_Ghost_Entity): Removed along with synthesized flag
	description and usage in nodes.
	(Is_Ghost_Subprogram): Removed along with synthesized flag description
	and usage in nodes.
	(Is_Ignored_Ghost_Entity): New routine and pragma Inline.
	(Set_Is_Checked_Ghost_Entity): New routine and pragma Inline.
	(Set_Is_Ignored_Ghost_Entity): New routine and pragma Inline.
	* freeze.adb (Freeze_Entity): A Ghost type cannot be effectively
	volatile.
	* par-prag.adb Pragma Ghost does not need special handling by
	the parser.
	* repinfo.adb (List_Mechanisms): Remove the entry for convention Ghost.
	* sem_attr.adb (Analyze_Access_Attribute): Remove obsolete check.
	* sem_ch3.adb (Analyze_Full_Type_Declaration): Mark
	the type as Ghost when its enclosing context is Ghost.
	(Analyze_Incomplete_Type_Decl): Mark the type as Ghost when
	its enclosing context is Ghost.
	(Analyze_Number_Declaration): Mark the number as Ghost when its
	enclosing context is Ghost.
	(Analyze_Object_Declaration): Mark the object as Ghost when its
	enclosing context is Ghost. Verify the Ghost policy between
	initial declaration and completion of a deferred constant.
	(Analyze_Object_Contract): A Ghost variable cannot be effectively
	volatile, imported or exported.
	(Build_Derived_Record_Type): Mark a type extension as Ghost when it
	implements a Ghost interface.
	(Build_Record_Type): Inherit volatility and "ghostness" from
	the parent type.
	(Check_Completion): A Ghost entity declared
	in a non-Ghost package does not require completion in a body.
	(Implements_Ghost_Interface): New routine.
	(Process_Full_View): Inherit "ghostness" from the partial view. Verify
	the Ghost policy between the partial and full views. Verify the
	completion of a Ghost type extension.
	* sem_ch4.adb (Check_Ghost_Subprogram_Call): Removed.
	* sem_ch5.adb (Analyze_Assignment): Analyze the left hand side first.
	* sem_ch6.adb (Analyze_Abstract_Subprogram_Declaration): Mark
	the subprogram as Ghost when its enclosing context is Ghost.
	(Analyze_Generic_Subprogram_Body): Mark the generic body as Ghost
	when its enclosing context is Ghost. Verify the Ghost policy
	between the spec and body.
	(Analyze_Subprogram_Body_Helper): Mark the body as Ghost when its
	enclosing context is Ghost. Verify the Ghost policy between the spec
	and body.
	(Check_Conformance): A Ghost subprogram profile and a non-Ghost
	subprogram profile are not subtype conformant.
	(Convention_Of): Removed.
	* sem_ch7.adb (Analyze_Package_Body_Helper): Inherit the
	"ghostness" from the spec. Verify the Ghost policy between
	the spec and body.
	(Analyze_Private_Type_Declaration): Mark the type as Ghost when its
	enclosing context is Ghost.
	(Requires_Completion_In_Body): New routine.
	(Unit_Requires_Body): Use Requires_Completion_In_Body.
	(Unit_Requires_Body_Info): Rename formal parameter P to Pack_Id, update
	comment on usage and all uses of P in the body. Use
	Requires_Completion_In_Body.
	* sem_ch7.ads (Unit_Requires_Body): Rename formal parameter P
	to Pack_Id, update comment on usage and all uses of P in the body.
	* sem_ch8.adb (Analyze_Exception_Renaming): Inherit the "ghostness"
	from the renamed excention.
	(Analyze_Generic_Renaming): Inherit the "ghostness" from the
	renamed generic subprogram.
	(Analyze_Object_Renaming): Inherit the "ghostness" from the renamed
	object.
	(Analyze_Package_Renaming): Inherit the "ghostness" from the
	renamed package.
	(Analyze_Subprogram_Renaming): Inherit the "ghostness" from the
	renamed subprogram.
	* sem_ch11.adb (Analyze_Exception_Declaration): Mark an exception
	as Ghost when its enclosing context is Ghost.
	* sem_ch12.adb (Analyze_Generic_Package_Declaration,
	Analyze_Generic_Subprogram_Declaration): Mark an exception as
	Ghost when its enclosing context is Ghost.
	(Preanalyze_Actuals): Remove obsolete check.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Add processing
	for aspect Ghost.
	(Check_Aspect_At_Freeze_Point): Aspects
	Depends and Global do no need special checking at freeze point.
	(Insert_After_SPARK_Mode): Update comment on usage.
	* sem_mech.adb (Set_Mechanisms): Remove the entry for convention Ghost.
	* sem_prag.adb Add an entry for pragma Ghost in table Sig_Flags.
	(Analyze_Abstract_State): Update the grammar of the pragma. Add
	formal parameter Pack_Id along with comment on usage. Mark an
	abstract state as Ghost when its enclosing context is Ghost. Add
	processing for option Ghost.
	(Analyze_Constituent): Verify
	that a Ghost abstract state is refined by Ghost constituents.
	(Analyze_Pragma): "Ghost" is now a valid policy. Add checks
	related to the use and placement of Check_Policy Ghost. Add
	processing for pragma Ghost.
	(Check_Ghost_Constituent): New routine.
	(Is_Valid_Assertion_Kind): "Ghost" is now a valid assertion.
	(Process_Convention): Remove obsolete check.
	(Set_Convention_From_Pragma): Remove the processing for convention
	Ghost.
	* sem_res.adb (Check_Ghost_Context): New routine.
	(Resolve_Call): Verify that a reference to a Ghost entity appears in a
	suitable context. Verify the Ghost polity between point of declaration
	and point of use.
	(Resolve_Entity_Name): Verify that a reference to
	a Ghost entity appears in a suitable context. Verify the Ghost
	polity between point of declaration and point of use.
	* sem_util.adb (Check_Ghost_Completion): New routine.
	(Check_Ghost_Derivation): New routine.
	(Incomplete_Or_Partial_View): New routine.
	(Incomplete_Or_Private_View): Removed.
	(Is_Ghost_Entity): New routine.
	(Is_Ghost_Statement_Or_Pragma): New routine.
	(Is_Subject_To_Ghost): New routine.
	(Policy_In_Effect): New routine.
	(Set_Is_Ghost_Entity): New routine.
	(Within_Ghost_Scope): New routine.
	* sem_util.ads (Check_Ghost_Completion): New routine.
	(Check_Ghost_Derivation): New routine.
	(Incomplete_Or_Partial_View): New routine.
	(Incomplete_Or_Private_View): Removed.
	(Is_Ghost_Entity): New routine.
	(Is_Ghost_Statement_Or_Pragma): New routine.
	(Is_Subject_To_Ghost): New routine.
	(Policy_In_Effect): New routine.
	(Set_Is_Ghost_Entity): New routine.
	(Within_Ghost_Scope): New routine.
	* snames.adb-tmpl (Get_Convention_Id): Remove the entry for
	convention Ghost.
	(Get_Convention_Name): Remove the entry for convention Ghost.
	* snames.ads-tmpl Remove the convention id for Ghost. Add a
	pragma id for Ghost.

2014-10-31  Sergey Rybin  <rybin@adacore.com frybin>

	* gnat_ugn.texi: Add description of --RTS option for ASIS tools.

From-SVN: r216981

1 files changed, 234 insertions, 27 deletions

diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 97f6ea1..893e1e1 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -109,6 +109,10 @@ package body Sem_Res is
       Pref : Node_Id);
    --  Check that the type of the prefix of a dereference is not incomplete
 
+   procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id);
+   --  Determine whether node Ghost_Ref appears within a Ghost-friendly context
+   --  where Ghost entity Ghost_Id can safely reside.
+
    function Check_Infinite_Recursion (N : Node_Id) return Boolean;
    --  Given a call node, N, which is known to occur immediately within the
    --  subprogram being called, determines whether it is a detectable case of
@@ -688,6 +692,193 @@ package body Sem_Res is
       end if;
    end Check_Fully_Declared_Prefix;
 
+   -------------------------
+   -- Check_Ghost_Context --
+   -------------------------
+
+   procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id) is
+      procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : Node_Id);
+      --  Verify that the Ghost policy at the point of declaration of entity Id
+      --  matches the policy at the point of reference. If this is not the case
+      --  emit an error at Err_N.
+
+      function Is_OK_Ghost_Context (Context : Node_Id) return Boolean;
+      --  Determine whether node Context denotes a Ghost-friendly context where
+      --  a Ghost entity can safely reside.
+
+      -------------------------
+      -- Is_OK_Ghost_Context --
+      -------------------------
+
+      function Is_OK_Ghost_Context (Context : Node_Id) return Boolean is
+         function Is_Ghost_Declaration (Decl : Node_Id) return Boolean;
+         --  Determine whether node Decl is a Ghost declaration or appears
+         --  within a Ghost declaration.
+
+         --------------------------
+         -- Is_Ghost_Declaration --
+         --------------------------
+
+         function Is_Ghost_Declaration (Decl : Node_Id) return Boolean is
+            Par       : Node_Id;
+            Subp_Decl : Node_Id;
+            Subp_Id   : Entity_Id;
+
+         begin
+            --  Climb the parent chain looking for an object declaration
+
+            Par := Decl;
+            while Present (Par) loop
+               case Nkind (Par) is
+                  when N_Abstract_Subprogram_Declaration        |
+                       N_Exception_Declaration                  |
+                       N_Exception_Renaming_Declaration         |
+                       N_Full_Type_Declaration                  |
+                       N_Generic_Function_Renaming_Declaration  |
+                       N_Generic_Package_Declaration            |
+                       N_Generic_Package_Renaming_Declaration   |
+                       N_Generic_Procedure_Renaming_Declaration |
+                       N_Generic_Subprogram_Declaration         |
+                       N_Number_Declaration                     |
+                       N_Object_Declaration                     |
+                       N_Object_Renaming_Declaration            |
+                       N_Package_Declaration                    |
+                       N_Package_Renaming_Declaration           |
+                       N_Private_Extension_Declaration          |
+                       N_Private_Type_Declaration               |
+                       N_Subprogram_Declaration                 |
+                       N_Subprogram_Renaming_Declaration        |
+                       N_Subtype_Declaration                    =>
+                     return Is_Subject_To_Ghost (Par);
+
+                  when others                                   =>
+                     null;
+               end case;
+
+               --  Special cases
+
+               --  A reference to a Ghost entity may appear as the default
+               --  expression of a formal parameter of a subprogram body. This
+               --  context must be treated as suitable because the relation
+               --  between the spec and the body has not been established and
+               --  the body is not marked as Ghost yet. The real check was
+               --  performed on the spec.
+
+               if Nkind (Par) = N_Parameter_Specification
+                 and then Nkind (Parent (Parent (Par))) = N_Subprogram_Body
+               then
+                  return True;
+
+               --  References to Ghost entities may be relocated in internally
+               --  generated bodies.
+
+               elsif Nkind (Par) = N_Subprogram_Body
+                 and then not Comes_From_Source (Par)
+               then
+                  Subp_Id := Corresponding_Spec (Par);
+
+                  --  The original context is an expression function that has
+                  --  been split into a spec and a body. The context is OK as
+                  --  long as the the initial declaration is Ghost.
+
+                  if Present (Subp_Id) then
+                     Subp_Decl :=
+                       Original_Node (Unit_Declaration_Node (Subp_Id));
+
+                     if Nkind (Subp_Decl) = N_Expression_Function then
+                        return Is_Subject_To_Ghost (Subp_Decl);
+                     end if;
+                  end if;
+
+                  --  Otherwise this is either an internal body or an internal
+                  --  completion. Both are OK because the real check was done
+                  --  before expansion activities.
+
+                  return True;
+               end if;
+
+               --  Prevent the search from going too far
+
+               if Is_Body_Or_Package_Declaration (Par) then
+                  return False;
+               end if;
+
+               Par := Parent (Par);
+            end loop;
+
+            return False;
+         end Is_Ghost_Declaration;
+
+      --  Start of processing for Is_OK_Ghost_Context
+
+      begin
+         --  The Ghost entity appears within an assertion expression
+
+         if In_Assertion_Expr > 0 then
+            return True;
+
+         --  The Ghost entity is part of a declaration or its completion
+
+         elsif Is_Ghost_Declaration (Context) then
+            return True;
+
+         --  The Ghost entity is referenced within a Ghost statement
+
+         elsif Is_Ghost_Statement_Or_Pragma (Context) then
+            return True;
+
+         else
+            return False;
+         end if;
+      end Is_OK_Ghost_Context;
+
+      ------------------------
+      -- Check_Ghost_Policy --
+      ------------------------
+
+      procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : Node_Id) is
+         Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
+
+      begin
+         --  The Ghost policy in effect a the point of declaration and at the
+         --  point of use must match (SPARK RM 6.9(13)).
+
+         if Is_Checked_Ghost_Entity (Id) and then Policy = Name_Ignore then
+            Error_Msg_Sloc := Sloc (Err_N);
+
+            SPARK_Msg_N  ("incompatible ghost policies in effect", Err_N);
+            SPARK_Msg_NE ("\& declared with ghost policy Check", Err_N, Id);
+            SPARK_Msg_NE ("\& used # with ghost policy Ignore", Err_N, Id);
+
+         elsif Is_Ignored_Ghost_Entity (Id) and then Policy = Name_Check then
+            Error_Msg_Sloc := Sloc (Err_N);
+
+            SPARK_Msg_N  ("incompatible ghost policies in effect", Err_N);
+            SPARK_Msg_NE ("\& declared with ghost policy Ignore", Err_N, Id);
+            SPARK_Msg_NE ("\& used # with ghost policy Check", Err_N, Id);
+         end if;
+      end Check_Ghost_Policy;
+
+   --  Start of processing for Check_Ghost_Context
+
+   begin
+      --  Once it has been established that the reference to the Ghost entity
+      --  is within a suitable context, ensure that the policy at the point of
+      --  declaration and at the point of use match.
+
+      if Is_OK_Ghost_Context (Ghost_Ref) then
+         Check_Ghost_Policy (Ghost_Id, Ghost_Ref);
+
+      --  Otherwise the Ghost entity appears in a non-Ghost context and affects
+      --  its behavior or value.
+
+      else
+         SPARK_Msg_N
+           ("ghost entity cannot appear in this context (SPARK RM 6.9(12))",
+            Ghost_Ref);
+      end if;
+   end Check_Ghost_Context;
+
    ------------------------------
    -- Check_Infinite_Recursion --
    ------------------------------
@@ -5545,9 +5736,9 @@ package body Sem_Res is
       end if;
 
       if Is_Access_Subprogram_Type (Base_Type (Etype (Nam)))
-         and then not Is_Access_Subprogram_Type (Base_Type (Typ))
-         and then Nkind (Subp) /= N_Explicit_Dereference
-         and then Present (Parameter_Associations (N))
+        and then not Is_Access_Subprogram_Type (Base_Type (Typ))
+        and then Nkind (Subp) /= N_Explicit_Dereference
+        and then Present (Parameter_Associations (N))
       then
          --  The prefix is a parameterless function call that returns an access
          --  to subprogram. If parameters are present in the current call, add
@@ -5808,6 +5999,12 @@ package body Sem_Res is
       Set_Is_Overloaded (Subp, False);
       Set_Is_Overloaded (N, False);
 
+      --  A Ghost entity must appear in a specific context
+
+      if Is_Ghost_Entity (Nam) and then Comes_From_Source (N) then
+         Check_Ghost_Context (Nam, N);
+      end if;
+
       --  If we are calling the current subprogram from immediately within its
       --  body, then that is the case where we can sometimes detect cases of
       --  infinite recursion statically. Do not try this in case restriction
@@ -6855,38 +7052,48 @@ package body Sem_Res is
          Par := Parent (Par);
       end if;
 
-      --  An effectively volatile object subject to enabled properties
-      --  Async_Writers or Effective_Reads must appear in a specific context.
       --  The following checks are only relevant when SPARK_Mode is on as they
       --  are not standard Ada legality rules.
 
-      if SPARK_Mode = On
-        and then Is_Object (E)
-        and then Is_Effectively_Volatile (E)
-        and then Comes_From_Source (E)
-        and then
-          (Async_Writers_Enabled (E) or else Effective_Reads_Enabled (E))
-      then
-         --  The effectively volatile objects appears in a "non-interfering
-         --  context" as defined in SPARK RM 7.1.3(13).
+      if SPARK_Mode = On then
 
-         if Is_OK_Volatile_Context (Par, N) then
-            null;
+         --  An effectively volatile object subject to enabled properties
+         --  Async_Writers or Effective_Reads must appear in a specific
+         --  context.
+
+         if Is_Object (E)
+           and then Is_Effectively_Volatile (E)
+           and then
+             (Async_Writers_Enabled (E) or else Effective_Reads_Enabled (E))
+           and then Comes_From_Source (N)
+         then
+            --  The effectively volatile objects appears in a "non-interfering
+            --  context" as defined in SPARK RM 7.1.3(13).
 
-         --  Assume that references to effectively volatile objects that appear
-         --  as actual parameters in a procedure call are always legal. A full
-         --  legality check is done when the actuals are resolved.
+            if Is_OK_Volatile_Context (Par, N) then
+               null;
 
-         elsif Nkind (Par) = N_Procedure_Call_Statement then
-            null;
+            --  Assume that references to effectively volatile objects that
+            --  appear as actual parameters in a procedure call are always
+            --  legal. A full legality check is done when the actuals are
+            --  resolved.
 
-         --  Otherwise the context causes a side effect with respect to the
-         --  effectively volatile object.
+            elsif Nkind (Par) = N_Procedure_Call_Statement then
+               null;
 
-         else
-            Error_Msg_N
-              ("volatile object cannot appear in this context "
-               & "(SPARK RM 7.1.3(13))", N);
+            --  Otherwise the context causes a side effect with respect to the
+            --  effectively volatile object.
+
+            else
+               SPARK_Msg_N
+                 ("volatile object cannot appear in this context "
+                  & "(SPARK RM 7.1.3(13))", N);
+            end if;
+
+         --  A Ghost entity must appear in a specific context
+
+         elsif Is_Ghost_Entity (E) and then Comes_From_Source (N) then
+            Check_Ghost_Context (E, N);
          end if;
       end if;
    end Resolve_Entity_Name;