From: Piotr Trojanek <trojanek@adacore.com>
Date: Mon, 28 Oct 2024 12:17:03 +0000 (+0100)
Subject: ada: Accept SPARK.Big_Integers.Big_Integer where Big_Integer is accepted
X-Git-Tag: basepoints/gcc-16~4403
X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=c74c88a3e17aa26f57e01dbcce8b4e782a05bfca;p=thirdparty%2Fgcc.git

ada: Accept SPARK.Big_Integers.Big_Integer where Big_Integer is accepted

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.
---

diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 666c9bae04f8..970af540e9c7 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 01f1be232286..701065df4bf2 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 942c2f712fbc..9cfd2ed4c48c 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 d877251110e8..f4ae89fd2e7a 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