V "GNAT Lib v15" A -nostdinc A -O2 A -Wextra A -Wall A -gnatwa A -g A -gnatp A -gnatg A -march=armv8-a A -mlittle-endian A -mabi=lp64 P ZX RN RV NO_DIRECT_BOOLEAN_OPERATORS RV NO_EXCEPTIONS RV NO_IMPLICIT_CONDITIONALS RV NO_STANDARD_STORAGE_POOLS RV NO_DYNAMIC_SIZED_OBJECTS RV NO_IMPLEMENTATION_ASPECT_SPECIFICATIONS RV NO_IMPLEMENTATION_PRAGMAS U system.img_decimal_32%s s-imde32.ads efa255e6 NE OL PK W ada%s ada.ads ada.ali W ada.numerics%s a-numeri.ads a-numeri.ali W ada.numerics.big_numbers%s a-nubinu.ads a-nubinu.ali W interfaces%s interfac.ads interfac.ali W system%s system.ads system.ali W system.image_d%s Z system.image_i%s Z system.img_util%s s-imguti.adb s-imguti.ali D ada.ads 20250808065140 76789da1 ada%s D a-assert.ads 20250808065140 ba465f5c ada.assertions%s D a-except.ads 20250808065140 e7970cd9 ada.exceptions%s D a-numeri.ads 20250808065140 84bea7a3 ada.numerics%s D a-nubinu.ads 20250808065140 93f1f3d1 ada.numerics.big_numbers%s D a-nbnbig.ads 20250808065140 31ff4aa1 ada.numerics.big_numbers.big_integers_ghost%s D a-nbnbig.adb 20250808065140 e7f9abf0 ada.numerics.big_numbers.big_integers_ghost%b D a-unccon.ads 20250808065140 0e9b276f ada.unchecked_conversion%s D interfac.ads 20250808065140 9111f9c1 interfaces%s D system.ads 20250808065140 d0bef732 system%s D s-assert.ads 20250808065140 9c4520c7 system.assertions%s D s-exctab.ads 20250808065140 91bef6ef system.exception_table%s D s-imaged.ads 20250808065140 f3032752 system.image_d%s D s-imaged.adb 20250808065140 82af1050 system.image_d%b D s-imagei.ads 20250808065140 5e131ce0 system.image_i%s D s-imagei.adb 20250808065140 7e62cc2a system.image_i%b D s-imde32.ads 20250808065140 5d0e7c47 system.img_decimal_32%s D s-imguti.ads 20250808065140 7719a4b9 system.img_util%s D s-parame.ads 20250808065140 3597fc11 system.parameters%s D s-stalib.ads 20250808065140 1c9580f6 system.standard_library%s D s-traent.ads 20250808065140 c81cbf8c system.traceback_entries%s D s-valspe.ads 20250808065140 f810d31c system.val_spec%s D s-vaispe.ads 20250808065140 8280550e system.value_i_spec%s D s-vaispe.adb 20250808065140 dbcabb05 system.value_i_spec%b D s-vauspe.ads 20250808065140 89269ba5 system.value_u_spec%s D s-vauspe.adb 20250808065140 8524adb4 system.value_u_spec%b G a e G c Z s s [image_decimal system__img_decimal_32__impl 43 14 44_4] G c Z s s [set_image_decimal system__img_decimal_32__impl 55 14 44_4] G c Z s s [max_log10 system__img_decimal_32__impl__uns_spec 63 13 53_4_44_4] G c Z s s [wrap_option system__img_decimal_32__impl__uns_spec 85 13 53_4_44_4] G c Z s s [only_decimal_ghost system__img_decimal_32__impl__uns_spec 88 13 53_4_44_4] G c Z s s [only_hexa_ghost system__img_decimal_32__impl__uns_spec 99 13 53_4_44_4] G c Z s s [last_hexa_ghost system__img_decimal_32__impl__uns_spec 108 13 53_4_44_4] G c Z s s [is_based_format_ghost system__img_decimal_32__impl__uns_spec 121 13 53_4_44_4] G c Z s s [hexa_to_unsigned_ghost system__img_decimal_32__impl__uns_spec 136 13 53_4_44_4] G c Z s s [scan_overflows_ghost system__img_decimal_32__impl__uns_spec 147 13 53_4_44_4] G c Z s s [scan_based_number_ghost system__img_decimal_32__impl__uns_spec 159 13 53_4_44_4] G c Z s s [lemma_scan_based_number_ghost_base system__img_decimal_32__impl__uns_spec 176 14 53_4_44_4] G c Z s s [lemma_scan_based_number_ghost_underscore system__img_decimal_32__impl__uns_spec 193 14 53_4_44_4] G c Z s s [lemma_scan_based_number_ghost_overflow system__img_decimal_32__impl__uns_spec 210 14 53_4_44_4] G c Z s s [lemma_scan_based_number_ghost_step system__img_decimal_32__impl__uns_spec 230 14 53_4_44_4] G c Z s s [exponent_unsigned_ghost system__img_decimal_32__impl__uns_spec 252 13 53_4_44_4] G c Z s s [lemma_exponent_unsigned_ghost_base system__img_decimal_32__impl__uns_spec 262 14 53_4_44_4] G c Z s s [lemma_exponent_unsigned_ghost_overflow system__img_decimal_32__impl__uns_spec 273 14 53_4_44_4] G c Z s s [lemma_exponent_unsigned_ghost_step system__img_decimal_32__impl__uns_spec 285 14 53_4_44_4] G c Z s s [raw_unsigned_starts_as_based_ghost system__img_decimal_32__impl__uns_spec 298 13 53_4_44_4] G c Z s s [raw_unsigned_is_based_ghost system__img_decimal_32__impl__uns_spec 312 13 53_4_44_4] G c Z s s [is_raw_unsigned_format_ghost system__img_decimal_32__impl__uns_spec 328 13 53_4_44_4] G c Z s s [scan_split_no_overflow_ghost system__img_decimal_32__impl__uns_spec 364 13 53_4_44_4] G c Z s s [scan_split_value_ghost system__img_decimal_32__impl__uns_spec 409 13 53_4_44_4] G c Z s s [raw_unsigned_no_overflow_ghost system__img_decimal_32__impl__uns_spec 455 13 53_4_44_4] G c Z s s [scan_raw_unsigned_ghost system__img_decimal_32__impl__uns_spec 478 13 53_4_44_4] G c Z s s [raw_unsigned_last_ghost system__img_decimal_32__impl__uns_spec 496 13 53_4_44_4] G c Z s s [slide_to_1 system__img_decimal_32__impl__uns_spec 529 13 53_4_44_4] G c Z s s [slide_if_necessary system__img_decimal_32__impl__uns_spec 537 13 53_4_44_4] G c Z s s [is_unsigned_ghost system__img_decimal_32__impl__uns_spec 541 13 53_4_44_4] G c Z s s [is_value_unsigned_ghost system__img_decimal_32__impl__uns_spec 560 13 53_4_44_4] G c Z s s [prove_scan_based_number_ghost_eq system__img_decimal_32__impl__uns_spec 575 14 53_4_44_4] G c Z s s [prove_scan_only_decimal_ghost system__img_decimal_32__impl__uns_spec 596 14 53_4_44_4] G c Z s s [uns_optionIP system__img_decimal_32__impl__uns_spec 75 9 53_4_44_4] G c Z s s [split_value_ghostIP system__img_decimal_32__impl__uns_spec 358 9 53_4_44_4] G c Z s s [uns_is_valid_int system__img_decimal_32__impl__int_spec 70 13 54_4_44_4] G c Z s s [is_int_of_uns system__img_decimal_32__impl__int_spec 77 13 54_4_44_4] G c Z s s [abs_uns_of_int system__img_decimal_32__impl__int_spec 91 13 54_4_44_4] G c Z s s [slide_to_1 system__img_decimal_32__impl__int_spec 97 13 54_4_44_4] G c Z s s [slide_if_necessary system__img_decimal_32__impl__int_spec 105 13 54_4_44_4] G c Z s s [is_integer_ghost system__img_decimal_32__impl__int_spec 109 13 54_4_44_4] G c Z s s [is_value_integer_ghost system__img_decimal_32__impl__int_spec 136 13 54_4_44_4] G c Z s s [prove_scan_only_decimal_ghost system__img_decimal_32__impl__int_spec 156 14 54_4_44_4] G c Z s s [image_integer system__img_decimal_32__impl__image_i 68 14 56_4_44_4] G c Z s s [set_image_integer system__img_decimal_32__impl__image_i 82 14 56_4_44_4] G c Z s s [uns_of_non_positive system__img_decimal_32__impl__image_i 53 13 56_4_44_4] G c Z s s [set_digits system__img_decimal_32__impl__image_i 56 14 56_4_44_4] G c Z s s [to_big_integer system__img_decimal_32__impl__image_i__unsigned_conversion 140 16 75_4_56_4_44_4] G c Z s s [from_big_integer system__img_decimal_32__impl__image_i__unsigned_conversion 145 16 75_4_56_4_44_4] G c Z s s [lemma_non_zero system__img_decimal_32__impl__image_i 89 14 56_4_44_4] G c Z s s [lemma_div_commutation system__img_decimal_32__impl__image_i 95 14 56_4_44_4] G c Z s s [lemma_div_twice system__img_decimal_32__impl__image_i 101 14 56_4_44_4] X 9 interfac.ads 47K9*Interfaces 247e15 17|36w6 41r21 42r21 65I9*Integer_32 17|41r32 92M9*Unsigned_32 17|42r32 X 10 system.ads 37K9*System 156e11 17|37r6 39r9 77r5 X 13 s-imaged.ads 41k16*Image_D 72e19 17|37w13 44r24 43U14*Image_Decimal 17|51r19[44] 55U14*Set_Image_Decimal 17|67r19[44] X 17 s-imde32.ads 39K16*Img_Decimal_32 10|37k9 17|77l12 77e26 41I12*Int32{9|65I9} 44r33 47r15 60r15 42M12*Uns32{9|92M9} 44r40 44K12*Impl[13|41] 51r14 67r14 46U14*Image_Decimal32=51:19 47i7 V{9|65I9} 48a7 S{string} 49i7 P{natural} 50i7 Scale{integer} 59U14*Set_Image_Decimal32=67:19 60i7 V{9|65I9} 61a7 S{string} 62i7 P{natural} 63i7 Scale{integer} 64i7 Fore{natural} 65i7 Aft{natural} 66i7 Exp{natural}