with Ada.Text_IO;
with Ada.Integer_Text_IO;
procedure Example with
  Annotate => (GNATprove, Might_Not_Return)
is

   Limit : constant Integer := 1_000;

   procedure Bounded_Increment
     (Value   : in out Integer;  -- A value to increment
      Bound   : in     Integer;  -- The maximum that Value may take
      Changed :    out Boolean)  -- Did Value change?
   is
   begin
      if Value < Bound then
         Value   := Value + 1;
         Changed := True;
      else
         Changed := False;
      end if;
   end Bounded_Increment;

   Value    : Integer;
   Modified : Boolean;

begin -- procedure Example
   Ada.Text_IO.Put_Line ("Enter a number.");
   Ada.Integer_Text_IO.Get (Value);
   Bounded_Increment (Bound   => Limit / 2,
                      Value   => Value,
                      Changed => Modified);
   if Modified then
      Ada.Text_IO.Put_Line ("Your number was changed to ");
      Ada.Integer_Text_IO.Put (Item  => Value,
                                Width => 1);
   end if;
end Example;