[Ada] Allow Big_Integer in loop and subprogram variants

In SPARK loop and subprogram variants we now allow expressions of any
discrete type and of Ada.Numerics.Big_Numbers.Big_Integers.Big_Integer
type.

gcc/ada/

	* exp_prag.adb (Expand_Pragma_Loop_Variant,
	Expand_Pragma_Subprogram_Variant): Adapt call via
	Process_Variant to Make_Variant_Comparison.
	* exp_util.adb (Make_Variant_Comparison): Compare Big_Integer
	expressions with a function call and not an operator.
	* exp_util.ads (Make_Variant_Comparison): Add type parameter,
	which is needed because the Curr_Val and Old_Val expressions
	might not be yet decorated.
	* rtsfind.ads: (RTU_Id): Add support for Big_Integers and
	Big_Integers_Ghost.
	(RE_Id): Add support for Big_Integer and its ghost variant.
	(RE_Unit_Table): Add mapping from Big_Integer to Big_Integers;
	same for the ghost variants.
	* rtsfind.adb (Get_Unit_Name): Add support for Big_Numbers.
	* sem_prag.adb (Analyze_Pragma): Allow Big_Integer in pragma
	Loop_Variant.
	(Analyze_Variant): Allow Big_Integer in pragma
	Subprogram_Variant.

6 files changed, 137 insertions, 7 deletions

diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb
index f434823..35ec250 100644
--- a/gcc/ada/exp_prag.adb
+++ b/gcc/ada/exp_prag.adb
@@ -2636,6 +2636,7 @@ package body Exp_Prag is
                  Expression =>
                    Make_Variant_Comparison (Loc,
                      Mode     => Chars (Variant),
+                     Typ      => Expr_Typ,
                      Curr_Val => New_Occurrence_Of (Curr_Id, Loc),
                      Old_Val  => New_Occurrence_Of (Old_Id, Loc)))));
 
@@ -3000,6 +3001,7 @@ package body Exp_Prag is
                  Expression =>
                    Make_Variant_Comparison (Loc,
                      Mode     => Chars (First (Choices (Variant))),
+                     Typ      => Expr_Typ,
                      Curr_Val => New_Occurrence_Of (Curr_Id, Loc),
                      Old_Val  => New_Occurrence_Of (Old_Id, Loc)))));
 
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 64324bf..416ce65 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -10239,15 +10239,61 @@ package body Exp_Util is
 
    function Make_Variant_Comparison
      (Loc      : Source_Ptr;
+      Typ      : Entity_Id;
       Mode     : Name_Id;
       Curr_Val : Node_Id;
       Old_Val  : Node_Id) return Node_Id
    is
+      function Big_Integer_Lt return Entity_Id;
+      --  Returns the entity of the predefined "<" function from
+      --  Ada.Numerics.Big_Numbers.Big_Integers.
+
+      --------------------
+      -- Big_Integer_Lt --
+      --------------------
+
+      function Big_Integer_Lt return Entity_Id is
+         Big_Integers : constant Entity_Id :=
+           RTU_Entity (Ada_Numerics_Big_Numbers_Big_Integers);
+
+         E : Entity_Id := First_Entity (Big_Integers);
+
+      begin
+         while Present (E) loop
+            if Chars (E) = Name_Op_Lt then
+               return E;
+            end if;
+            Next_Entity (E);
+         end loop;
+
+         raise Program_Error;
+      end Big_Integer_Lt;
+
+   --  Start of processing for Make_Variant_Comparison
+
    begin
       if Mode = Name_Increases then
          return Make_Op_Gt (Loc, Curr_Val, Old_Val);
+
       else pragma Assert (Mode = Name_Decreases);
-         return Make_Op_Lt (Loc, Curr_Val, Old_Val);
+
+         --  For discrete expressions use the "<" operator
+
+         if Is_Discrete_Type (Typ) then
+            return Make_Op_Lt (Loc, Curr_Val, Old_Val);
+
+         --  For Big_Integer expressions use the "<" function, because the
+         --  operator on private type might not be visible and won't be
+         --  resolved.
+
+         else pragma Assert (Is_RTE (Base_Type (Typ), RE_Big_Integer));
+            return
+              Make_Function_Call (Loc,
+                Name                   =>
+                  New_Occurrence_Of (Big_Integer_Lt, Loc),
+                Parameter_Associations =>
+                  New_List (Curr_Val, Old_Val));
+         end if;
       end if;
    end Make_Variant_Comparison;
 
diff --git a/gcc/ada/exp_util.ads b/gcc/ada/exp_util.ads
index 0233e56..d384567 100644
--- a/gcc/ada/exp_util.ads
+++ b/gcc/ada/exp_util.ads
@@ -901,12 +901,14 @@ package Exp_Util is
 
    function Make_Variant_Comparison
      (Loc      : Source_Ptr;
+      Typ      : Entity_Id;
       Mode     : Name_Id;
       Curr_Val : Node_Id;
       Old_Val  : Node_Id) return Node_Id;
    --  Subsidiary to the expansion of pragmas Loop_Variant and
    --  Subprogram_Variant. Generate a comparison between Curr_Val and Old_Val
