From: Piotr Trojanek <troja...@adacore.com>
For certification of a light SPARK runtime libraries we now accept
expressions of type SPARK.Big_Integers.Big_Integer in subprogram and
loop variants.
gcc/ada/ChangeLog:
* exp_util.adb (Make_Variant_Comparison): Accept new types in
expansion.
* rtsfind.adb (Get_Unit_Name): Support SPARK.Big_Integers.
* rtsfind.ads (RTU_Id, RE_Id, RE_Unit_Table): Support new type
and its enclosing unit.
* sem_prag.adb (Analyze_Pragma): Support new type in pragma
Loop_Variant.
(Analyze_Subprogram_Variant_In_Decl_Part): Support new type in
aspect Subprogram_Variant.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/exp_util.adb | 6 +++++-
gcc/ada/rtsfind.adb | 6 ++++++
gcc/ada/rtsfind.ads | 10 ++++++++++
gcc/ada/sem_prag.adb | 5 +++++
4 files changed, 26 insertions(+), 1 deletion(-)
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 666c9bae04f..970af540e9c 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -10838,7 +10838,11 @@ package body Exp_Util is
-- operator on private type might not be visible and won't be
-- resolved.
- else pragma Assert (Is_RTE (Base_Type (Typ), RE_Big_Integer));
+ else pragma Assert (Is_RTE (Base_Type (Typ), RE_Big_Integer)
+ or else
+ Is_RTE (Base_Type (Typ), RO_GH_Big_Integer)
+ or else
+ Is_RTE (Base_Type (Typ), RO_SP_Big_Integer));
return
Make_Function_Call (Loc,
Name =>
diff --git a/gcc/ada/rtsfind.adb b/gcc/ada/rtsfind.adb
index 01f1be23228..701065df4bf 100644
--- a/gcc/ada/rtsfind.adb
+++ b/gcc/ada/rtsfind.adb
@@ -604,6 +604,9 @@ package body Rtsfind is
subtype Interfaces_C_Descendant is Interfaces_Descendant
range Interfaces_C_Strings .. Interfaces_C_Strings;
+ subtype SPARK_Descendant is RTU_Id
+ range SPARK_Big_Integers .. SPARK_Big_Integers;
+
subtype System_Descendant is RTU_Id
range System_Address_To_Access_Conversions .. System_Tasking_Stages;
@@ -699,6 +702,9 @@ package body Rtsfind is
Name_Buffer (13) := '.';
end if;
+ elsif U_Id in SPARK_Descendant then
+ Name_Buffer (6) := '.';
+
elsif U_Id in System_Descendant then
Name_Buffer (7) := '.';
diff --git a/gcc/ada/rtsfind.ads b/gcc/ada/rtsfind.ads
index 942c2f712fb..9cfd2ed4c48 100644
--- a/gcc/ada/rtsfind.ads
+++ b/gcc/ada/rtsfind.ads
@@ -193,6 +193,14 @@ package Rtsfind is
Interfaces_C_Strings,
+ -- Package SPARK
+
+ SPARK,
+
+ -- Children of SPARK
+
+ SPARK_Big_Integers,
+
-- Package System
System,
@@ -575,6 +583,7 @@ package Rtsfind is
RE_Big_Integer, -- Ada.Numerics.Big_Numbers.Big_Integers
RO_GH_Big_Integer, -- Ada.Numerics.Big_Numbers.Big_Integers_Ghost
+ RO_SP_Big_Integer, -- SPARK.Big_Integers
RE_Names, -- Ada.Interrupts.Names
@@ -2222,6 +2231,7 @@ package Rtsfind is
RE_Big_Integer => Ada_Numerics_Big_Numbers_Big_Integers,
RO_GH_Big_Integer => Ada_Numerics_Big_Numbers_Big_Integers_Ghost,
+ RO_SP_Big_Integer => SPARK_Big_Integers,
RE_Names => Ada_Interrupts_Names,
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index d877251110e..f4ae89fd2e7 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -20498,6 +20498,9 @@ package body Sem_Prag is
or else
Is_RTE (Base_Type (Etype (Expression (Variant))),
RO_GH_Big_Integer)
+ or else
+ Is_RTE (Base_Type (Etype (Expression (Variant))),
+ RO_SP_Big_Integer)
then
if Chars (Variant) = Name_Increases then
Error_Msg_N
@@ -30966,6 +30969,8 @@ package body Sem_Prag is
Is_RTE (Base_Type (Etype (Expr)), RE_Big_Integer)
or else
Is_RTE (Base_Type (Etype (Expr)), RO_GH_Big_Integer)
+ or else
+ Is_RTE (Base_Type (Etype (Expr)), RO_SP_Big_Integer)
then
if Chars (Direction) = Name_Increases then
Error_Msg_N
--
2.43.0
