From e558c031867cd1eda528e5075fb208f20adaef8f Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Thu, 16 Jul 2020 10:14:07 +0200
Subject: [PATCH] Update Why3 and refresh generated files.
---
lib/add.c | 79 -----------------------
lib/add.h | 12 ----
lib/alias.h | 6 +-
lib/sqrt.c | 12 ++--
lib/sub.c | 90 --------------------------
lib/sub.h | 12 ----
lib/uint64gmp.h | 14 ++--
lib/util.c | 4 +-
lib/zadd.c | 167 ++++++++++++++++++++++++++++++++++++++++++------
lib/zsub.c | 165 ++++++++++++++++++++++++++++++++++++++++++-----
why3 | 2 +-
11 files changed, 317 insertions(+), 246 deletions(-)
diff --git a/lib/add.c b/lib/add.c
index ee4fce8..caa0289 100644
--- a/lib/add.c
+++ b/lib/add.c
@@ -51,82 +51,3 @@ uint64_t wmpn_add(uint64_t * r, uint64_t * x, int32_t sx, uint64_t * y,
}
return c;
}
-
-uint64_t add_n(uint64_t * r, uint64_t * x, uint64_t * y, int32_t sz) {
- uint64_t * nr;
- uint64_t * nx;
- uint64_t * ny;
- struct __open_sep_result struct_res;
- uint64_t res;
- struct_res = open_sep(r, x, sz, y, sz);
- nr = struct_res.__field_0;
- nx = struct_res.__field_1;
- ny = struct_res.__field_2;
- res = wmpn_add_n(nr, nx, ny, sz);
- IGNORE3(r,x,y);
- return res;
-}
-
-uint64_t add_n_rx(uint64_t * x, uint64_t * y, int32_t sz) {
- uint64_t * nr;
- uint64_t * nx;
- uint64_t * ny;
- struct __open_rx_result struct_res;
- uint64_t res;
- struct_res = open_rx(x, sz, y, sz);
- nr = struct_res.__field_0;
- nx = struct_res.__field_1;
- ny = struct_res.__field_2;
- res = wmpn_add_n(nr, nx, ny, sz);
- IGNORE3(x,sz,sz);
- return res;
-}
-
-uint64_t add(uint64_t * r, uint64_t * x, int32_t sx, uint64_t * y, int32_t sy) {
- uint64_t * nr;
- uint64_t * nx;
- uint64_t * ny;
- struct __open_sep_result struct_res;
- uint64_t res;
- struct_res = open_sep(r, x, sx, y, sy);
- nr = struct_res.__field_0;
- nx = struct_res.__field_1;
- ny = struct_res.__field_2;
- res = wmpn_add(nr, nx, sx, ny, sy);
- IGNORE3(r,x,y);
- return res;
-}
-
-uint64_t add_rx(uint64_t * x, int32_t sx, uint64_t * y, int32_t sy) {
- uint64_t * nr;
- uint64_t * nx;
- uint64_t * ny;
- struct __open_rx_result struct_res;
- uint64_t res;
- struct_res = open_rx(x, sx, y, sy);
- nr = struct_res.__field_0;
- nx = struct_res.__field_1;
- ny = struct_res.__field_2;
- res = wmpn_add(nr, nx, sx, ny, sy);
- IGNORE3(x,sx,sy);
- return res;
-}
-
-uint64_t add_ry(uint64_t * x, int32_t sx, uint64_t * y, int32_t sy) {
- uint64_t * nr;
- uint64_t * ny;
- uint64_t * nx;
- struct __open_rx_result struct_res;
- uint64_t res;
- struct_res = open_rx(y, sx, x, sx);
- nr = struct_res.__field_0;
- ny = struct_res.__field_1;
- nx = struct_res.__field_2;
- res = wmpn_add(nr, nx, sx, ny, sy);
- IGNORE3(y,sx,sx);
- return res;
-}
-
-uint64_t add_n_rxy(uint64_t * x, int32_t sx) {
- return wmpn_add_n(x, x, x, sx);
-}
diff --git a/lib/add.h b/lib/add.h
index 55e521a..c4061ed 100644
--- a/lib/add.h
+++ b/lib/add.h
@@ -10,17 +10,5 @@ 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,
int32_t sy);
-uint64_t add_n(uint64_t * r, uint64_t * x, uint64_t * y, int32_t sz);
-
-uint64_t add_n_rx(uint64_t * x, uint64_t * y, int32_t sz);
-
-uint64_t add(uint64_t * r, uint64_t * x, int32_t sx, uint64_t * y, int32_t sy);
-
-uint64_t add_rx(uint64_t * x, int32_t sx, uint64_t * y, int32_t sy);
-
-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);
-
#define ADD_H_INCLUDED
#endif // ADD_H_INCLUDED
diff --git a/lib/alias.h b/lib/alias.h
index 351cea8..a5b6611 100644
--- a/lib/alias.h
+++ b/lib/alias.h
@@ -22,7 +22,7 @@ struct __open_shift_sep_result {
};
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, uint64_t *y)
{
struct __open_sep_result result;
result.__field_0 = r;
@@ -32,7 +32,7 @@ open_sep (uint64_t *r, uint64_t *x, int32_t sx, uint64_t *y, int32_t sy)
}
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, uint64_t *y)
{
struct __open_rx_result result;
result.__field_0 = x;
@@ -42,7 +42,7 @@ open_rx (uint64_t *x, int32_t sx, uint64_t *y, int32_t sy)
}
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)
{
struct __open_shift_sep_result result;
result.__field_0 = r;
diff --git a/lib/sqrt.c b/lib/sqrt.c
index 4dd5b76..e45ffbd 100644
--- a/lib/sqrt.c
+++ b/lib/sqrt.c
@@ -88,11 +88,11 @@ uint64_t wmpn_dc_sqrtrem(uint64_t * sp, uint64_t * np, int32_t n,
q = q + sl;
sh = *scratch;
c = (int64_t)(sh % UINT64_C(2));
- struct_res = open_shift_sep(sp, scratch, l);
+ struct_res = open_shift_sep(sp, scratch);
nr = struct_res.__field_0;
nx = struct_res.__field_1;
res = wmpn_rshift(nr, nx, l, UINT64_C(1));
- IGNORE2(sp,scratch);
+ IGNORE2(sp, scratch);
res;
st = sp[l - 1];
ql = q << (64 - UINT64_C(1));
@@ -194,11 +194,11 @@ int32_t wmpn_sqrtrem(uint64_t * sp, uint64_t * rp, uint64_t * np, int32_t n) {
*tp = UINT64_C(0);
tpa = tp + adj;
if (!(c == UINT64_C(0))) {
- struct_res = open_shift_sep(tpa, np, n);
+ struct_res = open_shift_sep(tpa, np);
nr = struct_res.__field_0;
nx = struct_res.__field_1;
res1 = wmpn_lshift(nr, nx, n, UINT64_C(2) * c);
- IGNORE2(tpa,np);
+ IGNORE2(tpa, np);
res1;
} else {
wmpn_copyi1(tpa, np, n);
@@ -232,11 +232,11 @@ int32_t wmpn_sqrtrem(uint64_t * sp, uint64_t * rp, uint64_t * np, int32_t n) {
}
if (!(c2 == UINT64_C(0))) {
o4 = tp;
- struct_res1 = open_shift_sep(rp, o4, tn);
+ struct_res1 = open_shift_sep(rp, o4);
nr1 = struct_res1.__field_0;
nx1 = struct_res1.__field_1;
res2 = wmpn_rshift(nr1, nx1, tn, c2);
- IGNORE2(rp,o4);
+ IGNORE2(rp, o4);
res2;
} else {
wmpn_copyi1(rp, tp, tn);
diff --git a/lib/sub.c b/lib/sub.c
index 0851fa4..2b8291d 100644
--- a/lib/sub.c
+++ b/lib/sub.c
@@ -51,93 +51,3 @@ uint64_t wmpn_sub(uint64_t * r, uint64_t * x, int32_t sx, uint64_t * y,
}
return b;
}
-
-uint64_t sub_n(uint64_t * r, uint64_t * x, uint64_t * y, int32_t sz) {
- uint64_t * nr;
- uint64_t * nx;
- uint64_t * ny;
- struct __open_sep_result struct_res;
- uint64_t res;
- struct_res = open_sep(r, x, sz, y, sz);
- nr = struct_res.__field_0;
- nx = struct_res.__field_1;
- ny = struct_res.__field_2;
- res = wmpn_sub_n(nr, nx, ny, sz);
- IGNORE3(r,x,y);
- return res;
-}
-
-uint64_t sub_n_rx(uint64_t * x, uint64_t * y, int32_t sz) {
- uint64_t * nr;
- uint64_t * nx;
- uint64_t * ny;
- struct __open_rx_result struct_res;
- uint64_t res;
- struct_res = open_rx(x, sz, y, sz);
- nr = struct_res.__field_0;
- nx = struct_res.__field_1;
- ny = struct_res.__field_2;
- res = wmpn_sub_n(nr, nx, ny, sz);
- IGNORE3(x,sz,sz);
- return res;
-}
-
-uint64_t sub_n_ry(uint64_t * x, uint64_t * y, int32_t sz) {
- uint64_t * nr;
- uint64_t * ny;
- uint64_t * nx;
- struct __open_rx_result struct_res;
- uint64_t res;
- struct_res = open_rx(y, sz, x, sz);
- nr = struct_res.__field_0;
- ny = struct_res.__field_1;
- nx = struct_res.__field_2;
- res = wmpn_sub_n(nr, nx, ny, sz);
- IGNORE3(y,sz,sz);
- return res;
-}
-
-uint64_t sub(uint64_t * r, uint64_t * x, int32_t sx, uint64_t * y, int32_t sy) {
- uint64_t * nr;
- uint64_t * nx;
- uint64_t * ny;
- struct __open_sep_result struct_res;
- uint64_t res;
- struct_res = open_sep(r, x, sx, y, sy);
- nr = struct_res.__field_0;
- nx = struct_res.__field_1;
- ny = struct_res.__field_2;
- res = wmpn_sub(nr, nx, sx, ny, sy);
- IGNORE3(r,x,y);
- return res;
-}
-
-uint64_t sub_rx(uint64_t * x, int32_t sx, uint64_t * y, int32_t sy) {
- uint64_t * nr;
- uint64_t * nx;
- uint64_t * ny;
- struct __open_rx_result struct_res;
- uint64_t res;
- struct_res = open_rx(x, sx, y, sy);
- nr = struct_res.__field_0;
- nx = struct_res.__field_1;
- ny = struct_res.__field_2;
- res = wmpn_sub(nr, nx, sx, ny, sy);
- IGNORE3(x,sx,sy);
- return res;
-}
-
-uint64_t sub_ry(uint64_t * x, int32_t sx, uint64_t * y, int32_t sy) {
- uint64_t * nr;
- uint64_t * ny;
- uint64_t * nx;
- struct __open_rx_result struct_res;
- uint64_t res;
- struct_res = open_rx(y, sx, x, sx);
- nr = struct_res.__field_0;
- ny = struct_res.__field_1;
- nx = struct_res.__field_2;
- res = wmpn_sub(nr, nx, sx, ny, sy);
- IGNORE3(y,sx,sx);
- return res;
-}
diff --git a/lib/sub.h b/lib/sub.h
index 86eed71..3371f2c 100644
--- a/lib/sub.h
+++ b/lib/sub.h
@@ -10,17 +10,5 @@ uint64_t wmpn_sub_n(uint64_t * r, uint64_t * x, uint64_t * y, int32_t sz);
uint64_t wmpn_sub(uint64_t * r, uint64_t * x, int32_t sx, uint64_t * y,
int32_t sy);
-uint64_t sub_n(uint64_t * r, uint64_t * x, uint64_t * y, int32_t sz);
-
-uint64_t sub_n_rx(uint64_t * x, uint64_t * y, int32_t sz);
-
-uint64_t sub_n_ry(uint64_t * x, uint64_t * y, int32_t sz);
-
-uint64_t sub(uint64_t * r, uint64_t * x, int32_t sx, uint64_t * y, int32_t sy);
-
-uint64_t sub_rx(uint64_t * x, int32_t sx, uint64_t * y, int32_t sy);
-
-uint64_t sub_ry(uint64_t * x, int32_t sx, uint64_t * y, int32_t sy);
-
#define SUB_H_INCLUDED
#endif // SUB_H_INCLUDED
diff --git a/lib/uint64gmp.h b/lib/uint64gmp.h
index 58f3b33..1a4572a 100644
--- a/lib/uint64gmp.h
+++ b/lib/uint64gmp.h
@@ -4,19 +4,21 @@
typedef unsigned __int128 uint128_t;
-struct __mul64_double_result
-{ uint64_t __field_0;
+struct __mul64_double_result {
+ uint64_t __field_0;
uint64_t __field_1;
};
-static inline struct __mul64_double_result mul64_double(uint64_t x, uint64_t y)
+static inline struct __mul64_double_result
+mul64_double(uint64_t x, uint64_t y)
{
uint128_t z = (uint128_t)x * (uint128_t)y;
struct __mul64_double_result result = { z, z >> 64 };
return result;
}
-static inline uint64_t div64_2by1(uint64_t ul, uint64_t uh, uint64_t d)
+static inline uint64_t
+div64_2by1(uint64_t ul, uint64_t uh, uint64_t d)
{
return (((uint128_t)uh << 64) | ul) / d;
}
@@ -73,8 +75,8 @@ add64_3(uint64_t x, uint64_t y, uint64_t z)
return result;
}
-struct __lsld64_result
-{ uint64_t __field_0;
+struct __lsld64_result {
+ uint64_t __field_0;
uint64_t __field_1;
};
diff --git a/lib/util.c b/lib/util.c
index d7d7784..8c4c2fe 100644
--- a/lib/util.c
+++ b/lib/util.c
@@ -52,11 +52,11 @@ void wmpn_copyd_sep(uint64_t * rp, uint64_t * up, int32_t n) {
uint64_t * nr;
uint64_t * nx;
struct __open_shift_sep_result struct_res;
- struct_res = open_shift_sep(rp, up, n);
+ struct_res = open_shift_sep(rp, up);
nr = struct_res.__field_0;
nx = struct_res.__field_1;
wmpn_copyd(nr, nx, n);
- IGNORE2(rp,up);
+ IGNORE2(rp, up);
return;
}
diff --git a/lib/zadd.c b/lib/zadd.c
index d167518..7139963 100644
--- a/lib/zadd.c
+++ b/lib/zadd.c
@@ -8,24 +8,83 @@ void wmpz_add(wmpz_ptr w, wmpz_ptr u, wmpz_ptr v) {
int uw, vw;
uint64_t * wp;
uint64_t * vp;
- uint64_t usb, usb1;
+ uint64_t usb;
+ uint64_t * nr;
+ uint64_t * nx;
+ uint64_t * ny;
+ struct __open_rx_result struct_res;
+ uint64_t res, usb1;
uint64_t * up;
+ uint64_t * nr1;
+ uint64_t * ny1;
+ uint64_t * nx1;
+ struct __open_rx_result struct_res1;
+ uint64_t res1;
uint64_t * up1;
uint64_t * vp1;
- uint64_t usb2, usb3, usb4;
+ uint64_t usb2;
+ uint64_t * nr2;
+ uint64_t * nx2;
+ uint64_t * ny2;
+ struct __open_sep_result struct_res2;
+ uint64_t res2, usb3;
uint64_t * vp2;
+ uint64_t * nr3;
+ uint64_t * ny3;
+ uint64_t * nx3;
+ struct __open_rx_result struct_res3;
+ uint64_t res3, usb4;
+ uint64_t * nr4;
+ uint64_t * nx4;
+ uint64_t * ny4;
+ struct __open_rx_result struct_res4;
+ uint64_t res4, usb5;
uint64_t * up2;
- uint64_t usb5, usb6;
+ uint64_t * nr5;
+ uint64_t * nx5;
+ uint64_t * ny5;
+ struct __open_rx_result struct_res5;
+ uint64_t res5, usb6;
+ uint64_t * nr6;
+ uint64_t * ny6;
+ uint64_t * nx6;
+ struct __open_rx_result struct_res6;
+ uint64_t res6;
uint64_t * up3;
uint64_t * vp3;
- uint64_t usb7, usb8, o;
+ uint64_t usb7;
+ uint64_t * nr7;
+ uint64_t * nx7;
+ uint64_t * ny7;
+ struct __open_sep_result struct_res7;
+ uint64_t res7, usb8;
+ uint64_t * nr8;
+ uint64_t * nx8;
+ uint64_t * ny8;
+ struct __open_sep_result struct_res8;
+ uint64_t res8, o;
uint64_t cy;
uint64_t * vp4;
- uint64_t o1, o2;
+ uint64_t o1;
+ uint64_t * nr9;
+ uint64_t * nx9;
+ uint64_t * ny9;
+ struct __open_rx_result struct_res9;
+ uint64_t res9, o2;
uint64_t * up4;
+ uint64_t * nr10;
+ uint64_t * ny10;
+ uint64_t * nx10;
+ struct __open_rx_result struct_res10;
+ uint64_t res10;
uint64_t * up5;
uint64_t * vp5;
uint64_t o3;
+ uint64_t * nr11;
+ uint64_t * nx11;
+ uint64_t * ny11;
+ struct __open_sep_result struct_res11;
+ uint64_t res11;
u1 = u;
v1 = v;
usize = SIZ(u1);
@@ -51,17 +110,35 @@ void wmpz_add(wmpz_ptr w, wmpz_ptr u, wmpz_ptr v) {
if (!(abs_usize == abs_vsize)) {
if (uw) {
vp = PTR(v1);
- usb = sub_rx(wp, abs_usize, vp, abs_vsize);
+ struct_res = open_rx(wp, vp);
+ nr = struct_res.__field_0;
+ nx = struct_res.__field_1;
+ ny = struct_res.__field_2;
+ res = wmpn_sub(nr, nx, abs_usize, ny, abs_vsize);
+ IGNORE2(wp, vp);
+ usb = res;
(void)(v1);
} else {
if (vw) {
up = PTR(u1);
- usb1 = sub_ry(up, abs_usize, wp, abs_vsize);
+ struct_res1 = open_rx(wp, up);
+ nr1 = struct_res1.__field_0;
+ ny1 = struct_res1.__field_1;
+ nx1 = struct_res1.__field_2;
+ res1 = wmpn_sub(nr1, nx1, abs_usize, ny1, abs_vsize);
+ IGNORE2(wp, up);
+ usb1 = res1;
(void)(u1);
} else {
up1 = PTR(u1);
vp1 = PTR(v1);
- usb2 = sub(wp, up1, abs_usize, vp1, abs_vsize);
+ struct_res2 = open_sep(wp, up1, vp1);
+ nr2 = struct_res2.__field_0;
+ nx2 = struct_res2.__field_1;
+ ny2 = struct_res2.__field_2;
+ res2 = wmpn_sub(nr2, nx2, abs_usize, ny2, abs_vsize);
+ IGNORE3(wp, up1, vp1);
+ usb2 = res2;
(void)(u1);
(void)(v1);
}
@@ -76,13 +153,25 @@ void wmpz_add(wmpz_ptr w, wmpz_ptr u, wmpz_ptr v) {
if (uw) {
vp2 = PTR(v1);
if (wmpn_cmp(wp, vp2, abs_usize) < 0) {
- usb3 = sub_n_ry(vp2, wp, abs_usize);
+ struct_res3 = open_rx(wp, vp2);
+ nr3 = struct_res3.__field_0;
+ ny3 = struct_res3.__field_1;
+ nx3 = struct_res3.__field_2;
+ res3 = wmpn_sub_n(nr3, nx3, ny3, abs_usize);
+ IGNORE2(wp, vp2);
+ usb3 = res3;
normalize(wp, &wsize);
if (usize >= 0) {
wsize = -wsize;
}
} else {
- usb4 = sub_n_rx(wp, vp2, abs_usize);
+ struct_res4 = open_rx(wp, vp2);
+ nr4 = struct_res4.__field_0;
+ nx4 = struct_res4.__field_1;
+ ny4 = struct_res4.__field_2;
+ res4 = wmpn_sub_n(nr4, nx4, ny4, abs_usize);
+ IGNORE2(wp, vp2);
+ usb4 = res4;
normalize(wp, &wsize);
if (usize < 0) {
wsize = -wsize;
@@ -93,13 +182,25 @@ void wmpz_add(wmpz_ptr w, wmpz_ptr u, wmpz_ptr v) {
if (vw) {
up2 = PTR(u1);
if (wmpn_cmp(up2, wp, abs_usize) < 0) {
- usb5 = sub_n_rx(wp, up2, abs_usize);
+ struct_res5 = open_rx(wp, up2);
+ nr5 = struct_res5.__field_0;
+ nx5 = struct_res5.__field_1;
+ ny5 = struct_res5.__field_2;
+ res5 = wmpn_sub_n(nr5, nx5, ny5, abs_usize);
+ IGNORE2(wp, up2);
+ usb5 = res5;
normalize(wp, &wsize);
if (usize >= 0) {
wsize = -wsize;
}
} else {
- usb6 = sub_n_ry(up2, wp, abs_usize);
+ struct_res6 = open_rx(wp, up2);
+ nr6 = struct_res6.__field_0;
+ ny6 = struct_res6.__field_1;
+ nx6 = struct_res6.__field_2;
+ res6 = wmpn_sub_n(nr6, nx6, ny6, abs_usize);
+ IGNORE2(wp, up2);
+ usb6 = res6;
normalize(wp, &wsize);
if (usize < 0) {
wsize = -wsize;
@@ -110,13 +211,25 @@ void wmpz_add(wmpz_ptr w, wmpz_ptr u, wmpz_ptr v) {
up3 = PTR(u1);
vp3 = PTR(v1);
if (wmpn_cmp(up3, vp3, abs_usize) < 0) {
- usb7 = sub_n(wp, vp3, up3, abs_usize);
+ struct_res7 = open_sep(wp, vp3, up3);
+ nr7 = struct_res7.__field_0;
+ nx7 = struct_res7.__field_1;
+ ny7 = struct_res7.__field_2;
+ res7 = wmpn_sub_n(nr7, nx7, ny7, abs_usize);
+ IGNORE3(wp, vp3, up3);
+ usb7 = res7;
normalize(wp, &wsize);
if (usize >= 0) {
wsize = -wsize;
}
} else {
- usb8 = sub_n(wp, up3, vp3, abs_usize);
+ struct_res8 = open_sep(wp, up3, vp3);
+ nr8 = struct_res8.__field_0;
+ nx8 = struct_res8.__field_1;
+ ny8 = struct_res8.__field_2;
+ res8 = wmpn_sub_n(nr8, nx8, ny8, abs_usize);
+ IGNORE3(wp, up3, vp3);
+ usb8 = res8;
normalize(wp, &wsize);
if (usize < 0) {
wsize = -wsize;
@@ -131,24 +244,42 @@ void wmpz_add(wmpz_ptr w, wmpz_ptr u, wmpz_ptr v) {
cy = UINT64_C(0);
if (uw) {
if (vw) {
- o = add_n_rxy(wp, abs_vsize);
+ o = wmpn_add_n(wp, wp, wp, abs_vsize);
cy = o;
} else {
vp4 = PTR(v1);
- o1 = add_rx(wp, abs_usize, vp4, abs_vsize);
+ struct_res9 = open_rx(wp, vp4);
+ nr9 = struct_res9.__field_0;
+ nx9 = struct_res9.__field_1;
+ ny9 = struct_res9.__field_2;
+ res9 = wmpn_add(nr9, nx9, abs_usize, ny9, abs_vsize);
+ IGNORE2(wp, vp4);
+ o1 = res9;
cy = o1;
(void)(v1);
}
} else {
if (vw) {
up4 = PTR(u1);
- o2 = add_ry(up4, abs_usize, wp, abs_vsize);
+ struct_res10 = open_rx(wp, up4);
+ nr10 = struct_res10.__field_0;
+ ny10 = struct_res10.__field_1;
+ nx10 = struct_res10.__field_2;
+ res10 = wmpn_add(nr10, nx10, abs_usize, ny10, abs_vsize);
+ IGNORE2(wp, up4);
+ o2 = res10;
cy = o2;
(void)(u1);
} else {
up5 = PTR(u1);
vp5 = PTR(v1);
- o3 = add(wp, up5, abs_usize, vp5, abs_vsize);
+ struct_res11 = open_sep(wp, up5, vp5);
+ nr11 = struct_res11.__field_0;
+ nx11 = struct_res11.__field_1;
+ ny11 = struct_res11.__field_2;
+ res11 = wmpn_add(nr11, nx11, abs_usize, ny11, abs_vsize);
+ IGNORE3(wp, up5, vp5);
+ o3 = res11;
cy = o3;
(void)(u1);
(void)(v1);
diff --git a/lib/zsub.c b/lib/zsub.c
index dc3e96e..2328dd7 100644
--- a/lib/zsub.c
+++ b/lib/zsub.c
@@ -8,24 +8,83 @@ void wmpz_sub(wmpz_ptr w, wmpz_ptr u, wmpz_ptr v) {
int uw, vw;
uint64_t * wp;
uint64_t * vp;
- uint64_t usb, usb1;
+ uint64_t usb;
+ uint64_t * nr;
+ uint64_t * nx;
+ uint64_t * ny;
+ struct __open_rx_result struct_res;
+ uint64_t res, usb1;
uint64_t * up;
+ uint64_t * nr1;
+ uint64_t * ny1;
+ uint64_t * nx1;
+ struct __open_rx_result struct_res1;
+ uint64_t res1;
uint64_t * up1;
uint64_t * vp1;
- uint64_t usb2, usb3, usb4;
+ uint64_t usb2;
+ uint64_t * nr2;
+ uint64_t * nx2;
+ uint64_t * ny2;
+ struct __open_sep_result struct_res2;
+ uint64_t res2, usb3;
uint64_t * vp2;
+ uint64_t * nr3;
+ uint64_t * ny3;
+ uint64_t * nx3;
+ struct __open_rx_result struct_res3;
+ uint64_t res3, usb4;
+ uint64_t * nr4;
+ uint64_t * nx4;
+ uint64_t * ny4;
+ struct __open_rx_result struct_res4;
+ uint64_t res4, usb5;
uint64_t * up2;
- uint64_t usb5, usb6;
+ uint64_t * nr5;
+ uint64_t * nx5;
+ uint64_t * ny5;
+ struct __open_rx_result struct_res5;
+ uint64_t res5, usb6;
+ uint64_t * nr6;
+ uint64_t * ny6;
+ uint64_t * nx6;
+ struct __open_rx_result struct_res6;
+ uint64_t res6;
uint64_t * up3;
uint64_t * vp3;
- uint64_t usb7, usb8;
+ uint64_t usb7;
+ uint64_t * nr7;
+ uint64_t * nx7;
+ uint64_t * ny7;
+ struct __open_sep_result struct_res7;
+ uint64_t res7, usb8;
+ uint64_t * nr8;
+ uint64_t * nx8;
+ uint64_t * ny8;
+ struct __open_sep_result struct_res8;
+ uint64_t res8;
uint64_t cy;
uint64_t * vp4;
- uint64_t o, o1;
+ uint64_t o;
+ uint64_t * nr9;
+ uint64_t * nx9;
+ uint64_t * ny9;
+ struct __open_rx_result struct_res9;
+ uint64_t res9, o1;
uint64_t * up4;
+ uint64_t * nr10;
+ uint64_t * ny10;
+ uint64_t * nx10;
+ struct __open_rx_result struct_res10;
+ uint64_t res10;
uint64_t * up5;
uint64_t * vp5;
uint64_t o2;
+ uint64_t * nr11;
+ uint64_t * nx11;
+ uint64_t * ny11;
+ struct __open_sep_result struct_res11;
+ uint64_t res11;
u1 = u;
v1 = v;
if (u1 == v1) {
@@ -55,17 +114,35 @@ void wmpz_sub(wmpz_ptr w, wmpz_ptr u, wmpz_ptr v) {
if (!(abs_usize == abs_vsize)) {
if (uw) {
vp = PTR(v1);
- usb = sub_rx(wp, abs_usize, vp, abs_vsize);
+ struct_res = open_rx(wp, vp);
+ nr = struct_res.__field_0;
+ nx = struct_res.__field_1;
+ ny = struct_res.__field_2;
+ res = wmpn_sub(nr, nx, abs_usize, ny, abs_vsize);
+ IGNORE2(wp, vp);
+ usb = res;
(void)(v1);
} else {
if (vw) {
up = PTR(u1);
- usb1 = sub_ry(up, abs_usize, wp, abs_vsize);
+ struct_res1 = open_rx(wp, up);
+ nr1 = struct_res1.__field_0;
+ ny1 = struct_res1.__field_1;
+ nx1 = struct_res1.__field_2;
+ res1 = wmpn_sub(nr1, nx1, abs_usize, ny1, abs_vsize);
+ IGNORE2(wp, up);
+ usb1 = res1;
(void)(u1);
} else {
up1 = PTR(u1);
vp1 = PTR(v1);
- usb2 = sub(wp, up1, abs_usize, vp1, abs_vsize);
+ struct_res2 = open_sep(wp, up1, vp1);
+ nr2 = struct_res2.__field_0;
+ nx2 = struct_res2.__field_1;
+ ny2 = struct_res2.__field_2;
+ res2 = wmpn_sub(nr2, nx2, abs_usize, ny2, abs_vsize);
+ IGNORE3(wp, up1, vp1);
+ usb2 = res2;
(void)(u1);
(void)(v1);
}
@@ -80,13 +157,25 @@ void wmpz_sub(wmpz_ptr w, wmpz_ptr u, wmpz_ptr v) {
if (uw) {
vp2 = PTR(v1);
if (wmpn_cmp(wp, vp2, abs_usize) < 0) {
- usb3 = sub_n_ry(vp2, wp, abs_usize);
+ struct_res3 = open_rx(wp, vp2);
+ nr3 = struct_res3.__field_0;
+ ny3 = struct_res3.__field_1;
+ nx3 = struct_res3.__field_2;
+ res3 = wmpn_sub_n(nr3, nx3, ny3, abs_usize);
+ IGNORE2(wp, vp2);
+ usb3 = res3;
normalize(wp, &wsize);
if (usize >= 0) {
wsize = -wsize;
}
} else {
- usb4 = sub_n_rx(wp, vp2, abs_usize);
+ struct_res4 = open_rx(wp, vp2);
+ nr4 = struct_res4.__field_0;
+ nx4 = struct_res4.__field_1;
+ ny4 = struct_res4.__field_2;
+ res4 = wmpn_sub_n(nr4, nx4, ny4, abs_usize);
+ IGNORE2(wp, vp2);
+ usb4 = res4;
normalize(wp, &wsize);
if (usize < 0) {
wsize = -wsize;
@@ -97,13 +186,25 @@ void wmpz_sub(wmpz_ptr w, wmpz_ptr u, wmpz_ptr v) {
if (vw) {
up2 = PTR(u1);
if (wmpn_cmp(up2, wp, abs_usize) < 0) {
- usb5 = sub_n_rx(wp, up2, abs_usize);
+ struct_res5 = open_rx(wp, up2);
+ nr5 = struct_res5.__field_0;
+ nx5 = struct_res5.__field_1;
+ ny5 = struct_res5.__field_2;
+ res5 = wmpn_sub_n(nr5, nx5, ny5, abs_usize);
+ IGNORE2(wp, up2);
+ usb5 = res5;
normalize(wp, &wsize);
if (usize >= 0) {
wsize = -wsize;
}
} else {
- usb6 = sub_n_ry(up2, wp, abs_usize);
+ struct_res6 = open_rx(wp, up2);
+ nr6 = struct_res6.__field_0;
+ ny6 = struct_res6.__field_1;
+ nx6 = struct_res6.__field_2;
+ res6 = wmpn_sub_n(nr6, nx6, ny6, abs_usize);
+ IGNORE2(wp, up2);
+ usb6 = res6;
normalize(wp, &wsize);
if (usize < 0) {
wsize = -wsize;
@@ -114,13 +215,25 @@ void wmpz_sub(wmpz_ptr w, wmpz_ptr u, wmpz_ptr v) {
up3 = PTR(u1);
vp3 = PTR(v1);
if (wmpn_cmp(up3, vp3, abs_usize) < 0) {
- usb7 = sub_n(wp, vp3, up3, abs_usize);
+ struct_res7 = open_sep(wp, vp3, up3);
+ nr7 = struct_res7.__field_0;
+ nx7 = struct_res7.__field_1;
+ ny7 = struct_res7.__field_2;
+ res7 = wmpn_sub_n(nr7, nx7, ny7, abs_usize);
+ IGNORE3(wp, vp3, up3);
+ usb7 = res7;
normalize(wp, &wsize);
if (usize >= 0) {
wsize = -wsize;
}
} else {
- usb8 = sub_n(wp, up3, vp3, abs_usize);
+ struct_res8 = open_sep(wp, up3, vp3);
+ nr8 = struct_res8.__field_0;
+ nx8 = struct_res8.__field_1;
+ ny8 = struct_res8.__field_2;
+ res8 = wmpn_sub_n(nr8, nx8, ny8, abs_usize);
+ IGNORE3(wp, up3, vp3);
+ usb8 = res8;
normalize(wp, &wsize);
if (usize < 0) {
wsize = -wsize;
@@ -135,19 +248,37 @@ void wmpz_sub(wmpz_ptr w, wmpz_ptr u, wmpz_ptr v) {
cy = UINT64_C(0);
if (uw) {
vp4 = PTR(v1);
- o = add_rx(wp, abs_usize, vp4, abs_vsize);
+ struct_res9 = open_rx(wp, vp4);
+ nr9 = struct_res9.__field_0;
+ nx9 = struct_res9.__field_1;
+ ny9 = struct_res9.__field_2;
+ res9 = wmpn_add(nr9, nx9, abs_usize, ny9, abs_vsize);
+ IGNORE2(wp, vp4);
+ o = res9;
cy = o;
(void)(v1);
} else {
if (vw) {
up4 = PTR(u1);
- o1 = add_ry(up4, abs_usize, wp, abs_vsize);
+ struct_res10 = open_rx(wp, up4);
+ nr10 = struct_res10.__field_0;
+ ny10 = struct_res10.__field_1;
+ nx10 = struct_res10.__field_2;
+ res10 = wmpn_add(nr10, nx10, abs_usize, ny10, abs_vsize);
+ IGNORE2(wp, up4);
+ o1 = res10;
cy = o1;
(void)(u1);
} else {
up5 = PTR(u1);
vp5 = PTR(v1);
- o2 = add(wp, up5, abs_usize, vp5, abs_vsize);
+ struct_res11 = open_sep(wp, up5, vp5);
+ nr11 = struct_res11.__field_0;
+ nx11 = struct_res11.__field_1;
+ ny11 = struct_res11.__field_2;
+ res11 = wmpn_add(nr11, nx11, abs_usize, ny11, abs_vsize);
+ IGNORE3(wp, up5, vp5);
+ o2 = res11;
cy = o2;
(void)(u1);
(void)(v1);
diff --git a/why3 b/why3
index 226ba5b..2a35b57 160000
--- a/why3
+++ b/why3
@@ -1 +1 @@
-Subproject commit 226ba5b0f0777654d637b1b88006ab54c46a31a2
+Subproject commit 2a35b574eba191bed7953b6d9fc6ffb4c417ab0b
--
GitLab