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
RV NO_ELABORATION_CODE

U system.vs_llu%s	s-vs_llu.ads		2c87250b EE OL PR
W system%s		system.ads		system.ali
W system.unsigned_types%s  s-unstyp.ads		s-unstyp.ali

D system.ads		20250808065140 d0bef732 system%s
D s-unstyp.ads		20250808065140 fa2a7f59 system.unsigned_types%s
D s-valspe.ads		20250808065140 f810d31c system.val_spec%s
D s-vauspe.ads		20250808065140 89269ba5 system.value_u_spec%s
D s-vauspe.adb		20250808065140 8524adb4 system.value_u_spec%b
D s-vs_llu.ads		20250808065140 8f3536c5 system.vs_llu%s
G a e
G c Z s s [max_log10 system__vs_llu__spec 63 13 56_4]
G c Z s s [wrap_option system__vs_llu__spec 85 13 56_4]
G c Z s s [only_decimal_ghost system__vs_llu__spec 88 13 56_4]
G c Z s s [only_hexa_ghost system__vs_llu__spec 99 13 56_4]
G c Z s s [last_hexa_ghost system__vs_llu__spec 108 13 56_4]
G c Z s s [is_based_format_ghost system__vs_llu__spec 121 13 56_4]
G c Z s s [hexa_to_unsigned_ghost system__vs_llu__spec 136 13 56_4]
G c Z s s [scan_overflows_ghost system__vs_llu__spec 147 13 56_4]
G c Z s s [scan_based_number_ghost system__vs_llu__spec 159 13 56_4]
G c Z s s [lemma_scan_based_number_ghost_base system__vs_llu__spec 176 14 56_4]
G c Z s s [lemma_scan_based_number_ghost_underscore system__vs_llu__spec 193 14 56_4]
G c Z s s [lemma_scan_based_number_ghost_overflow system__vs_llu__spec 210 14 56_4]
G c Z s s [lemma_scan_based_number_ghost_step system__vs_llu__spec 230 14 56_4]
G c Z s s [exponent_unsigned_ghost system__vs_llu__spec 252 13 56_4]
G c Z s s [lemma_exponent_unsigned_ghost_base system__vs_llu__spec 262 14 56_4]
G c Z s s [lemma_exponent_unsigned_ghost_overflow system__vs_llu__spec 273 14 56_4]
G c Z s s [lemma_exponent_unsigned_ghost_step system__vs_llu__spec 285 14 56_4]
G c Z s s [raw_unsigned_starts_as_based_ghost system__vs_llu__spec 298 13 56_4]
G c Z s s [raw_unsigned_is_based_ghost system__vs_llu__spec 312 13 56_4]
G c Z s s [is_raw_unsigned_format_ghost system__vs_llu__spec 328 13 56_4]
G c Z s s [scan_split_no_overflow_ghost system__vs_llu__spec 364 13 56_4]
G c Z s s [scan_split_value_ghost system__vs_llu__spec 409 13 56_4]
G c Z s s [raw_unsigned_no_overflow_ghost system__vs_llu__spec 455 13 56_4]
G c Z s s [scan_raw_unsigned_ghost system__vs_llu__spec 478 13 56_4]
G c Z s s [raw_unsigned_last_ghost system__vs_llu__spec 496 13 56_4]
G c Z s s [slide_to_1 system__vs_llu__spec 529 13 56_4]
G c Z s s [slide_if_necessary system__vs_llu__spec 537 13 56_4]
G c Z s s [is_unsigned_ghost system__vs_llu__spec 541 13 56_4]
G c Z s s [is_value_unsigned_ghost system__vs_llu__spec 560 13 56_4]
G c Z s s [prove_scan_based_number_ghost_eq system__vs_llu__spec 575 14 56_4]
G c Z s s [prove_scan_only_decimal_ghost system__vs_llu__spec 596 14 56_4]
G c Z s s [uns_optionIP system__vs_llu__spec 75 9 56_4]
G c Z s s [split_value_ghostIP system__vs_llu__spec 358 9 56_4]
X 1 system.ads
37K9*System 156e11 6|48r6 49r6 51r9 56r24 58r5
X 2 s-unstyp.ads
38K16*Unsigned_Types 256e26 6|48w13 54r34
46M9*Long_Long_Unsigned 6|54r49