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.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@197909 138bc75d-0d04-0410-961f-82ee72b054a4

19 files changed, 383 insertions, 174 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index e524d1c7a27..80705e94146 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,60 @@
+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.
+
 2013-04-12  Arnaud Charlet  <charlet@adacore.com>
 
 	* sem_prag.adb (Set_Imported): Do not generate error for multiple
diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb
index 2ef728c8476..7799fa83a70 100644
--- a/gcc/ada/aspects.adb
+++ b/gcc/ada/aspects.adb
@@ -110,15 +110,6 @@ package body Aspects is
       end if;
    end Aspect_Specifications;
 
-   -------------------
-   -- Get_Aspect_Id --
-   -------------------
-
-   function Get_Aspect_Id (Name : Name_Id) return Aspect_Id is
-   begin
-      return Aspect_Id_Hash_Table.Get (Name);
-   end Get_Aspect_Id;
-
    -----------------
    -- Find_Aspect --
    -----------------
@@ -169,6 +160,38 @@ package body Aspects is
       return Empty;
    end Find_Aspect;
 
+   -------------------
+   -- Get_Aspect_Id --
+   -------------------
+
+   function Get_Aspect_Id (Name : Name_Id) return Aspect_Id is
+   begin
+      return Aspect_Id_Hash_Table.Get (Name);
+   end Get_Aspect_Id;
+
+   ----------------
+   -- Has_Aspect --
+   ----------------
+
+   function Has_Aspect (Id : Entity_Id; A : Aspect_Id) return Boolean is
+      Decl   : constant Node_Id := Parent (Parent (Id));
+      Aspect : Node_Id;
+
+   begin
+      if Has_Aspects (Decl) then
+         Aspect := First (Aspect_Specifications (Decl));
+         while Present (Aspect) loop
+            if Get_Aspect_Id (Chars (Identifier (Aspect))) = A then
+               return True;
+            end if;
+
+            Next (Aspect);
+         end loop;
+      end if;
+
+      return False;
+   end Has_Aspect;
+
    ------------------
    -- Move_Aspects --
    ------------------
@@ -271,6 +294,7 @@ package body Aspects is
     Aspect_External_Name                => Aspect_External_Name,
     Aspect_External_Tag                 => Aspect_External_Tag,
     Aspect_Favor_Top_Level              => Aspect_Favor_Top_Level,
+    Aspect_Ghost                        => Aspect_Ghost,
     Aspect_Global                       => Aspect_Global,
     Aspect_Implicit_Dereference         => Aspect_Implicit_Dereference,
     Aspect_Import                       => Aspect_Import,
diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads
index 25ce022e0c3..e282f1a6afc 100644
--- a/gcc/ada/aspects.ads
+++ b/gcc/ada/aspects.ads
@@ -161,6 +161,7 @@ package Aspects is
       Aspect_Discard_Names,
       Aspect_Export,
       Aspect_Favor_Top_Level,               -- GNAT
+      Aspect_Ghost,                         -- GNAT
       Aspect_Independent,
       Aspect_Independent_Components,
       Aspect_Import,
@@ -234,6 +235,7 @@ package Aspects is
                              Aspect_Dimension                => True,
                              Aspect_Dimension_System         => True,
                              Aspect_Favor_Top_Level          => True,
+                             Aspect_Ghost                    => True,
                              Aspect_Global                   => True,
                              Aspect_Inline_Always            => True,
                              Aspect_Invariant                => True,
@@ -413,6 +415,7 @@ package Aspects is
      Aspect_External_Tag                 => Name_External_Tag,
      Aspect_Export                       => Name_Export,
      Aspect_Favor_Top_Level              => Name_Favor_Top_Level,
+     Aspect_Ghost                        => Name_Ghost,
      Aspect_Global                       => Name_Global,
      Aspect_Implicit_Dereference         => Name_Implicit_Dereference,
      Aspect_Import                       => Name_Import,
@@ -500,11 +503,6 @@ package Aspects is
    --  implemented internally with a hash table in the body, that provides
    --  access to aspect specifications.
 
-   function Permits_Aspect_Specifications (N : Node_Id) return Boolean;
-   --  Returns True if the node N is a declaration node that permits aspect
-   --  specifications in the grammar. It is possible for other nodes to have
-   --  aspect specifications as a result of Rewrite or Replace calls.
-
    function Aspect_Specifications (N : Node_Id) return List_Id;
    --  Given a node N, returns the list of N_Aspect_Specification nodes that
    --  are attached to this declaration node. If the node is in the class of
@@ -519,34 +517,42 @@ package Aspects is
    --  Replace calls, and this function may be used to retrieve the aspect
    --  specifications for the original rewritten node in such cases.
 
-   procedure Set_Aspect_Specifications (N : Node_Id; L : List_Id);
-   --  The node N must be in the class of declaration nodes that permit aspect
-   --  specifications and the Has_Aspects flag must be False on entry. L must
-   --  be a non-empty list of N_Aspect_Specification nodes. This procedure sets
-   --  the Has_Aspects flag to True, and makes an entry that can be retrieved
-   --  by a subsequent Aspect_Specifications call. It is an error to call this
-   --  procedure with a node that does not permit aspect specifications, or a
-   --  node that has its Has_Aspects flag set True on entry, or with L being an
-   --  empty list or No_List.
-
    function Find_Aspect (Ent : Entity_Id; A : Aspect_Id) return Node_Id;
    --  Find value of a given aspect from aspect list of entity
 
