[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.
This commit is contained in:
parent
2fe776e2d3
commit
93e7c91eb7
6 changed files with 137 additions and 7 deletions
|
@ -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)))));
|
||||
|
||||
|
|
|
@ -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;
|
||||
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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) := '.';
|
||||
|
||||
|
|
|
@ -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,
|
||||
|
|
|
@ -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
|
||||
|
|
Loading…
Add table
Reference in a new issue