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.
Tested on x86_64-pc-linux-gnu, committed on trunk
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.
diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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