+   function Has_Aspect (Id : Entity_Id; A : Aspect_Id) return Boolean;
+   --  Determine whether entity Id has aspect A
+
    procedure Move_Aspects (From : Node_Id; To : Node_Id);
    --  Moves aspects from 'From' node to 'To' node. Has_Aspects (To) must be
    --  False on entry. If Has_Aspects (From) is False, the call has no effect.
    --  Otherwise the aspects are moved and on return Has_Aspects (To) is True,
    --  and Has_Aspects (From) is False.
 
+   function Permits_Aspect_Specifications (N : Node_Id) return Boolean;
+   --  Returns True if the node N is a declaration node that permits aspect
+   --  specifications in the grammar. It is possible for other nodes to have
+   --  aspect specifications as a result of Rewrite or Replace calls.
+
    function Same_Aspect (A1 : Aspect_Id; A2 : Aspect_Id) return Boolean;
    --  Returns True if A1 and A2 are (essentially) the same aspect. This is not
    --  a simple equality test because e.g. Post and Postcondition are the same.
    --  This is used for detecting duplicate aspects.
 
-   procedure Tree_Write;
-   --  Writes contents of Aspect_Specifications hash table to the tree file
+   procedure Set_Aspect_Specifications (N : Node_Id; L : List_Id);
+   --  The node N must be in the class of declaration nodes that permit aspect
+   --  specifications and the Has_Aspects flag must be False on entry. L must
+   --  be a non-empty list of N_Aspect_Specification nodes. This procedure sets
+   --  the Has_Aspects flag to True, and makes an entry that can be retrieved
+   --  by a subsequent Aspect_Specifications call. It is an error to call this
+   --  procedure with a node that does not permit aspect specifications, or a
+   --  node that has its Has_Aspects flag set True on entry, or with L being an
+   --  empty list or No_List.
 
    procedure Tree_Read;
    --  Reads contents of Aspect_Specifications hash table from the tree file
 
+   procedure Tree_Write;
+   --  Writes contents of Aspect_Specifications hash table to the tree file
+
 end Aspects;
diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index 3d88294006c..234c67246b7 100644
--- a/gcc/ada/einfo.adb
+++ b/gcc/ada/einfo.adb
@@ -32,12 +32,13 @@
 pragma Style_Checks (All_Checks);
 --  Turn off subprogram ordering, not used for this unit
 
-with Atree;  use Atree;
-with Namet;  use Namet;
-with Nlists; use Nlists;
-with Output; use Output;
-with Sinfo;  use Sinfo;
-with Stand;  use Stand;
+with Aspects; use Aspects;
+with Atree;   use Atree;
+with Namet;   use Namet;
+with Nlists;  use Nlists;
+with Output;  use Output;
+with Sinfo;   use Sinfo;
+with Stand;   use Stand;
 
 package body Einfo is
 
@@ -6549,10 +6550,31 @@ package body Einfo is
 
    function Is_Finalizer (Id : E) return B is
    begin
-      return Ekind (Id) = E_Procedure
-        and then Chars (Id) = Name_uFinalizer;
+      return Ekind (Id) = E_Procedure and then Chars (Id) = Name_uFinalizer;
    end Is_Finalizer;
 
+   -----------------------
+   -- Is_Ghost_Function --
+   -----------------------
+
+   function Is_Ghost_Function (Id : E) return B is
+      Subp_Id : Entity_Id := Id;
+
+   begin
+      if Present (Subp_Id) and then Ekind (Subp_Id) = E_Function then
+
+         --  Handle renamings of functions
+
+         if Present (Alias (Subp_Id)) then
+            Subp_Id := Alias (Subp_Id);
+         end if;
+
+         return Has_Aspect (Subp_Id, Aspect_Ghost);
+      end if;
+
+      return False;
+   end Is_Ghost_Function;
+
    --------------------
    -- Is_Input_State --
    --------------------
@@ -6570,8 +6592,7 @@ package body Einfo is
    function Is_Null_State (Id : E) return B is
    begin
       return
-        Ekind (Id) = E_Abstract_State
-          and then Nkind (Parent (Id)) = N_Null;
+        Ekind (Id) = E_Abstract_State and then Nkind (Parent (Id)) = N_Null;
    end Is_Null_State;
 
    ---------------------
@@ -6590,10 +6611,7 @@ package body Einfo is
 
    function Is_Package_Or_Generic_Package (Id : E) return B is
    begin
-      return
-        Ekind (Id) = E_Package
-          or else
-        Ekind (Id) = E_Generic_Package;
+      return Ekind_In (Id, E_Generic_Package, E_Package);
    end Is_Package_Or_Generic_Package;
 
    ---------------
@@ -6612,8 +6630,7 @@ package body Einfo is
 
    function Is_Protected_Component (Id : E) return B is
    begin
