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/cppdefault.cc | |
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/cppdefault.cc')
0 files changed, 0 insertions, 0 deletions