diff options
| author | Piotr Trojanek <trojanek@adacore.com> | 2024-10-28 13:17:03 +0100 |
|---|---|---|
| committer | Marc Poulhiès <dkm@gcc.gnu.org> | 2024-11-12 14:00:53 +0100 |
| commit | c74c88a3e17aa26f57e01dbcce8b4e782a05bfca (patch) | |
| tree | bcb59189fe549d51250774b03298421718c2749f /gcc | |
| parent | d1a199adb9b263f5b76daa4e8a5b32ac272c9cfe (diff) | |
| download | gcc-c74c88a3e17aa26f57e01dbcce8b4e782a05bfca.zip gcc-c74c88a3e17aa26f57e01dbcce8b4e782a05bfca.tar.gz gcc-c74c88a3e17aa26f57e01dbcce8b4e782a05bfca.tar.bz2 | |
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.
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/exp_util.adb | 6 | ||||
| -rw-r--r-- | gcc/ada/rtsfind.adb | 6 | ||||
| -rw-r--r-- | gcc/ada/rtsfind.ads | 10 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 5 |
4 files changed, 26 insertions, 1 deletions
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index 666c9ba..970af54 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 01f1be2..701065d 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 942c2f7..9cfd2ed 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 d877251..f4ae89f 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 |