Fragment of i-c.adb from GCC 15.2.0

         To := Target'First;
         for From in Item'Range loop
            Target (To) := To_C (Item (From));

            pragma Loop_Invariant (To in Target'Range);
            pragma Loop_Invariant
              (To - Target'First = size_t (From - Item'First));
            pragma Loop_Invariant
              (for all J in Target'First .. To => Target (J)'Initialized);
            pragma Loop_Invariant
              (Target (Target'First .. To)'Initialized);
            pragma Loop_Invariant
              (for all J in Item'First .. From =>
                Target (Target'First + size_t (J - Item'First)) =
                  To_C (Item (J)));

            To := To + 1;
         end loop;