-   --  depending on the variant mode (Increases / Decreases).
+   --  depending on the variant mode (Increases / Decreases) using less or
+   --  greater operator for Typ.
 
    procedure Map_Formals
      (Parent_Subp  : Entity_Id;
diff --git a/gcc/ada/rtsfind.adb b/gcc/ada/rtsfind.adb
index 6808efa..cda13d4 100644
--- a/gcc/ada/rtsfind.adb
+++ b/gcc/ada/rtsfind.adb
@@ -564,8 +564,12 @@ package body Rtsfind is
      Ada_Interrupts_Names .. Ada_Interrupts_Names;
 
    subtype Ada_Numerics_Descendant is Ada_Descendant
-     range Ada_Numerics_Generic_Elementary_Functions ..
-           Ada_Numerics_Generic_Elementary_Functions;
+     range Ada_Numerics_Big_Numbers ..
+           Ada_Numerics_Big_Numbers_Big_Integers_Ghost;
+
+   subtype Ada_Numerics_Big_Numbers_Descendant is Ada_Descendant
+     range Ada_Numerics_Big_Numbers_Big_Integers ..
+           Ada_Numerics_Big_Numbers_Big_Integers_Ghost;
 
    subtype Ada_Real_Time_Descendant is Ada_Descendant
      range Ada_Real_Time_Delays .. Ada_Real_Time_Timing_Events;
@@ -657,6 +661,10 @@ package body Rtsfind is
          elsif U_Id in Ada_Numerics_Descendant then
             Name_Buffer (13) := '.';
 
+            if U_Id in Ada_Numerics_Big_Numbers_Descendant then
+               Name_Buffer (25) := '.';
+            end if;
+
          elsif U_Id in Ada_Real_Time_Descendant then
             Name_Buffer (14) := '.';
 
diff --git a/gcc/ada/rtsfind.ads b/gcc/ada/rtsfind.ads
index e174e75..8c831f0 100644
--- a/gcc/ada/rtsfind.ads
+++ b/gcc/ada/rtsfind.ads
@@ -115,8 +115,14 @@ package Rtsfind is
 
       --  Children of Ada.Numerics
 
+      Ada_Numerics_Big_Numbers,
       Ada_Numerics_Generic_Elementary_Functions,
 
+      --  Children of Ada.Numerics.Big_Numbers
+
+      Ada_Numerics_Big_Numbers_Big_Integers,
+      Ada_Numerics_Big_Numbers_Big_Integers_Ghost,
+
       --  Children of Ada.Real_Time
 
       Ada_Real_Time_Delays,
@@ -585,6 +591,9 @@ package Rtsfind is
      RE_Detach_Handler,                  -- Ada.Interrupts
      RE_Reference,                       -- Ada.Interrupts
 
+     RE_Big_Integer,             -- Ada.Numerics.Big_Numbers.Big_Integers
+     RO_GH_Big_Integer,          -- Ada.Numerics.Big_Numbers.Big_Integers_Ghost
+
      RE_Names,                           -- Ada.Interrupts.Names
 
      RE_Clock,                           -- Ada.Real_Time
@@ -2271,6 +2280,9 @@ package Rtsfind is
      RE_Detach_Handler                   => Ada_Interrupts,
      RE_Reference                        => Ada_Interrupts,
 
+     RE_Big_Integer             => Ada_Numerics_Big_Numbers_Big_Integers,
+     RO_GH_Big_Integer          => Ada_Numerics_Big_Numbers_Big_Integers_Ghost,
+
      RE_Names                            => Ada_Interrupts_Names,
 
      RE_Clock                            => Ada_Real_Time,
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 1289f4f..9ef3a06 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -19455,8 +19455,39 @@ package body Sem_Prag is
                   end;
                end if;
 
-               Preanalyze_Assert_Expression
-                 (Expression (Variant), Any_Discrete);
+               --  Preanalyze_Assert_Expression, but without enforcing any of
+               --  the two acceptable types.
+
+               Preanalyze_Assert_Expression (Expression (Variant));
+
+               --  Expression of a discrete type is allowed
+
+               if Is_Discrete_Type (Etype (Expression (Variant))) then
+                  null;
+
+               --  Expression of a Big_Integer type (or its ghost variant) is
+               --  only allowed in Decreases clause.
+
+               elsif
+                 Is_RTE (Base_Type (Etype (Expression (Variant))),
+                         RE_Big_Integer)
+                   or else
+                 Is_RTE (Base_Type (Etype (Expression (Variant))),
+                         RO_GH_Big_Integer)
+               then
+                  if Chars (Variant) = Name_Increases then
+                     Error_Msg_N
+                       ("Loop_Variant with Big_Integer can only decrease",
+                        Expression (Variant));
+                  end if;
+
+               --  Expression of other types is not allowed
+
+               else
+                  Error_Msg_N
+                    ("expected a discrete or Big_Integer type",
+                     Expression (Variant));
+               end if;
 
                Next (Variant);
             end loop;
@@ -29415,7 +29446,36 @@ package body Sem_Prag is
          end if;
 
          Errors := Serious_Errors_Detected;
-         Preanalyze_Assert_Expression (Expr, Any_Discrete);
+
+         --  Preanalyze_Assert_Expression, but without enforcing any of the two
+         --  acceptable types.
+
+         Preanalyze_Assert_Expression (Expr);
+
+         --  Expression of a discrete type is allowed
+
+         if Is_Discrete_Type (Etype (Expr)) then
+            null;
+
+         --  Expression of a Big_Integer type (or its ghost variant) is only
+         --  allowed in Decreases clause.
+
+         elsif
+           Is_RTE (Base_Type (Etype (Expr)), RE_Big_Integer)
+             or else
+           Is_RTE (Base_Type (Etype (Expr)), RO_GH_Big_Integer)
+         then
+            if Chars (Direction) = Name_Increases then
+               Error_Msg_N
+                 ("Subprogram_Variant with Big_Integer can only decrease",
+                  Expr);
+            end if;
+
+         --  Expression of other types is not allowed
+
+         else
+            Error_Msg_N ("expected a discrete or Big_Integer type", Expr);
+         end if;
 
          --  Emit a clarification message when the variant expression
          --  contains at least one undefined reference, possibly due