Update Why3 and refresh generated files.

.gitignore

@@ -12,6 +12,15 @@
 /libwmp.a
 
 /autom4te.cache/
+
 /lib/*.o
 /lib/.deps/
 /lib/.dirstamp
+/lib/extracted
+
+/lib/alias.c
+/lib/c.c
+/lib/fxp.c
+/lib/uint32gmp.c
+/lib/uint64gmp.c
+/lib/z.c

Makefile.am

@@ -5,14 +5,12 @@ EXTRA_DIST = COPYING.md COPYING.GPLv3.md NEWS.md README.md
 lib_LIBRARIES = libwmp.a
 
 libwmp_a_SOURCES = \
-  lib/int.h lib/int32.h lib/uint32gmp.h lib/int64.h lib/uint64.h lib/uint64gmp.h lib/fxp.h \
-  lib/euclideandivision.h lib/computerdivision.h lib/bool.h \
-  lib/array.h lib/map.h lib/c.h lib/power.h lib/types.h lib/realinfix.h lib/minmax.h \
-  lib/explog.h lib/square.h \
+  lib/uint32gmp.h lib/uint64gmp.h lib/fxp.h lib/c.h \
   lib/util.c lib/util.h lib/utilold.c lib/utilold.h \
   lib/logical.c lib/logical.h \
   lib/logicalutil.c lib/logicalutil.h \
   lib/logicalold.c lib/logicalold.h \
+  lib/baseinfo.c lib/baseinfo.h \
   lib/compare.c lib/compare.h \
   lib/add.c lib/add.h lib/sub.c lib/sub.h \
   lib/add_1.c lib/add_1.h lib/sub_1.c lib/sub_1.h \
@@ -21,10 +19,17 @@ libwmp_a_SOURCES = \
   lib/div.c lib/div.h \
   lib/powm.c lib/powm.h lib/binverttab.h \
   lib/sqrt.c lib/sqrt.h lib/sqrt1.c lib/sqrt1.h lib/sqrtinit.h \
-  lib/alias.h lib/abs.h \
-  lib/z.c lib/z.h lib/zutil.c lib/zutil.h lib/set.c lib/set.h lib/zadd.c lib/zadd.h \
-  lib/zcmp.c lib/zcmp.h lib/zsub.c lib/zsub.h lib/zmul.c lib/zmul.h \
-  lib/zmul2exp.c lib/zmul2exp.h lib/zdiv2exp.c lib/zdiv2exp.h
-
+  lib/get_str.c lib/get_str.h \
+  lib/set_str.c lib/set_str.h \
+  lib/alias.h \
+  lib/z.h lib/zutil.c lib/zutil.h lib/set.c lib/set.h lib/zadd.c lib/zadd.h \
+  lib/zabs.c lib/zabs.h \
+  lib/zcmp.c lib/zcmp.h \
+  lib/zcmpabs.c lib/zcmpabs.h \
+  lib/zsub.c lib/zsub.h lib/zmul.c lib/zmul.h \
+  lib/zmul2exp.c lib/zmul2exp.h lib/zdiv2exp.c lib/zdiv2exp.h \
+  lib/zdiv.c lib/zdiv.h \
+  lib/zget_str.c lib/zget_str.h \
+  lib/zset_str.c lib/zset_str.h
 
 include_HEADERS = wmp.h wmp-gmp.h

lib/abs.h

-#ifndef ABS_H_INCLUDED
-
-#include <stdlib.h>
-#include <stdint.h>
-#include <stdio.h>
-#include <assert.h>
-#include <alloca.h>
-
-#define ABS_H_INCLUDED
-#endif // ABS_H_INCLUDED

lib/add.c

-#include <stdlib.h>
+#include "add.h"
 #include <stdint.h>
-#include <stdio.h>
-#include <assert.h>
-#include <alloca.h>
-#include "c.h"
-
-#include "int.h"
-
-#include "int32.h"
-
-#include "uint64gmp.h"
-
-#include "types.h"
-
-#include "array.h"
-
-#include "map.h"
-
-#include "power.h"
-
-#include "alias.h"
 
 uint64_t wmpn_add_n(uint64_t * r, uint64_t * x, uint64_t * y, int32_t sz) {
   uint64_t lx, ly, c;
@@ -150,4 +130,3 @@ uint64_t add_ry(uint64_t * x, int32_t sx, uint64_t * y, int32_t sy) {
 uint64_t add_n_rxy(uint64_t * x, int32_t sx) {
   return wmpn_add_n(x, x, x, sx);
 }
-

lib/add.h

 #ifndef ADD_H_INCLUDED
 
-#include <stdlib.h>
+#include "c.h"
+#include "uint64gmp.h"
+#include "alias.h"
 #include <stdint.h>
-#include <stdio.h>
-#include <assert.h>
-#include <alloca.h>
+
 uint64_t wmpn_add_n(uint64_t * r, uint64_t * x, uint64_t * y, int32_t sz);
 
 uint64_t wmpn_add(uint64_t * r, uint64_t * x, int32_t sx, uint64_t * y,

lib/add_1.c

-#include <stdlib.h>
+#include "add_1.h"
 #include <stdint.h>
-#include <stdio.h>
-#include <assert.h>
-#include <alloca.h>
-#include "int.h"
-
-#include "int32.h"
-
-#include "uint64gmp.h"
-
-#include "power.h"
-
-#include "c.h"
-
-#include "array.h"
-
-#include "map.h"
-
-#include "types.h"
-
-#include "euclideandivision.h"
 
 uint64_t wmpn_add_1(uint64_t * r, uint64_t * x, int32_t sz, uint64_t y) {
   uint64_t lx;
@@ -119,4 +99,3 @@ uint64_t wmpn_add_1_in_place(uint64_t * x, int32_t sz, uint64_t y) {
   }
   return c;
 }
-

lib/add_1.h

 #ifndef ADD_1_H_INCLUDED
 
-#include <stdlib.h>
+#include "uint64gmp.h"
+#include "c.h"
 #include <stdint.h>
-#include <stdio.h>
-#include <assert.h>
-#include <alloca.h>
+
 uint64_t wmpn_add_1(uint64_t * r, uint64_t * x, int32_t sz, uint64_t y);
 
 void wmpn_incr(uint64_t * x, uint64_t y);

lib/addold.c

-#include <stdlib.h>
+#include "addold.h"
 #include <stdint.h>
-#include <stdio.h>
-#include <assert.h>
-#include <alloca.h>
-#include "c.h"
-
-#include "int.h"
-
-#include "int32.h"
-
-#include "uint64gmp.h"
-
-#include "types.h"
-
-#include "array.h"
-
-#include "map.h"
-
-#include "power.h"
-
-#include "alias.h"
 
 uint64_t wmpn_add_n1(uint64_t * r, uint64_t * x, uint64_t * y, int32_t sz) {
   uint64_t lx, ly, c;
@@ -116,4 +96,3 @@ uint64_t wmpn_add_in_place(uint64_t * x, int32_t sx, uint64_t * y, int32_t sy) {
   }
   return c;
 }
-

lib/addold.h

 #ifndef ADDOLD_H_INCLUDED
 
-#include <stdlib.h>
+#include "c.h"
+#include "uint64gmp.h"
+#include "alias.h"
 #include <stdint.h>
-#include <stdio.h>
-#include <assert.h>
-#include <alloca.h>
+
 uint64_t wmpn_add_n1(uint64_t * r, uint64_t * x, uint64_t * y, int32_t sz);
 
 uint64_t wmpn_add1(uint64_t * r, uint64_t * x, int32_t sx, uint64_t * y,

lib/alias.h

 #ifndef ALIAS_H_INCLUDED
 
-#include <stdlib.h>
+#include "c.h"
+#include "uint64gmp.h"
 #include <stdint.h>
-#include <stdio.h>
-#include <assert.h>
-#include <alloca.h>
-
-struct __open_sep_result
-{ uint64_t *__field_0;
-uint64_t *__field_1;
-uint64_t *__field_2;
+
+struct __open_sep_result {
+  uint64_t *__field_0;
+  uint64_t *__field_1;
+  uint64_t *__field_2;
 };
 
-struct __open_rx_result
-{ uint64_t *__field_0;
-uint64_t *__field_1;
-uint64_t *__field_2;
+struct __open_rx_result {
+  uint64_t *__field_0;
+  uint64_t *__field_1;
+  uint64_t *__field_2;
 };
 
-struct __open_shift_sep_result
-{ uint64_t *__field_0;
-uint64_t *__field_1;
+struct __open_shift_sep_result {
+  uint64_t *__field_0;
+  uint64_t *__field_1;
 };
 
 static inline struct __open_sep_result
-open_sep (uint64_t * r, uint64_t * x, int32_t sx, uint64_t * y, int32_t sy)
+open_sep (uint64_t *r, uint64_t *x, int32_t sx, uint64_t *y, int32_t sy)
 {
-struct __open_sep_result result;
-result.__field_0 = r;
-result.__field_1 = x;
-result.__field_2 = y;
-return result;
+  struct __open_sep_result result;
+  result.__field_0 = r;
+  result.__field_1 = x;
+  result.__field_2 = y;
+  return result;
 }
 
 static inline struct __open_rx_result
-open_rx (uint64_t * x, int32_t sx, uint64_t * y, int32_t sy)
+open_rx (uint64_t *x, int32_t sx, uint64_t *y, int32_t sy)
 {
-struct __open_rx_result result;
-result.__field_0 = x;
-result.__field_1 = x;
-result.__field_2 = y;
-return result;
+  struct __open_rx_result result;
+  result.__field_0 = x;
+  result.__field_1 = x;
+  result.__field_2 = y;
+  return result;
 }
 
 static inline struct __open_shift_sep_result
-open_shift_sep (uint64_t * r, uint64_t * x, int32_t sz)
+open_shift_sep (uint64_t *r, uint64_t *x, int32_t sz)
 {
-struct __open_shift_sep_result result;
-result.__field_0 = r;
-result.__field_1 = x;
-return result;
+  struct __open_shift_sep_result result;
+  result.__field_0 = r;
+  result.__field_1 = x;
+  return result;
 }
 
 #define ALIAS_H_INCLUDED

lib/array.h

-#ifndef ARRAY_H_INCLUDED
-
-#include <stdlib.h>
-#include <stdint.h>
-#include <stdio.h>
-#include <assert.h>
-#include <alloca.h>
-
-
-
-
-
-
-#define ARRAY_H_INCLUDED
-#endif // ARRAY_H_INCLUDED

lib/baseinfo.c

+#include "baseinfo.h"
+#include <stdint.h>
+
+uint32_t wmpn_base_power_of_two_p(uint64_t b) {
+  if (b == UINT64_C(2)) {
+    return 1U;
+  } else {
+    if (b == UINT64_C(4)) {
+      return 2U;
+    } else {
+      if (b == UINT64_C(8)) {
+        return 3U;
+      } else {
+        if (b == UINT64_C(16)) {
+          return 4U;
+        } else {
+          if (b == UINT64_C(32)) {
+            return 5U;
+          } else {
+            if (b == UINT64_C(64)) {
+              return 6U;
+            } else {
+              if (b == UINT64_C(128)) {
+                return 7U;
+              } else {
+                if (b == UINT64_C(256)) {
+                  return 8U;
+                } else {
+                  return 0U;
+                }
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+}
+struct wmpn_base_info;
+
+
+struct wmpn_base_info wmpn_get_base_info(uint64_t b) {
+  uint64_t m;
+  uint64_t p;
+  uint32_t exp;
+  struct wmpn_base_info wmpn_base_info;
+  m = UINT64_C(0xFFFFFFFFFFFFFFFF) / b;
+  p = b;
+  exp = 1U;
+  while (p <= m) {
+    p = p * b;
+    exp = exp + 1U;
+  }
+  wmpn_base_info.exp = exp;
+  wmpn_base_info.bb = p;
+  return wmpn_base_info;
+}
+
+uint64_t wmpn_limb_size_in_base_2(uint64_t u) {
+  uint64_t shift;
+  shift = (uint64_t)__builtin_clzll(u);
+  return UINT64_C(64) - shift;
+}

lib/baseinfo.h

+#ifndef BASEINFO_H_INCLUDED
+
+#include "logical.h"
+#include <stdint.h>
+
+uint32_t wmpn_base_power_of_two_p(uint64_t b);
+
+struct wmpn_base_info {
+  uint32_t exp;
+  uint64_t bb;
+};
+
+struct wmpn_base_info wmpn_get_base_info(uint64_t b);
+
+uint64_t wmpn_limb_size_in_base_2(uint64_t u);
+
+#define BASEINFO_H_INCLUDED
+#endif // BASEINFO_H_INCLUDED

lib/bool.h

-#ifndef BOOL_H_INCLUDED
-
-#include <stdlib.h>
-#include <stdint.h>
-#include <stdio.h>
-#include <assert.h>
-#include <alloca.h>
-int implb(int x, int y);
-
-#define BOOL_H_INCLUDED
-#endif // BOOL_H_INCLUDED

lib/c.h

 #ifndef C_H_INCLUDED
 
-#include <stdlib.h>
+#include "uint32gmp.h"
 #include <stdint.h>
+#include <stdlib.h>
 #include <stdio.h>
 #include <assert.h>
 #include <alloca.h>
 #define IGNORE2(x,y) do { (void)(x); (void)(y); } while (0)
 #define IGNORE3(x,y,z) do { (void)(x); (void)(y); (void)(z); } while (0)
+
 #define C_H_INCLUDED
 #endif // C_H_INCLUDED

lib/compare.c

-#include <stdlib.h>
+#include "compare.h"
 #include <stdint.h>
-#include <stdio.h>
-#include <assert.h>
-#include <alloca.h>
-#include "int.h"
-
-#include "int32.h"
-
-#include "uint64gmp.h"
-
-#include "power.h"
-
-#include "c.h"
-
-#include "map.h"
-
-#include "types.h"
 
 int32_t wmpn_cmp(uint64_t * x, uint64_t * y, int32_t sz) {
   int32_t i;
@@ -35,4 +19,3 @@ int32_t wmpn_cmp(uint64_t * x, uint64_t * y, int32_t sz) {
   }
   return 0;
 }
-

lib/compare.h

 #ifndef COMPARE_H_INCLUDED
 
-#include <stdlib.h>
+#include "uint64gmp.h"
+#include "c.h"
 #include <stdint.h>
-#include <stdio.h>
-#include <assert.h>
-#include <alloca.h>
+
 int32_t wmpn_cmp(uint64_t * x, uint64_t * y, int32_t sz);
 
 #define COMPARE_H_INCLUDED

lib/computerdivision.h

-#ifndef COMPUTERDIVISION_H_INCLUDED
-
-#include <stdlib.h>
-#include <stdint.h>
-#include <stdio.h>
-#include <assert.h>
-#include <alloca.h>
-#define COMPUTERDIVISION_H_INCLUDED
-#endif // COMPUTERDIVISION_H_INCLUDED

lib/div.c

-#include <stdlib.h>
+#include "div.h"
 #include <stdint.h>
-#include <stdio.h>
-#include <assert.h>
-#include <alloca.h>
-#include "int.h"
-
-#include "int32.h"
-
-#include "uint64gmp.h"
-
-#include "power.h"
-
-#include "c.h"
-
-#include "array.h"
-
-#include "map.h"
-
-#include "types.h"
-
-#include "compare.h"
-
-#include "utilold.h"
-
-#include "addold.h"
-
-#include "subold.h"
-
-#include "logicalutil.h"
-
-#include "logicalold.h"
-
-#include "euclideandivision.h"
-
-#include "minmax.h"
-
-#include "mul.h"
 
 uint64_t invert_limb(uint64_t d) {
-  return div64_2by1((0xffffffffffffffffUL), (0xffffffffffffffffUL) - d, d);
+  return div64_2by1(0xffffffffffffffffUL, 0xffffffffffffffffUL - d, d);
 }
+struct __div2by1_inv_result;
 
-struct __div2by1_inv_result
-{ uint64_t __field_0;
-  uint64_t __field_1;
-};
 
 struct __div2by1_inv_result div2by1_inv(uint64_t uh, uint64_t ul, uint64_t d,
                                         uint64_t v) {
@@ -124,12 +85,8 @@ uint64_t wmpn_divrem_1(uint64_t * q, uint64_t * x, int32_t sz, uint64_t y) {
     return r;
   }
 }
+struct __div3by2_inv_result;
 
-struct __div3by2_inv_result
-{ uint64_t __field_0;
-  uint64_t __field_1;
-  uint64_t __field_2;
-};
 
 struct __div3by2_inv_result div3by2_inv(uint64_t uh, uint64_t um,
                                         uint64_t ul, uint64_t dh,
@@ -141,7 +98,7 @@ struct __div3by2_inv_result div3by2_inv(uint64_t uh, uint64_t um,
   uint64_t sh, p, tl, th, il, b;
   struct __mul64_double_result struct_res3;
   struct __sub64_with_borrow_result struct_res4, struct_res5, struct_res6,
-                                  struct_res7;
+                                    struct_res7;
   uint64_t ih, bl, b2, bh, rl, c1, rh, bl1, b1;
   struct __add64_with_carry_result struct_res8, struct_res9;
   struct __sub64_with_borrow_result struct_res10, struct_res11;
@@ -272,7 +229,7 @@ uint64_t div_sb_qr(uint64_t * q, uint64_t * x, int32_t sx, uint64_t * y,
     xd1 = xp + mdn;
     nx0 = (xp)[1];
     if (__builtin_expect(x1 == dh && nx0 == dl,0)) {
-      ql = (0xffffffffffffffffUL);
+      ql = 0xffffffffffffffffUL;
       wmpn_submul_1(xd1, y, sy, ql);
       x1 = (xp)[1];
       qp = qp + -1;
@@ -508,4 +465,3 @@ void wmpn_tdiv_qr_in_place(uint64_t * q, int32_t qxn, uint64_t * x,
   free(ny);
   return;
 }
-

lib/div.h

 #ifndef DIV_H_INCLUDED
 
-#include <stdlib.h>
+#include "uint64gmp.h"
+#include "c.h"
+#include "compare.h"
+#include "utilold.h"
+#include "addold.h"
+#include "subold.h"
+#include "logicalutil.h"
+#include "logicalold.h"
+#include "mul.h"
 #include <stdint.h>
-#include <stdio.h>
-#include <assert.h>
-#include <alloca.h>
+
 uint64_t invert_limb(uint64_t d);
 
-struct __div2by1_inv_result
-{ uint64_t __field_0;
+struct __div2by1_inv_result {
+  uint64_t __field_0;
   uint64_t __field_1;
 };
 
@@ -17,8 +23,8 @@ struct __div2by1_inv_result div2by1_inv(uint64_t uh, uint64_t ul, uint64_t d,
 
 uint64_t wmpn_divrem_1(uint64_t * q, uint64_t * x, int32_t sz, uint64_t y);
 
-struct __div3by2_inv_result
-{ uint64_t __field_0;
+struct __div3by2_inv_result {
+  uint64_t __field_0;
   uint64_t __field_1;
   uint64_t __field_2;
 };