gcc/testsuite/gnat.dg/loop_entry2.adb

--  { dg-do compile }
--  { dg-options "-gnata" }

procedure Loop_Entry2 (S : String) is
   J : Integer := S'First;
begin
   while S(J..J+1) = S(J..J+1) loop
      pragma Loop_Invariant (for all K in J'Loop_Entry .. J => K <= J);
      J := J + 1;
   end loop;
end;