[Ada] Support ghost generic formal parameters

This adds support in GNAT for ghost generic formal parameters, as
included in SPARK RM 6.9.

gcc/ada/

	* ghost.adb (Check_Ghost_Context): Delay checking for generic
	associations.
	(Check_Ghost_Context_In_Generic_Association): Perform ghost
	checking in analyzed generic associations.
	(Check_Ghost_Formal_Procedure_Or_Package): Check SPARK RM
	6.9(13-14) for formal procedures and packages.
	(Check_Ghost_Formal_Variable): Check SPARK RM 6.9(13-14) for
	variables.
	* ghost.ads: Declarations for the above.
	* sem_ch12.adb (Analyze_Associations): Apply delayed checking
	for generic associations.
	(Analyze_Formal_Object_Declaration): Same.
	(Analyze_Formal_Subprogram_Declaration): Same.
	(Instantiate_Formal_Package): Same.
	(Instantiate_Formal_Subprogram): Same.
	(Instantiate_Object): Same.  Copy ghost aspect to newly declared
	object for actual for IN formal object. Use new function
	Get_Enclosing_Deep_Object to retrieve root object.
	(Instantiate_Type): Copy ghost aspect to declared subtype for
	actual for formal type.
	* sem_prag.adb (Analyze_Pragma): Recognize new allowed
	declarations.
	* sem_util.adb (Copy_Ghost_Aspect): Copy the ghost aspect
	between nodes.
	(Get_Enclosing_Deep_Object): New function to return enclosing
	deep object (or root for reachable part).
	* sem_util.ads (Copy_Ghost_Aspect): Same.
	(Get_Enclosing_Deep_Object): Same.
	* libgnat/s-imageu.ads: Declare formal subprograms as ghost.
	* libgnat/s-valuei.ads: Same.
	* libgnat/s-valuti.ads: Same.

3 files changed, 46 insertions, 23 deletions

diff --git a/gcc/ada/libgnat/s-imageu.ads b/gcc/ada/libgnat/s-imageu.ads
index d3f2981..789cf65 100644
--- a/gcc/ada/libgnat/s-imageu.ads
+++ b/gcc/ada/libgnat/s-imageu.ads
@@ -54,27 +54,34 @@ generic
 
    Unsigned_Width_Ghost : Natural;
 
-   with function Wrap_Option (Value : Uns) return Uns_Option;
+   with function Wrap_Option (Value : Uns) return Uns_Option
+      with Ghost;
    with function Only_Decimal_Ghost
      (Str      : String;
       From, To : Integer)
-      return Boolean;
-   with function Hexa_To_Unsigned_Ghost (X : Character) return Uns;
+      return Boolean
+      with Ghost;
+   with function Hexa_To_Unsigned_Ghost (X : Character) return Uns
+      with Ghost;
    with function Scan_Based_Number_Ghost
      (Str      : String;
       From, To : Integer;
       Base     : Uns := 10;
-      Acc      : Uns := 0) return Uns_Option;
-   with function Is_Unsigned_Ghost (Str : String) return Boolean;
+      Acc      : Uns := 0) return Uns_Option
+      with Ghost;
+   with function Is_Unsigned_Ghost (Str : String) return Boolean
+      with Ghost;
    with function Value_Unsigned (Str : String) return Uns;
    with procedure Prove_Iter_Scan_Based_Number_Ghost
      (Str1, Str2 : String;
       From, To : Integer;
       Base     : Uns := 10;
-      Acc      : Uns := 0);
+      Acc      : Uns := 0)
+      with Ghost;
    with procedure Prove_Scan_Only_Decimal_Ghost
      (Str : String;
-      Val : Uns);
+      Val : Uns)
+      with Ghost;
 
 package System.Image_U is
 
diff --git a/gcc/ada/libgnat/s-valuei.ads b/gcc/ada/libgnat/s-valuei.ads
index c5b4b8e..5e42773 100644
--- a/gcc/ada/libgnat/s-valuei.ads
+++ b/gcc/ada/libgnat/s-valuei.ads
@@ -55,30 +55,37 @@ generic
    --  Additional parameters for ghost subprograms used inside contracts
 
    type Uns_Option is private;
-   with function Wrap_Option (Value : Uns) return Uns_Option;
-   with function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean;
+   with function Wrap_Option (Value : Uns) return Uns_Option
+      with Ghost;
+   with function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean
+      with Ghost;
    with function Raw_Unsigned_Overflows_Ghost
      (Str      : String;
       From, To : Integer)
-      return Boolean;
+      return Boolean
+      with Ghost;
    with function Scan_Raw_Unsigned_Ghost
      (Str      : String;
       From, To : Integer)
-      return Uns;
+      return Uns
+      with Ghost;
    with function Raw_Unsigned_Last_Ghost
      (Str      : String;
       From, To : Integer)
-      return Positive;
+      return Positive
+      with Ghost;
    with function Only_Decimal_Ghost
      (Str      : String;
       From, To : Integer)
-      return Boolean;
+      return Boolean
+      with Ghost;
    with function Scan_Based_Number_Ghost
      (Str      : String;
       From, To : Integer;
       Base     : Uns := 10;
       Acc      : Uns := 0)
-      return Uns_Option;
+      return Uns_Option
+      with Ghost;
 
 package System.Value_I is
    pragma Preelaborate;
diff --git a/gcc/ada/libgnat/s-valuti.ads b/gcc/ada/libgnat/s-valuti.ads
index 45a0b66..2b89b12 100644
--- a/gcc/ada/libgnat/s-valuti.ads
+++ b/gcc/ada/libgnat/s-valuti.ads
@@ -384,27 +384,36 @@ is
 
       Unsigned_Width_Ghost : Natural;
 
-      with function Wrap_Option (Value : Uns) return Uns_Option;
+      with function Wrap_Option (Value : Uns) return Uns_Option
+         with Ghost;
       with function Only_Decimal_Ghost
         (Str      : String;
          From, To : Integer)
-         return Boolean;
-      with function Hexa_To_Unsigned_Ghost (X : Character) return Uns;
+         return Boolean
+         with Ghost;
+      with function Hexa_To_Unsigned_Ghost (X : Character) return Uns
+         with Ghost;
       with function Scan_Based_Number_Ghost
         (Str      : String;
          From, To : Integer;
          Base     : Uns := 10;
          Acc      : Uns := 0)
-         return Uns_Option;
-      with function Is_Integer_Ghost (Str : String) return Boolean;
+         return Uns_Option
+         with Ghost;
+      with function Is_Integer_Ghost (Str : String) return Boolean
+         with Ghost;
       with procedure Prove_Iter_Scan_Based_Number_Ghost
         (Str1, Str2 : String;
          From, To : Integer;
          Base     : Uns := 10;
-         Acc      : Uns := 0);
-      with procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int);
-      with function Abs_Uns_Of_Int (Val : Int) return Uns;
-      with function Value_Integer (Str : String) return Int;
+         Acc      : Uns := 0)
+         with Ghost;
+      with procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int)
+         with Ghost;
+      with function Abs_Uns_Of_Int (Val : Int) return Uns
+         with Ghost;
+      with function Value_Integer (Str : String) return Int
+         with Ghost;
 
    package Int_Params is
    end Int_Params;