aboutsummaryrefslogtreecommitdiff
path: root/gcc/cppdefault.cc
diff options
context:
space:
mode:
authorPiotr Trojanek <trojanek@adacore.com>2024-10-28 13:17:03 +0100
committerMarc Poulhiès <dkm@gcc.gnu.org>2024-11-12 14:00:53 +0100
commitc74c88a3e17aa26f57e01dbcce8b4e782a05bfca (patch)
treebcb59189fe549d51250774b03298421718c2749f /gcc/cppdefault.cc
parentd1a199adb9b263f5b76daa4e8a5b32ac272c9cfe (diff)
downloadgcc-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/cppdefault.cc')
0 files changed, 0 insertions, 0 deletions