-      return Ekind (Id) = E_Component
-        and then Is_Protected_Type (Scope (Id));
+      return Ekind (Id) = E_Component and then Is_Protected_Type (Scope (Id));
    end Is_Protected_Component;
 
    ----------------------------
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index 70646f37442..5b7c95dd339 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -1230,7 +1230,7 @@ package Einfo is
 --       the same structure for constrained and unconstrained arrays, subtype
 --       marks and discrete ranges are both represented by a subtype. This
 --       function returns the tree node corresponding to an occurrence of the
---       first index (NOT the entity for the type). Subsequent indexes are
+--       first index (NOT the entity for the type). Subsequent indices are
 --       obtained using Next_Index. Note that this field is defined for the
 --       case of string literal subtypes, but is always Empty.
 
@@ -2292,6 +2292,10 @@ package Einfo is
 --       package, generic function, generic procedure), and False for all
 --       other entities.
 
+--    Is_Ghost_Function (synthesized)
+--       Applies to all entities. Yields True for a function marked by aspect
+--       Ghost.
+
 --    Is_Hidden (Flag57)
 --       Defined in all entities. Set true for all entities declared in the
 --       private part or body of a package. Also marks generic formals of a
@@ -5404,6 +5408,7 @@ package Einfo is
    --    Address_Clause                      (synth)
    --    First_Formal                        (synth)
    --    First_Formal_With_Extras            (synth)
+   --    Is_Ghost_Function                   (synth)    (non-generic case only)
    --    Last_Formal                         (synth)
    --    Number_Formals                      (synth)
    --    Scope_Depth                         (synth)
@@ -6611,6 +6616,7 @@ package Einfo is
    function Is_Discriminal                      (Id : E) return B;
    function Is_Dynamic_Scope                    (Id : E) return B;
    function Is_Finalizer                        (Id : E) return B;
+   function Is_Ghost_Function                   (Id : E) return B;
    function Is_Input_State                      (Id : E) return B;
    function Is_Null_State                       (Id : E) return B;
    function Is_Output_State                     (Id : E) return B;
diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb
index ee8ce836803..e9458cf6bed 100644
--- a/gcc/ada/exp_ch4.adb
+++ b/gcc/ada/exp_ch4.adb
@@ -5033,30 +5033,9 @@ package body Exp_Ch4 is
             ----------------------------
 
             function Find_Enclosing_Context return Node_Id is
-               function Is_Body_Or_Unit (N : Node_Id) return Boolean;
-               --  Determine whether N denotes a body or unit declaration
-
-               ---------------------
-               -- Is_Body_Or_Unit --
-               ---------------------
-
-               function Is_Body_Or_Unit (N : Node_Id) return Boolean is
-               begin
-                  return Nkind_In (N, N_Entry_Body,
-                                      N_Package_Body,
-                                      N_Package_Declaration,
-                                      N_Protected_Body,
-                                      N_Subprogram_Body,
-                                      N_Task_Body);
-               end Is_Body_Or_Unit;
-
-               --  Local variables
-
                Par : Node_Id;
                Top : Node_Id;
 
-            --  Start of processing for Find_Enclosing_Context
-
             begin
                --  The expression_with_actions is in a case/if expression and
                --  the lifetime of any temporary controlled object is therefore
@@ -5074,7 +5053,7 @@ package body Exp_Ch4 is
 
                      --  Prevent the search from going too far
 
-                     elsif Is_Body_Or_Unit (Par) then
+                     elsif Is_Body_Or_Package_Declaration (Par) then
                         exit;
                      end if;
 
@@ -5099,7 +5078,7 @@ package body Exp_Ch4 is
 
                      --  Prevent the search from going too far
 
-                     elsif Is_Body_Or_Unit (Par) then
+                     elsif Is_Body_Or_Package_Declaration (Par) then
                         exit;
                      end if;
 
@@ -5171,7 +5150,9 @@ package body Exp_Ch4 is
                      then
                         return Par;
 
-                     elsif Is_Body_Or_Unit (Par) then
+                     --  Prevent the search from going too far
+
+                     elsif Is_Body_Or_Package_Declaration (Par) then
                         exit;
                      end if;
 
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 059cd092e48..69e16c99689 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -8013,13 +8013,7 @@ package body Exp_Util is
 
          --  Prevent the search from going too far
 
-         elsif Nkind_In (Par, N_Entry_Body,
-                              N_Package_Body,
-                              N_Package_Declaration,
-                              N_Protected_Body,
-                              N_Subprogram_Body,
-                              N_Task_Body)
-         then
+         elsif Is_Body_Or_Package_Declaration (Par) then
             return False;
          end if;
 
diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb
index cda47de8152..be463778a7d 100644
--- a/gcc/ada/par-prag.adb
+++ b/gcc/ada/par-prag.adb
@@ -1166,6 +1166,7 @@ begin
            Pragma_Fast_Math                      |
            Pragma_Finalize_Storage_Only          |
            Pragma_Float_Representation           |
+           Pragma_Ghost                          |
            Pragma_Global                         |
            Pragma_Ident                          |
            Pragma_Implementation_Defined         |
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index 11667cde467..4b3c46c4f1d 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -602,10 +602,13 @@ package body Sem_Attr is
             if Has_Pragma_Inline_Always (Entity (P)) then
                Error_Attr_P
                  ("prefix of % attribute cannot be Inline_Always subprogram");
