GNATprove : "overflow check might fail" in exponentiation function

Question

I can't solve this problem with SPARK 2018, I think I need some invariant to solve the problem of overflow, but I have already tried everything and can not find it. If someone could shed some light on my problem.

I'll try Exponentiation by simple mode and by binary mode by successive squaring.

Thank you very much in advance.

THIS IS THE ERRORS:

practica.adb:20:17: medium: overflow check might fail (e.g. when A = 0 and r = 1)
practica.adb:40:33: medium: loop invariant might fail after first iteration, cannot prove r * (x ** y) = (M ** N (e.g. when M = 0 and N = 0 and r = 0 and x = 0 and y = 0)
practica.adb:44:20: medium: overflow check might fail (e.g. when x = 0)
practica.adb:47:20: medium: overflow check might fail (e.g. when r = 0 and x = 0)
practica.ads:8:19: medium: postcondition might fail, cannot prove power_simple'Result = (A ** B (e.g. when A = 0 and B = 2 and power_simple'Result = 0)
practica.ads:16:22: medium: postcondition might fail, cannot prove power_binary'Result = (M ** N (e.g. when M = 0 and N = 2 and power_binary'Result = 0)

This is my code .ads

package Practica with SPARK_Mode => On is

   -- Funcion que calcula la potenciacion de A elevado a B
   function power_simple (A : Natural; B : Natural) return Integer
     with Depends => (power_simple'Result => (A,B)), 
          Pre => B >= 0,
          Post => power_simple'Result = (A ** B)
                  and (if B = 0 then power_simple'Result = 1);


   -- Funcion que calcula mediante exponenciacion binaria, potencias de un numero dado
   function power_binary (M : Integer; N : Integer) return Integer
       with  Depends => (power_binary'Result => (M,N)),
             Pre => (M >= 0) and (N >= 0),
             Post => power_binary'Result = (M ** N)
             and (if N = 0 then power_binary'Result = 1);

end Practica;

and this is my code .adb

   -- Funcion que calcula la potenciacion de A elevado a B
   function  power_simple (A : Natural; B : Natural) return Integer is
      x : Integer := 0;
      r : Integer := 1;
   begin

      while x /= B loop
         pragma Loop_Invariant (0 <= x);
         pragma Loop_Invariant (x <= B);
         pragma Loop_Invariant (r = (A ** x));
         pragma Loop_Invariant (r >= 0);
         pragma Loop_Invariant ((if x = 0 then r /= 0));
         pragma Loop_Variant (Decreases => B - x);

         r := r * A;
         x := x + 1;

      end loop;

      if (B = 0) then r := 1; end if;
      if (B = 1) then r := A; end if;

      return r;
   end power_simple;


   --Funcion que calcula mediante exponenciacion binaria, potencias de un numero
   function power_binary(M : Integer; N : Integer) return Integer is
      x : Integer := M;
      y : Integer := N;
      r : Integer := 1;
   begin
      while y /= 0 loop
         pragma Loop_Invariant ((x >= 0) and (y >= 0));
         pragma Loop_Invariant (r * (x ** y) = (M ** N));
         pragma Loop_Variant (Decreases => y);

         if (y mod 2) = 0 then
            x := x * x;
            y := y / 2;
         else
            r := r * x;
            y := y - 1;
         end if;
      end loop;

      if (N = 0) then r := 1; end if;
      if (N = 1) then r := M; end if;

      return r;
   end power_binary;