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_UNCHECKED_CONVERSION RV NO_IMPLEMENTATION_ASPECT_SPECIFICATIONS RV NO_IMPLEMENTATION_PRAGMAS U system.arith_32%b s-arit32.adb 78776468 NE OL PK W ada%s ada.ads ada.ali Z ada.exceptions%s a-except.adb a-except.ali W ada.numerics%s a-numeri.ads a-numeri.ali W ada.numerics.big_numbers%s a-nubinu.ads a-nubinu.ali W ada.unchecked_conversion%s W system%s system.ads system.ali N A266:7 gnatprove intentional "exception might be raised" "Procedure Raise_Error is called to signal input errors" U system.arith_32%s s-arit32.ads 98026e24 NE OL PU 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 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-arit32.ads 20250808065140 e8522a76 system.arith_32%s D s-arit32.adb 20250808065140 af4123d0 system.arith_32%b D s-assert.ads 20250808065140 9c4520c7 system.assertions%s D s-exctab.ads 20250808065140 91bef6ef system.exception_table%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 G a e G c Z s s [to_big_integer system__arith_32__signed_conversion 119 16 62_4] G c Z s s [from_big_integer system__arith_32__signed_conversion 124 16 62_4] G c Z s s [big system__arith_32 66 13 none] G c Z s s [in_int32_range system__arith_32 70 13 none] G c Z s s [same_sign system__arith_32 75 13 none] G c Z s s [round_quotient system__arith_32 81 13 none] G c Z s b [scaled_divide32 system__arith_32 91 14 none] G c Z b b [to_int system__arith_32 59 13 none] G c Z b b [to_big_integer system__arith_32__unsigned_conversion 140 16 61_4] G c Z b b [from_big_integer system__arith_32__unsigned_conversion 145 16 61_4] G c Z b b [big system__arith_32 63 13 none] G c Z b b [to_big_integer system__arith_32__unsigned_conversion_64 140 16 67_4] G c Z b b [from_big_integer system__arith_32__unsigned_conversion_64 145 16 67_4] G c Z b b [big system__arith_32 69 13 none] G c Z b b [Oabs system__arith_32 92 13 none] G c Z b b [lo system__arith_32 99 13 none] G c Z b b [hi system__arith_32 102 13 none] G c Z b b [to_neg_int system__arith_32 105 13 none] G c Z b b [to_pos_int system__arith_32 114 13 none] G c Z b b [raise_error system__arith_32 122 14 none] G c Z b b [lemma_abs_commutation system__arith_32 132 14 none] G c Z b b [lemma_abs_div_commutation system__arith_32 137 14 none] G c Z b b [lemma_abs_mult_commutation system__arith_32 143 14 none] G c Z b b [lemma_abs_rem_commutation system__arith_32 148 14 none] G c Z b b [lemma_div_commutation system__arith_32 154 14 none] G c Z b b [lemma_div_ge system__arith_32 160 14 none] G c Z b b [lemma_ge_commutation system__arith_32 166 14 none] G c Z b b [lemma_hi_lo system__arith_32 172 14 none] G c Z b b [lemma_mult_commutation system__arith_32 178 14 none] G c Z b b [lemma_mult_non_negative system__arith_32 184 14 none] G c Z b b [lemma_mult_non_positive system__arith_32 191 14 none] G c Z b b [lemma_neg_rem system__arith_32 198 14 none] G c Z b b [lemma_not_in_range_big2xx32 system__arith_32 204 14 none] G c Z b b [lemma_rem_commutation system__arith_32 209 14 none] X 1 ada.ads 18K9*Ada 22e8 11|48r6 53r13 59r6 63r6 71r7 12|43r6 44r5 45r6 59r27 X 4 a-numeri.ads 20K13*Numerics 36e17 11|48r10 53r17 59r10 63r10 71r11 12|43r10 44r9 X 5 a-nubinu.ads 19K22*Big_Numbers 30e29 11|48r19 53r26 59r19 63r19 71r20 12|43r19 44r18 X 8 a-unccon.ads 23v14*Unchecked_Conversion 12|45w10 59r31 X 9 interfac.ads 47K9*Interfaces 247e15 11|47w6 54r13 56r21 12|54r21 55r21 57r8 65I9*Integer_32 11|54r24 56r32 92M9*Unsigned_32 12|54r32 95M9*Unsigned_64 12|55r32 184V13*Shift_Right{95M9} 12|102s52 X 10 system.ads 37K9*System 156e11 11|50r9 136r5 12|47r14 584r5 X 11 s-arit32.ads 50K16*Arith_32 10|37k9 11|136l12 136e20 12|47b21 584l12 584t20 56I12*Int32{9|65I9} 64r14 66r24 72r19 72r38 76r16 77r26 78r27 78r51 82r32 . 82r51 83r43 84r23 92r17 93r21 12|59r60 92r24 93r14 95r19 105r43 114r43 . 132r41 219r41 276r17 277r21 557r43 558r20 559r28 574r43 575r20 91U14*Scaled_Divide32 92>7 92>10 92>13 93<7 93<10 94>7 12|275b14 551l8 551t23 92i7 X{56I12} 98r46 99r46 100r46 101r21 102r29 105r44 106r44 108r28 12|276b7 . 280r35 293r49 304r22 304r44 306r49 307r49 308r49 309r24 318r42 320r35 321r35 . 322r35 329r22 329r45 331r49 332r49 333r49 334r24 343r32 344r33 346r34 358r46 . 365r32 366r33 369r37 376r18 378r19 390r40 401r42 410r40 419r29 443r14 457r40 . 468r20 469r21 471r40 490r39 491r39 492r30 535r11 535r44 92i10 Y{56I12} 98r56 99r56 100r56 101r31 102r39 105r54 106r54 108r38 12|276b10 . 281r35 293r59 304r33 304r54 306r59 307r59 308r59 309r34 318r52 320r45 321r45 . 322r45 329r33 329r55 331r59 332r59 333r59 334r34 343r42 344r43 346r44 358r56 . 365r42 366r43 369r47 376r29 378r30 390r49 401r52 410r49 419r39 443r25 457r49 . 468r30 469r31 471r50 490r49 491r49 493r30 535r27 535r59 92i13 Z{56I12} 96r14 98r65 99r66 100r68 101r41 102r51 105r63 106r64 108r48 . 12|276b13 282r35 303r17 306r68 307r69 308r71 309r44 311r16 317r17 317r69 . 318r62 320r54 321r55 322r57 328r17 331r68 332r69 333r71 334r44 336r16 342r17 . 343r52 344r55 346r53 348r47 358r17 358r68 364r17 365r52 366r55 369r56 378r42 . 399r57 400r33 401r61 419r48 434r46 464r10 468r40 469r43 471r59 490r58 491r58 . 494r30 503r49 539r19 547r19 93i7 Q{56I12} 105r18 108r18 12|277b7 377r20 380r47 444r58 446r58 539m10 547m10 93i10 R{56I12} 102r19 106r73 12|277b10 375r20 380r22 444r33 446r33 538m10 . 546m10 94b7 Round{boolean} 98r14 104r14 12|278b7 306r17 331r17 368r17 470r10 507r10 X 12 s-arit32.adb 54M12 Uns32{9|92M9} 59r53 61r68 63r24 77r11 80r11 92r38 94r12 95r12 99r35 . 99r45 102r35 102r45 105r29 114r29 135r33 166r43 172r50 224r43 253r50 280r22 . 281r22 282r22 287r12 288r12 317r58 348r36 350r26 350r39 399r46 422r33 422r46 . 487r13 488r13 503r38 510r24 510r37 516r21 522r24 557r29 574r29 55M12 Uns64{9|95M9} 67r71 69r24 83r11 99r21 102r21 154r44 172r32 178r48 209r44 . 222r44 225r48 230r44 253r32 255r22 255r41 256r22 284r13 455r12 455r25 487r24 . 488r26 495r31 495r43 496r33 497r33 499r22 499r39 500r22 500r41 59V13 To_Int[8|23]{9|65I9} 559s46 575s29 92V14 "abs"{54M12} 92b14 92>20 135s40 280s31 281s31 282s31 317s65 348s43 . 399s53 503s45 92i20 X{11|56I12} 93r10 95r30 99V13 Lo{54M12} 99b13 99>17 175s38 459s31 460s61 99m17 A{55M12} 99r52 102V13 Hi{54M12} 102b13 102>17 175s20 459s23 460s46 478s10 479s32 102m17 A{55M12} 102r65 105V13 To_Neg_Int{11|56I12} 105>25 108r19 376s63 379s19 539s51 546s15 547s30 . 557b13 568l8 568t18 105m25 A{54M12} 107r36 108r46 557b25 559r13 559r54 114V13 To_Pos_Int{11|56I12} 114>25 117r19 376s42 378s55 538s15 539s30 547s51 . 574b13 582l8 582t18 114m25 A{54M12} 116r35 117r45 574b25 575r37 122U14 Raise_Error 125r22 263b14 269l8 269t19 465s10 482s10 519s16 566s10 . 580s10 204U14 Lemma_Not_In_Range_Big2xx32 518s16 229U14 Lemma_Not_In_Range_Big2xx32 280m7 Xu{54M12} 455r19 495r38 281m7 Yu{54M12} 455r32 495r50 282m7 Zu{54M12} 348r25 350r21 422r28 478r20 479r40 480r50 487r31 488r33 496r40 . 497r40 499r46 500r48 503r27 510r19 284m7 D{55M12} 455m7 458r34 459r20 459r27 459r35 460r50 460r65 478r14 479r36 . 487r20 488r20 495r55 496r30 497r30 499r35 500r35 287m7 Qu{54M12} 372r25 378r67 379r31 487m7 499r29 502r27 511r45 516r16 522m13 . 522r19 527r27 539r42 539r63 547r42 547r63 288m7 Ru{54M12} 347r25 350r15 371r25 376r54 376r75 422r22 488m7 500r29 501r27 . 510r13 528r27 538r27 546r27 558i7 R{11|56I12} 563r10 564r17 575i7 R{11|56I12} 577r10 578r17