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 666c9bae04f86f643ebd9b4aba4cb30dcc9e0f96..970af540e9c7ee8d5fca0e4c5320c09a755c0451 100644 (file)
--- 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 01f1be2322861e8f57e7229caa6d2dc0939643d4..701065df4bf2043b9ed8cc2111e7652c5ceb439e 100644 (file)
--- 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 942c2f712fbcf35d09d46ca30ed41974eaa8a404..9cfd2ed4c48c0be6d13ba97c9ee9de656a485c65 100644 (file)
--- 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 d877251110e8519707c9594f5d67733183adccbf..f4ae89fd2e7afe377f9154bd6779b3fb82eea1c6 100644 (file)
--- 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