Prove absence of overflows for fractional numbers

Closes #4

JWX.gpr

@@ -93,4 +93,17 @@ project JWX is
       for Switches use ("-Wa", "-a", "-p");
    end Stack;
 
+   package Prove is
+      for Proof_Switches ("Ada") use
+      (
+         "-j0",
+         "--prover=z3,cvc4,altergo",
+         "--steps=1000",
+         "--timeout=60",
+         "--memlimit=1000",
+         "--checks-as-errors",
+         "--warnings=error"
+      );
+   end Prove;
+
 end JWX;

Makefile

@@ -1,4 +1,4 @@
-GNATPROVE_OPTS = --prover=z3,cvc4 -j2 --codepeer=off --output-header --no-inlining --proof=progressive --steps=100
+GNATPROVE_OPTS = -j0 --output-header
 COMMON_OPTS = -Xlibtype=dynamic
 
 EXAMPLES = b64 json area jwt authproxy

src/jwx-json.adb

@@ -723,7 +723,6 @@ is
          return;
       end if;
 
-      Result := 1;
       for I in 1 .. Scale
       loop
          pragma Loop_Invariant (Result > 0);
@@ -810,13 +809,13 @@ is
          declare
             Tmp : Real_Type := Real_Type (Integer_Component) + Fractional_Component;
          begin
-            if Match_Exponent = Match_OK
+            if Match_Exponent = Match_OK and Tmp >= 1.0
             then
                if Scale_Negative
                then
                   Tmp := Tmp / Real_Type (Scale);
                else
-                  if Tmp >= Real_Type'Last / Real_Type (Scale)
+                  if Real_Type (Scale) >= Real_Type'Last / Tmp
                   then
                      return;
                   end if;