-            end if;
 
-            if Aname = Name_Unchecked_Access then
+            elsif Aname = Name_Unchecked_Access then
                Error_Attr ("attribute% cannot be applied to a subprogram", P);
+
+            elsif Is_Ghost_Function (Entity (P)) then
+               Error_Attr_P
+                 ("prefix of % attribute cannot be a ghost function");
             end if;
 
             --  Issue an error if the prefix denotes an eliminated subprogram
@@ -3694,13 +3697,7 @@ package body Sem_Attr is
 
                   --  Prevent the search from going too far
 
-                  elsif Nkind_In (Stmt, N_Entry_Body,
-                                        N_Package_Body,
-                                        N_Package_Declaration,
-                                        N_Protected_Body,
-                                        N_Subprogram_Body,
-                                        N_Task_Body)
-                  then
+                  elsif Is_Body_Or_Package_Declaration (Stmt) then
                      exit;
                   end if;
 
@@ -3845,13 +3842,7 @@ package body Sem_Attr is
 
             --  Prevent the search from going too far
 
-            elsif Nkind_In (Stmt, N_Entry_Body,
-                                  N_Package_Body,
-                                  N_Package_Declaration,
-                                  N_Protected_Body,
-                                  N_Subprogram_Body,
-                                  N_Task_Body)
-            then
+            elsif Is_Body_Or_Package_Declaration (Stmt) then
                exit;
             end if;
 
@@ -9193,7 +9184,6 @@ package body Sem_Attr is
                     and then
                       (Ekind (Btyp) = E_Access_Subprogram_Type
                         or else Is_Local_Anonymous_Access (Btyp))
-
                     and then Subprogram_Access_Level (Entity (P)) >
                                Type_Access_Level (Btyp)
                   then
@@ -9595,9 +9585,9 @@ package body Sem_Attr is
                --  in such a context.
 
                if Attr_Id /= Attribute_Unchecked_Access
+                 and then Ekind (Btyp) = E_General_Access_Type
                  and then
                    Object_Access_Level (P) > Deepest_Type_Access_Level (Btyp)
-                 and then Ekind (Btyp) = E_General_Access_Type
                then
                   Accessibility_Message;
                   return;
diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index d04ef4652fa..1fe5277cfd8 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -12402,7 +12402,16 @@ package body Sem_Ch12 is
                Analyze (Act);
             end if;
 
-            if Errs /= Serious_Errors_Detected then
+            --  Ensure that a ghost function does not act as generic actual
+
+            if Is_Entity_Name (Act)
+              and then Is_Ghost_Function (Entity (Act))
+            then
+               Error_Msg_N
+                 ("ghost function & cannot act as generic actual", Act);
+               Abandon_Instantiation (Act);
+
+            elsif Errs /= Serious_Errors_Detected then
 
                --  Do a minimal analysis of the generic, to prevent spurious
                --  warnings complaining about the generic being unreferenced,
diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb
index a66b19482cb..b8ecf3989cf 100644
--- a/gcc/ada/sem_ch4.adb
+++ b/gcc/ada/sem_ch4.adb
@@ -868,6 +868,11 @@ package body Sem_Ch4 is
       --  Flag indicates whether an interpretation of the prefix is a
       --  parameterless call that returns an access_to_subprogram.
 
+      procedure Check_Ghost_Function_Call;
+      --  Verify the legality of a call to a ghost function. Such calls can
+      --  appear only in assertion expressions except subtype predicates or
+      --  from within another ghost function.
+
       procedure Check_Mixed_Parameter_And_Named_Associations;
       --  Check that parameter and named associations are not mixed. This is
       --  a restriction in SPARK mode.
@@ -882,6 +887,38 @@ package body Sem_Ch4 is
       procedure No_Interpretation;
       --  Output error message when no valid interpretation exists
 
+      -------------------------------
+      -- Check_Ghost_Function_Call --
+      -------------------------------
+
+      procedure Check_Ghost_Function_Call is
+         S : Entity_Id;
+
+      begin
+         --  The ghost function appears inside an assertion expression
+
+         if In_Assertion_Expression (N) then
+            return;
+
+         else
+            S := Current_Scope;
+            while Present (S) and then S /= Standard_Standard loop
+
+               --  The call appears inside another ghost function
+
+               if Is_Ghost_Function (S) then
+                  return;
+               end if;
+
+               S := Scope (S);
+            end loop;
+         end if;
+
+         Error_Msg_N
+           ("call to ghost function must appear in assertion expression or "
+            & "another ghost function", N);
+      end Check_Ghost_Function_Call;
+
       --------------------------------------------------
       -- Check_Mixed_Parameter_And_Named_Associations --
       --------------------------------------------------
@@ -972,6 +1009,12 @@ package body Sem_Ch4 is
          Check_Mixed_Parameter_And_Named_Associations;
       end if;
 
+      --  Mark a function that appears inside an assertion expression
+
+      if Nkind (N) = N_Function_Call and then In_Assertion_Expr > 0 then
+         Set_In_Assertion_Expression (N);
+      end if;
+
       --  Initialize the type of the result of the call to the error type,
       --  which will be reset if the type is successfully resolved.
 
@@ -1078,6 +1121,8 @@ package body Sem_Ch4 is
             Set_Etype (Nam_Ent, Etype (N));
          end if;
 
+      --  Overloaded call
+
       else
          --  An overloaded selected component must denote overloaded operations
          --  of a concurrent type. The interpretations are attached to the
@@ -1162,9 +1207,9 @@ package body Sem_Ch4 is
             Get_Next_Interp (X, It);
          end loop;
 
-         --  If the name is the result of a function call, it can only
-         --  be a call to a function returning an access to subprogram.
-         --  Insert explicit dereference.
+         --  If the name is the result of a function call, it can only be a
+         --  call to a function returning an access to subprogram. Insert
+         --  explicit dereference.
 
          if Nkind (Nam) = N_Function_Call then
             Insert_Explicit_Dereference (Nam);
@@ -1243,6 +1288,13 @@ package body Sem_Ch4 is
 
          End_Interp_List;
       end if;
+
+      --  A call to a ghost function is allowed only in assertion expressions,
+      --  excluding subtype predicates, or from within another ghost function.
+
+      if Is_Ghost_Function (Get_Subprogram_Entity (N)) then
+         Check_Ghost_Function_Call;
+      end if;
    end Analyze_Call;
 
    -----------------------------
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index c3e7d433ebb..c524f89e8b4 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -486,19 +486,21 @@ package body Sem_Ch6 is
    ----------------------------
 
    procedure Analyze_Function_Call (N : Node_Id) is
-      P       : constant Node_Id := Name (N);
-      Actuals : constant List_Id := Parameter_Associations (N);
-      Actual  : Node_Id;
+      Actuals  : constant List_Id := Parameter_Associations (N);
+      Func_Nam : constant Node_Id := Name (N);
+      Actual   : Node_Id;
+
+   --  Start of processing for Analyze_Function_Call
 
    begin
-      Analyze (P);
+      Analyze (Func_Nam);
 
       --  A call of the form A.B (X) may be an Ada 2005 call, which is
       --  rewritten as B (A, X). If the rewriting is successful, the call
       --  has been analyzed and we just return.
 
-      if Nkind (P) = N_Selected_Component
-        and then Name (N) /= P
+      if Nkind (Func_Nam) = N_Selected_Component
+        and then Name (N) /= Func_Nam
         and then Is_Rewrite_Substitution (N)
         and then Present (Etype (N))
       then
@@ -507,7 +509,7 @@ package body Sem_Ch6 is
 
       --  If error analyzing name, then set Any_Type as result type and return
 
-      if Etype (P) = Any_Type then
+      if Etype (Func_Nam) = Any_Type then
          Set_Etype (N, Any_Type);
          return;
       end if;
@@ -524,12 +526,6 @@ package body Sem_Ch6 is
       end if;
 
       Analyze_Call (N);
-
-      --  Mark function call if within assertion
-
-      if In_Assertion_Expr /= 0 then
-         Set_In_Assertion (N);
-      end if;
    end Analyze_Function_Call;
 
    -----------------------------
@@ -537,9 +533,9 @@ package body Sem_Ch6 is
    -----------------------------
 
    procedure Analyze_Function_Return (N : Node_Id) is
-      Loc        : constant Source_Ptr  := Sloc (N);
-      Stm_Entity : constant Entity_Id   := Return_Statement_Entity (N);
-      Scope_Id   : constant Entity_Id   := Return_Applies_To (Stm_Entity);
+      Loc        : constant Source_Ptr := Sloc (N);
+      Stm_Entity : constant Entity_Id  := Return_Statement_Entity (N);
+      Scope_Id   : constant Entity_Id  := Return_Applies_To (Stm_Entity);
 
       R_Type : constant Entity_Id := Etype (Scope_Id);
       --  Function result subtype
@@ -6562,6 +6558,11 @@ package body Sem_Ch6 is
                else
                   Set_Overridden_Operation (Subp, Overridden_Subp);
                end if;
+
+            --  Ensure that a ghost function is not overriding another routine
+
+            elsif Is_Ghost_Function (Subp) then
+               Error_Msg_N ("ghost function & cannot be overriding", Subp);
             end if;
          end if;
 
diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb
index 881fdb1fb73..710983ffa53 100644
--- a/gcc/ada/sem_elab.adb
+++ b/gcc/ada/sem_elab.adb
@@ -2258,7 +2258,7 @@ package body Sem_Elab is
            --  in this case, due to the out of order handling in this case.
 
            and then (Nkind (Original_Node (N)) /= N_Function_Call
-                      or else not In_Assertion (Original_Node (N)))
+                      or else not In_Assertion_Expression (Original_Node (N)))
          then
             if Inst_Case then
                Error_Msg_NE
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index a8d3fe589b9..240eb0c7684 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -253,10 +253,15 @@ package body Sem_Prag is
       --  Pre-analyze the guard and consequence expressions of a Contract_Cases
       --  pragma/aspect aggregate expression.
 
+      ----------------------------
+      -- Analyze_Contract_Cases --
+      ----------------------------
+
       procedure Analyze_Contract_Cases (Aggr : Node_Id) is
          Case_Guard : Node_Id;
          Conseq     : Node_Id;
          Post_Case  : Node_Id;
+
       begin
          Post_Case := First (Component_Associations (Aggr));
          while Present (Post_Case) loop
@@ -266,19 +271,24 @@ package body Sem_Prag is
             --  Preanalyze the boolean expression, we treat this as a spec
             --  expression (i.e. similar to a default expression).
 
-            Preanalyze_Assert_Expression (Case_Guard, Standard_Boolean);
+            if Nkind (Case_Guard) /= N_Others_Choice then
+               Preanalyze_Assert_Expression (Case_Guard, Standard_Boolean);
+            end if;
+
             Preanalyze_Assert_Expression (Conseq, Standard_Boolean);
 
             Next (Post_Case);
          end loop;
       end Analyze_Contract_Cases;
 
+   --  Start of processing for Analyze_CTC_In_Decl_Part
+
    begin
       --  Install formals and push subprogram spec onto scope stack so that we
       --  can see the formals from the pragma.
 
-      Install_Formals (S);
       Push_Scope (S);
+      Install_Formals (S);
 
       --  Preanalyze the boolean expressions, we treat these as spec
       --  expressions (i.e. similar to a default expression).
@@ -11194,6 +11204,39 @@ package body Sem_Prag is
             end if;
          end Float_Representation;
 
+         -----------
+         -- Ghost --
+         -----------
+
+         --  pragma GHOST (function_LOCAL_NAME);
+
+         when Pragma_Ghost => Ghost : declare
+            Subp    : Node_Id;
+            Subp_Id : Entity_Id;
+
+         begin
+            GNAT_Pragma;
+            S14_Pragma;
+            Check_Arg_Count (1);
+            Check_Arg_Is_Local_Name (Arg1);
+
+            --  Ensure the proper placement of the pragma. Ghost must be
+            --  associated with a subprogram declaration.
+
+            Subp := Parent (Corresponding_Aspect (N));
+
+            if Nkind (Subp) /= N_Subprogram_Declaration then
+               Pragma_Misplaced;
+               return;
+            end if;
+
+            Subp_Id := Defining_Unit_Name (Specification (Subp));
+
+            if Ekind (Subp_Id) /= E_Function then
+               Error_Pragma ("pragma % must be applied to a function");
+            end if;
+         end Ghost;
+
          ------------
          -- Global --
          ------------
@@ -13542,14 +13585,12 @@ package body Sem_Prag is
                return;
             end if;
 
-            Preanalyze_And_Resolve (Expression (Arg1), Any_Boolean);
+            Preanalyze_Assert_Expression (Expression (Arg1), Any_Boolean);
 
             --  Transform pragma Loop_Invariant into equivalent pragma Check
             --  Generate:
             --    pragma Check (Loop_Invaraint, Arg1);
 
-            --  Seems completely wrong to hijack pragma Check this way ???
-
             Rewrite (N,
               Make_Pragma (Loc,
                 Chars                        => Name_Check,
@@ -13625,7 +13666,8 @@ package body Sem_Prag is
                   Error_Pragma_Arg ("wrong change modifier", Variant);
                end if;
 
-               Preanalyze_And_Resolve (Expression (Variant), Any_Discrete);
+               Preanalyze_Assert_Expression
+                 (Expression (Variant), Any_Discrete);
 
                Next (Variant);
             end loop;
@@ -17762,6 +17804,7 @@ package body Sem_Prag is
       Pragma_Fast_Math                      => -1,
       Pragma_Finalize_Storage_Only          =>  0,
       Pragma_Float_Representation           =>  0,
+      Pragma_Ghost                          =>  0,
       Pragma_Global                         => -1,
       Pragma_Ident                          => -1,
       Pragma_Implementation_Defined         => -1,
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 806b6484a50..533834e7272 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -5612,49 +5612,58 @@ package body Sem_Util is
    ---------------------------
 
    function Get_Subprogram_Entity (Nod : Node_Id) return Entity_Id is
-      Nam  : Node_Id;
-      Proc : Entity_Id;
+      Subp    : Node_Id;
+      Subp_Id : Entity_Id;
 
    begin
       if Nkind (Nod) = N_Accept_Statement then
-         Nam := Entry_Direct_Name (Nod);
+         Subp := Entry_Direct_Name (Nod);
+
+      elsif Nkind (Nod) = N_Slice then
+         Subp := Prefix (Nod);
+
+      else
+         Subp := Name (Nod);
+      end if;
+
+      --  Strip the subprogram call
+
+      loop
+         if Nkind_In (Subp, N_Explicit_Dereference,
+                            N_Indexed_Component,
+                            N_Selected_Component)
+         then
+            Subp := Prefix (Subp);
 
-      --  For an entry call, the prefix of the call is a selected component.
-      --  Need additional code for internal calls ???
+         elsif Nkind_In (Subp, N_Type_Conversion,
+                               N_Unchecked_Type_Conversion)
+         then
+            Subp := Expression (Subp);
 
-      elsif Nkind (Nod) = N_Entry_Call_Statement then
-         if Nkind (Name (Nod)) = N_Selected_Component then
-            Nam := Entity (Selector_Name (Name (Nod)));
          else
-            Nam := Empty;
+            exit;
          end if;
+      end loop;
 
-      else
-         Nam := Name (Nod);
-      end if;
+      --  Extract the entity of the subprogram call
 
-      if Nkind (Nam) = N_Explicit_Dereference then
-         Proc := Etype (Prefix (Nam));
-      elsif Is_Entity_Name (Nam) then
-         Proc := Entity (Nam);
-      else
-         return Empty;
-      end if;
+      if Is_Entity_Name (Subp) then
+         Subp_Id := Entity (Subp);
 
-      if Is_Object (Proc) then
-         Proc := Etype (Proc);
-      end if;
+         if Ekind (Subp_Id) = E_Access_Subprogram_Type then
+            Subp_Id := Directly_Designated_Type (Subp_Id);
+         end if;
 
-      if Ekind (Proc) = E_Access_Subprogram_Type then
-         Proc := Directly_Designated_Type (Proc);
-      end if;
+         if Is_Subprogram (Subp_Id) then
+            return Subp_Id;
+         else
+            return Empty;
+         end if;
+
+      --  The search did not find a construct that denotes a subprogram
 
-      if not Is_Subprogram (Proc)
-        and then Ekind (Proc) /= E_Subprogram_Type
-      then
-         return Empty;
       else
-         return Proc;
+         return Empty;
       end if;
    end Get_Subprogram_Entity;
 
@@ -7714,6 +7723,20 @@ package body Sem_Util is
       end if;
    end Is_Atomic_Object;
 
+   ------------------------------------
+   -- Is_Body_Or_Package_Declaration --
+   ------------------------------------
+
+   function Is_Body_Or_Package_Declaration (N : Node_Id) return Boolean is
+   begin
+      return Nkind_In (N, N_Entry_Body,
+                          N_Package_Body,
+                          N_Package_Declaration,
+                          N_Protected_Body,
+                          N_Subprogram_Body,
+                          N_Task_Body);
+   end Is_Body_Or_Package_Declaration;
+
    -----------------------
    -- Is_Bounded_String --
    -----------------------
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 1296786ef5a..3d252a2c634 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -178,6 +178,17 @@ package Sem_Util is
    --  not necessarily mean that CE could be raised, but a response of True
    --  means that for sure CE cannot be raised.
 
+   procedure Check_Dynamically_Tagged_Expression
+     (Expr        : Node_Id;
+      Typ         : Entity_Id;
+      Related_Nod : Node_Id);
+   --  Check wrong use of dynamically tagged expression
+
+   procedure Check_Fully_Declared (T : Entity_Id; N : Node_Id);
+   --  Verify that the full declaration of type T has been seen. If not, place
+   --  error message on node N. Used in object declarations, type conversions
+   --  and qualified expressions.
+
    procedure Check_Function_Writable_Actuals (N : Node_Id);
    --  (Ada 2012): If the construct N has two or more direct constituents that
    --  are names or expressions whose evaluation may occur in an arbitrary
@@ -210,17 +221,6 @@ package Sem_Util is
    --  remains in the Examiner (JB01-005). Note that the Examiner does not
    --  count package declarations in later declarative items.
 
-   procedure Check_Dynamically_Tagged_Expression
-     (Expr        : Node_Id;
-      Typ         : Entity_Id;
-      Related_Nod : Node_Id);
-   --  Check wrong use of dynamically tagged expression
-
-   procedure Check_Fully_Declared (T : Entity_Id; N : Node_Id);
-   --  Verify that the full declaration of type T has been seen. If not, place
-   --  error message on node N. Used in object declarations, type conversions
-   --  and qualified expressions.
-
    procedure Check_Nested_Access (Ent : Entity_Id);
    --  Check whether Ent denotes an entity declared in an uplevel scope, which
    --  is accessed inside a nested procedure, and set Has_Up_Level_Access flag
@@ -470,7 +470,7 @@ package Sem_Util is
    --  discriminant at the same position in this new type.
 
    procedure Find_Overlaid_Entity
-     (N : Node_Id;
+     (N   : Node_Id;
       Ent : out Entity_Id;
       Off : out Boolean);
    --  The node N should be an address representation clause. Determines if
@@ -849,6 +849,9 @@ package Sem_Util is
    --  Determines if the given node denotes an atomic object in the sense of
    --  the legality checks described in RM C.6(12).
 
+   function Is_Body_Or_Package_Declaration (N : Node_Id) return Boolean;
+   --  Determine whether node N denotes a body or a package declaration
+
    function Is_Bounded_String (T : Entity_Id) return Boolean;
    --  True if T is a bounded string type. Used to make sure "=" composes
    --  properly for bounded string types.
@@ -1304,9 +1307,9 @@ package Sem_Util is
    --  S2. Otherwise, it is S itself.
 
    function Object_Access_Level (Obj : Node_Id) return Uint;
-   --  Return the accessibility level of the view of the object Obj.
-   --  For convenience, qualified expressions applied to object names
-   --  are also allowed as actuals for this function.
+   --  Return the accessibility level of the view of the object Obj. For
+   --  convenience, qualified expressions applied to object names are also
+   --  allowed as actuals for this function.
 
    function Primitive_Names_Match (E1, E2 : Entity_Id) return Boolean;
    --  Returns True if the names of both entities correspond with matching
diff --git a/gcc/ada/sinfo.adb b/gcc/ada/sinfo.adb
index 98dbe553fae..3c9096fb944 100644
--- a/gcc/ada/sinfo.adb
+++ b/gcc/ada/sinfo.adb
@@ -1640,13 +1640,13 @@ package body Sinfo is
       return Flag16 (N);
    end Import_Interface_Present;
 
-   function In_Assertion
+   function In_Assertion_Expression
       (N : Node_Id) return Boolean is
    begin
       pragma Assert (False
         or else NT (N).Nkind = N_Function_Call);
       return Flag4 (N);
-   end In_Assertion;
+   end In_Assertion_Expression;
 
    function In_Present
       (N : Node_Id) return Boolean is
@@ -4722,13 +4722,13 @@ package body Sinfo is
       Set_Flag16 (N, Val);
    end Set_Import_Interface_Present;
 
-   procedure Set_In_Assertion
+   procedure Set_In_Assertion_Expression
       (N : Node_Id; Val : Boolean := True) is
    begin
       pragma Assert (False
         or else NT (N).Nkind = N_Function_Call);
       Set_Flag4 (N, Val);
-   end Set_In_Assertion;
+   end Set_In_Assertion_Expression;
 
    procedure Set_In_Present
       (N : Node_Id; Val : Boolean := True) is
diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads
index 3c8d26a0035..1711252ed31 100644
--- a/gcc/ada/sinfo.ads
+++ b/gcc/ada/sinfo.ads
@@ -1227,7 +1227,7 @@ package Sinfo is
    --     pragma of the other kind is also present. This is used to avoid
    --     generating some unwanted error messages.
 
-   --  In_Assertion (Flag4-Sem)
+   --  In_Assertion_Expression (Flag4-Sem)
    --     This flag is present in N_Function_Call nodes. It is set if the
    --     function is called from within an assertion expression. This is
    --     used to avoid some bogus warnings about early elaboration.
@@ -4772,7 +4772,7 @@ package Sinfo is
       --   actual parameter part)
       --  First_Named_Actual (Node4-Sem)
       --  Controlling_Argument (Node1-Sem) (set to Empty if not dispatching)
-      --  In_Assertion (Flag4-Sem)
+      --  In_Assertion_Expression (Flag4-Sem)
       --  Is_Expanded_Build_In_Place_Call (Flag11-Sem)
       --  Do_Tag_Check (Flag13-Sem)
       --  No_Elaboration_Check (Flag14-Sem)
@@ -8628,7 +8628,7 @@ package Sinfo is
    function Import_Interface_Present
      (N : Node_Id) return Boolean;    -- Flag16
 
-   function In_Assertion
+   function In_Assertion_Expression
      (N : Node_Id) return Boolean;    -- Flag4
 
    function In_Present
@@ -9609,7 +9609,7 @@ package Sinfo is
    procedure Set_Import_Interface_Present
      (N : Node_Id; Val : Boolean := True);    -- Flag16
 
-   procedure Set_In_Assertion
+   procedure Set_In_Assertion_Expression
      (N : Node_Id; Val : Boolean := True);    -- Flag4
 
    procedure Set_In_Present
@@ -12007,7 +12007,7 @@ package Sinfo is
    pragma Inline (Interface_Present);
    pragma Inline (Includes_Infinities);
    pragma Inline (Import_Interface_Present);
-   pragma Inline (In_Assertion);
+   pragma Inline (In_Assertion_Expression);
    pragma Inline (In_Present);
    pragma Inline (Inherited_Discriminant);
    pragma Inline (Instance_Spec);
@@ -12329,7 +12329,7 @@ package Sinfo is
    pragma Inline (Set_Interface_List);
    pragma Inline (Set_Interface_Present);
    pragma Inline (Set_Import_Interface_Present);
-   pragma Inline (Set_In_Assertion);
+   pragma Inline (Set_In_Assertion_Expression);
    pragma Inline (Set_In_Present);
    pragma Inline (Set_Inherited_Discriminant);
    pragma Inline (Set_Instance_Spec);
diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl
index 05d11dd155f..0510c5dfd6c 100644
--- a/gcc/ada/snames.ads-tmpl
+++ b/gcc/ada/snames.ads-tmpl
@@ -498,6 +498,7 @@ package Snames is
    Name_Export_Valued_Procedure        : constant Name_Id := N + $; -- GNAT
    Name_External                       : constant Name_Id := N + $; -- GNAT
    Name_Finalize_Storage_Only          : constant Name_Id := N + $; -- GNAT
+   Name_Ghost                          : constant Name_Id := N + $; -- GNAT
    Name_Global                         : constant Name_Id := N + $; -- GNAT
    Name_Ident                          : constant Name_Id := N + $; -- VMS
    Name_Implementation_Defined         : constant Name_Id := N + $; -- GNAT
@@ -1792,6 +1793,7 @@ package Snames is
       Pragma_Export_Valued_Procedure,
       Pragma_External,
       Pragma_Finalize_Storage_Only,
+      Pragma_Ghost,
       Pragma_Global,
       Pragma_Ident,
       Pragma_Implementation_Defined,