From c26e1a29592bc9dbebb2a14ddc8ef936c6283df6 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 10 Jun 2020 12:29:44 +0200
Subject: [PATCH] [e-acsl] fix soundness bug when initializing rationals from
integers
---
.../e-acsl/share/e-acsl/e_acsl_gmp_api.h | 9 +-
src/plugins/e-acsl/src/code_generator/gmp.ml | 19 +-
src/plugins/e-acsl/src/code_generator/gmp.mli | 2 +-
.../tests/arith/oracle_ci/gen_functions.c | 90 +++++-----
.../tests/arith/oracle_ci/gen_functions_rec.c | 164 +++++++++---------
.../tests/arith/oracle_ci/gen_rationals.c | 42 ++++-
.../arith/oracle_ci/rationals.res.oracle | 2 +
src/plugins/e-acsl/tests/arith/rationals.c | 3 +
.../e-acsl/tests/bts/oracle_ci/gen_bts1307.c | 4 +-
.../tests/gmp-only/oracle_ci/gen_functions.c | 152 ++++++++--------
10 files changed, 268 insertions(+), 219 deletions(-)
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h
index 829f7cf15b4..962a72dff8e 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h
@@ -145,8 +145,8 @@ extern void __gmpq_set_d(mpq_t q, double d)
__attribute__((FC_BUILTIN));
/*@ requires \valid(q);
- @ assigns *q \from n; */
-extern void __gmpq_set_si(mpq_t q, signed long int n)
+ @ assigns *q \from n,d; */
+extern void __gmpq_set_si(mpq_t q, signed long int n, unsigned long int d)
__attribute__((FC_BUILTIN));
/*@ allocates q;
@@ -158,9 +158,8 @@ extern int __gmpq_set_str(mpq_t q, const char *str, int base)
__attribute__((FC_BUILTIN));
/*@ requires \valid(z);
-// @ ensures z->n == n;
- @ assigns *z \from n; */
-extern void __gmpz_set_ui(mpz_t z, unsigned long int n)
+ @ assigns *z \from n,d; */
+extern void __gmpz_set_ui(mpz_t z, unsigned long int n, unsigned long int d)
__attribute__((FC_BUILTIN));
/*@ requires \valid(z);
diff --git a/src/plugins/e-acsl/src/code_generator/gmp.ml b/src/plugins/e-acsl/src/code_generator/gmp.ml
index dd373192bd1..89ea82b0bdf 100644
--- a/src/plugins/e-acsl/src/code_generator/gmp.ml
+++ b/src/plugins/e-acsl/src/code_generator/gmp.ml
@@ -40,18 +40,25 @@ let clear ~loc e = apply_on_var "clear" ~loc e
exception Longlong of ikind
-let get_set_suffix_and_arg e =
+let get_set_suffix_and_arg res_ty e =
let ty = Cil.typeOf e in
if Gmp_types.Z.is_t ty || Gmp_types.Q.is_t ty then "", [ e ]
else
+ let args_uisi e =
+ if Gmp_types.Z.is_t res_ty then [ e ]
+ else begin
+ assert (Gmp_types.Q.is_t res_ty);
+ [ e; Cil.one ~loc:e.eloc ]
+ end
+ in
match Cil.unrollType ty with
| TInt(IChar, _) ->
(if Cil.theMachine.Cil.theMachine.char_is_unsigned then "_ui"
else "_si"),
- [ e ]
+ args_uisi e
| TInt((IBool | IUChar | IUInt | IUShort | IULong), _) ->
- "_ui", [ e ]
- | TInt((ISChar | IShort | IInt | ILong), _) -> "_si", [ e ]
+ "_ui", args_uisi e
+ | TInt((ISChar | IShort | IInt | ILong), _) -> "_si", args_uisi e
| TInt((ILongLong | IULongLong as ikind), _) -> raise (Longlong ikind)
| TPtr(TInt(IChar, _), _) ->
"_str",
@@ -71,7 +78,7 @@ let get_set_suffix_and_arg e =
let generic_affect ~loc fname lv ev e =
let ty = Cil.typeOf ev in
if Gmp_types.Z.is_t ty || Gmp_types.Q.is_t ty then begin
- let suf, args = get_set_suffix_and_arg e in
+ let suf, args = get_set_suffix_and_arg ty e in
Constructor.mk_lib_call ~loc (fname ^ suf) (ev :: args)
end else
Cil.mkStmtOneInstr ~valid_sid:true (Set(lv, e, e.eloc))
@@ -122,6 +129,6 @@ let affect ~loc lv ev e =
(*
Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/code_generator/gmp.mli b/src/plugins/e-acsl/src/code_generator/gmp.mli
index d2b467d7fbc..db4811dbeca 100644
--- a/src/plugins/e-acsl/src/code_generator/gmp.mli
+++ b/src/plugins/e-acsl/src/code_generator/gmp.mli
@@ -42,6 +42,6 @@ val affect: loc:location -> lval -> exp -> exp -> stmt
(*
Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
index 8a80b252478..cfdc4b4830a 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
@@ -232,6 +232,51 @@ void __gen_e_acsl_k(int x)
return;
}
+double __gen_e_acsl_f2(double x)
+{
+ __e_acsl_mpq_t __gen_e_acsl__8;
+ __e_acsl_mpq_t __gen_e_acsl__9;
+ __e_acsl_mpq_t __gen_e_acsl_div;
+ double __gen_e_acsl__10;
+ __gmpq_init(__gen_e_acsl__8);
+ __gmpq_set_str(__gen_e_acsl__8,"1",10);
+ __gmpq_init(__gen_e_acsl__9);
+ __gmpq_set_d(__gen_e_acsl__9,x);
+ __gmpq_init(__gen_e_acsl_div);
+ __gmpq_div(__gen_e_acsl_div,(__e_acsl_mpq_struct const *)(__gen_e_acsl__8),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__9));
+ __gen_e_acsl__10 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl_div));
+ __gmpq_clear(__gen_e_acsl__8);
+ __gmpq_clear(__gen_e_acsl__9);
+ __gmpq_clear(__gen_e_acsl_div);
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__10); */
+ return __gen_e_acsl__10;
+}
+
+int __gen_e_acsl_g(int x)
+{
+ int __gen_e_acsl_g_hidden_2;
+ __gen_e_acsl_g_hidden_2 = __gen_e_acsl_g_hidden(x);
+ return __gen_e_acsl_g_hidden_2;
+}
+
+mystruct __gen_e_acsl_t1(mystruct m)
+{
+ return m;
+}
+
+int __gen_e_acsl_p1(int x, int y)
+{
+ int __retres = x + (long)y > 0L;
+ return __retres;
+}
+
+long __gen_e_acsl_t2(mystruct m)
+{
+ long __retres = m.k + (long)m.l;
+ return __retres;
+}
+
int __gen_e_acsl_p2(int x, int y)
{
int __retres = x + (long)y > 0L;
@@ -339,49 +384,4 @@ int __gen_e_acsl_g_hidden(int x)
return x;
}
-double __gen_e_acsl_f2(double x)
-{
- __e_acsl_mpq_t __gen_e_acsl__8;
- __e_acsl_mpq_t __gen_e_acsl__9;
- __e_acsl_mpq_t __gen_e_acsl_div;
- double __gen_e_acsl__10;
- __gmpq_init(__gen_e_acsl__8);
- __gmpq_set_str(__gen_e_acsl__8,"1",10);
- __gmpq_init(__gen_e_acsl__9);
- __gmpq_set_d(__gen_e_acsl__9,x);
- __gmpq_init(__gen_e_acsl_div);
- __gmpq_div(__gen_e_acsl_div,(__e_acsl_mpq_struct const *)(__gen_e_acsl__8),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__9));
- __gen_e_acsl__10 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl_div));
- __gmpq_clear(__gen_e_acsl__8);
- __gmpq_clear(__gen_e_acsl__9);
- __gmpq_clear(__gen_e_acsl_div);
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__10); */
- return __gen_e_acsl__10;
-}
-
-int __gen_e_acsl_g(int x)
-{
- int __gen_e_acsl_g_hidden_2;
- __gen_e_acsl_g_hidden_2 = __gen_e_acsl_g_hidden(x);
- return __gen_e_acsl_g_hidden_2;
-}
-
-mystruct __gen_e_acsl_t1(mystruct m)
-{
- return m;
-}
-
-int __gen_e_acsl_p1(int x, int y)
-{
- int __retres = x + (long)y > 0L;
- return __retres;
-}
-
-long __gen_e_acsl_t2(mystruct m)
-{
- long __retres = m.k + (long)m.l;
- return __retres;
-}
-
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
index d7e6ba9cda3..b9015c95933 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
@@ -105,88 +105,6 @@ int main(void)
return __retres;
}
-int __gen_e_acsl_g(int n)
-{
- int __retres = 0;
- return __retres;
-}
-
-int __gen_e_acsl_g_5(long n)
-{
- int __retres = 0;
- return __retres;
-}
-
-int __gen_e_acsl_f3(int n)
-{
- int __gen_e_acsl_if_6;
- if (n > 0) {
- int __gen_e_acsl_g_2;
- int __gen_e_acsl_f3_5;
- __gen_e_acsl_g_2 = __gen_e_acsl_g(n);
- __gen_e_acsl_f3_5 = __gen_e_acsl_f3_2(n - 1L);
- __gen_e_acsl_if_6 = __gen_e_acsl_g_2 * __gen_e_acsl_f3_5 - 5;
- }
- else {
- int __gen_e_acsl_g_8;
- __gen_e_acsl_g_8 = __gen_e_acsl_g_5(n + 1L);
- __gen_e_acsl_if_6 = __gen_e_acsl_g_8;
- }
- return __gen_e_acsl_if_6;
-}
-
-int __gen_e_acsl_f3_2(long n)
-{
- int __gen_e_acsl_if_5;
- if (n > 0L) {
- int __gen_e_acsl_g_4;
- int __gen_e_acsl_f3_4;
- __gen_e_acsl_g_4 = __gen_e_acsl_g((int)n);
- __gen_e_acsl_f3_4 = __gen_e_acsl_f3_2(n - 1L);
- __gen_e_acsl_if_5 = __gen_e_acsl_g_4 * __gen_e_acsl_f3_4 - 5;
- }
- else {
- int __gen_e_acsl_g_6;
- __gen_e_acsl_g_6 = __gen_e_acsl_g_5(n + 1L);
- __gen_e_acsl_if_5 = __gen_e_acsl_g_6;
- }
- return __gen_e_acsl_if_5;
-}
-
-unsigned long __gen_e_acsl_f4(int n)
-{
- unsigned long __gen_e_acsl_if_10;
- if (n < 100) {
- unsigned long __gen_e_acsl_f4_5;
- __gen_e_acsl_f4_5 = __gen_e_acsl_f4_2(n + 1L);
- __gen_e_acsl_if_10 = __gen_e_acsl_f4_5;
- }
- else {
- unsigned long __gen_e_acsl_if_9;
- if ((long)n < 9223372036854775807L) __gen_e_acsl_if_9 = 9223372036854775807UL;
- else __gen_e_acsl_if_9 = 6UL;
- __gen_e_acsl_if_10 = __gen_e_acsl_if_9;
- }
- return __gen_e_acsl_if_10;
-}
-
-unsigned long __gen_e_acsl_f4_2(long n)
-{
- unsigned long __gen_e_acsl_if_8;
- if (n < 100L) {
- unsigned long __gen_e_acsl_f4_4;
- __gen_e_acsl_f4_4 = __gen_e_acsl_f4_2(n + 1L);
- __gen_e_acsl_if_8 = __gen_e_acsl_f4_4;
- }
- else {
- unsigned long __gen_e_acsl_if_7;
- if (n < 9223372036854775807L) __gen_e_acsl_if_7 = 9223372036854775807UL;
- else __gen_e_acsl_if_7 = 6UL;
- __gen_e_acsl_if_8 = __gen_e_acsl_if_7;
- }
- return __gen_e_acsl_if_8;
-}
-
void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int n)
{
__e_acsl_mpz_t __gen_e_acsl_if_2;
@@ -317,4 +235,86 @@ int __gen_e_acsl_f2_2(long n)
return __gen_e_acsl_if_3;
}
+int __gen_e_acsl_g(int n)
+{
+ int __retres = 0;
+ return __retres;
+}
+
+int __gen_e_acsl_g_5(long n)
+{
+ int __retres = 0;
+ return __retres;
+}
+
+int __gen_e_acsl_f3(int n)
+{
+ int __gen_e_acsl_if_6;
+ if (n > 0) {
+ int __gen_e_acsl_g_2;
+ int __gen_e_acsl_f3_5;
+ __gen_e_acsl_g_2 = __gen_e_acsl_g(n);
+ __gen_e_acsl_f3_5 = __gen_e_acsl_f3_2(n - 1L);
+ __gen_e_acsl_if_6 = __gen_e_acsl_g_2 * __gen_e_acsl_f3_5 - 5;
+ }
+ else {
+ int __gen_e_acsl_g_8;
+ __gen_e_acsl_g_8 = __gen_e_acsl_g_5(n + 1L);
+ __gen_e_acsl_if_6 = __gen_e_acsl_g_8;
+ }
+ return __gen_e_acsl_if_6;
+}
+
+int __gen_e_acsl_f3_2(long n)
+{
+ int __gen_e_acsl_if_5;
+ if (n > 0L) {
+ int __gen_e_acsl_g_4;
+ int __gen_e_acsl_f3_4;
+ __gen_e_acsl_g_4 = __gen_e_acsl_g((int)n);
+ __gen_e_acsl_f3_4 = __gen_e_acsl_f3_2(n - 1L);
+ __gen_e_acsl_if_5 = __gen_e_acsl_g_4 * __gen_e_acsl_f3_4 - 5;
+ }
+ else {
+ int __gen_e_acsl_g_6;
+ __gen_e_acsl_g_6 = __gen_e_acsl_g_5(n + 1L);
+ __gen_e_acsl_if_5 = __gen_e_acsl_g_6;
+ }
+ return __gen_e_acsl_if_5;
+}
+
+unsigned long __gen_e_acsl_f4(int n)
+{
+ unsigned long __gen_e_acsl_if_10;
+ if (n < 100) {
+ unsigned long __gen_e_acsl_f4_5;
+ __gen_e_acsl_f4_5 = __gen_e_acsl_f4_2(n + 1L);
+ __gen_e_acsl_if_10 = __gen_e_acsl_f4_5;
+ }
+ else {
+ unsigned long __gen_e_acsl_if_9;
+ if ((long)n < 9223372036854775807L) __gen_e_acsl_if_9 = 9223372036854775807UL;
+ else __gen_e_acsl_if_9 = 6UL;
+ __gen_e_acsl_if_10 = __gen_e_acsl_if_9;
+ }
+ return __gen_e_acsl_if_10;
+}
+
+unsigned long __gen_e_acsl_f4_2(long n)
+{
+ unsigned long __gen_e_acsl_if_8;
+ if (n < 100L) {
+ unsigned long __gen_e_acsl_f4_4;
+ __gen_e_acsl_f4_4 = __gen_e_acsl_f4_2(n + 1L);
+ __gen_e_acsl_if_8 = __gen_e_acsl_f4_4;
+ }
+ else {
+ unsigned long __gen_e_acsl_if_7;
+ if (n < 9223372036854775807L) __gen_e_acsl_if_7 = 9223372036854775807UL;
+ else __gen_e_acsl_if_7 = 6UL;
+ __gen_e_acsl_if_8 = __gen_e_acsl_if_7;
+ }
+ return __gen_e_acsl_if_8;
+}
+
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
index 7943b9907d6..ab25e5f5395 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
@@ -223,6 +223,44 @@ int main(void)
__gmpq_clear(__gen_e_acsl__24);
}
/*@ assert 1.1d ≢ 1 + 0.1; */ ;
+ short a = (short)1;
+ short b = (short)1;
+ {
+ __e_acsl_mpq_t __gen_e_acsl__25;
+ __e_acsl_mpq_t __gen_e_acsl__26;
+ __e_acsl_mpq_t __gen_e_acsl_add_5;
+ __e_acsl_mpq_t __gen_e_acsl__27;
+ __e_acsl_mpq_t __gen_e_acsl__28;
+ __e_acsl_mpq_t __gen_e_acsl_sub_2;
+ int __gen_e_acsl_gt;
+ __gmpq_init(__gen_e_acsl__25);
+ __gmpq_set_si(__gen_e_acsl__25,(long)a,1UL);
+ __gmpq_init(__gen_e_acsl__26);
+ __gmpq_set_si(__gen_e_acsl__26,(long)((int)b),1UL);
+ __gmpq_init(__gen_e_acsl_add_5);
+ __gmpq_add(__gen_e_acsl_add_5,
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__25),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__26));
+ __gmpq_init(__gen_e_acsl__27);
+ __gmpq_set_d(__gen_e_acsl__27,2.);
+ __gmpq_init(__gen_e_acsl__28);
+ __gmpq_set_d(__gen_e_acsl__28,1.);
+ __gmpq_init(__gen_e_acsl_sub_2);
+ __gmpq_sub(__gen_e_acsl_sub_2,
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__27),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__28));
+ __gen_e_acsl_gt = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_add_5),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl_sub_2));
+ __e_acsl_assert(__gen_e_acsl_gt > 0,"Assertion","main","a + b > 2. - 1.",
+ "tests/arith/rationals.c",32);
+ __gmpq_clear(__gen_e_acsl__25);
+ __gmpq_clear(__gen_e_acsl__26);
+ __gmpq_clear(__gen_e_acsl_add_5);
+ __gmpq_clear(__gen_e_acsl__27);
+ __gmpq_clear(__gen_e_acsl__28);
+ __gmpq_clear(__gen_e_acsl_sub_2);
+ }
+ /*@ assert a + b > 2. - 1.; */ ;
__retres = 0;
return __retres;
}
@@ -275,7 +313,7 @@ double __gen_e_acsl_avg(double a, double b)
__gmpq_set(__gen_e_acsl_avg_real,
(__e_acsl_mpq_struct const *)(__gen_e_acsl_div));
__gmpq_init(__gen_e_acsl_delta_2);
- __gmpq_set_si(__gen_e_acsl_delta_2,(long)__gen_e_acsl_delta);
+ __gmpq_set_si(__gen_e_acsl_delta_2,(long)__gen_e_acsl_delta,1UL);
__gmpq_init(__gen_e_acsl_sub);
__gmpq_sub(__gen_e_acsl_sub,
(__e_acsl_mpq_struct const *)(__gen_e_acsl_avg_real),
@@ -290,7 +328,7 @@ double __gen_e_acsl_avg(double a, double b)
__e_acsl_mpq_t __gen_e_acsl__4;
int __gen_e_acsl_lt_2;
__gmpq_init(__gen_e_acsl_delta_3);
- __gmpq_set_si(__gen_e_acsl_delta_3,(long)__gen_e_acsl_delta);
+ __gmpq_set_si(__gen_e_acsl_delta_3,(long)__gen_e_acsl_delta,1UL);
__gmpq_init(__gen_e_acsl_add_2);
__gmpq_add(__gen_e_acsl_add_2,
(__e_acsl_mpq_struct const *)(__gen_e_acsl_avg_real),
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/rationals.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/rationals.res.oracle
index 6b6e958fe33..579fe2293bd 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/rationals.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/rationals.res.oracle
@@ -43,3 +43,5 @@
[eva:alarm] tests/arith/rationals.c:29: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/rationals.c:29: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/rationals.c:32: Warning:
+ function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/arith/rationals.c b/src/plugins/e-acsl/tests/arith/rationals.c
index 18ed5111f70..dbd2704d9a1 100644
--- a/src/plugins/e-acsl/tests/arith/rationals.c
+++ b/src/plugins/e-acsl/tests/arith/rationals.c
@@ -28,6 +28,9 @@ int main(void) {
/*@ assert 1.1d != 1 + 0.1; */ ;
+ short a = 1, b = 1;
+ //@ assert a+b > 2. - 1.; // gitlab public issue #14
+
// Not yet:
// long double ld = 0.1l;
// /*@ assert d + 1 != ld + 1; */ ; // long double
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1307.c
index dddabbabf17..7ecbe49081f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1307.c
@@ -272,9 +272,9 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
__gmpq_init(__gen_e_acsl_);
__gmpq_set_str(__gen_e_acsl_,"5",10);
__gmpq_init(__gen_e_acsl__2);
- __gmpq_set_si(__gen_e_acsl__2,5L);
+ __gmpq_set_si(__gen_e_acsl__2,5L,1UL);
__gmpq_init(__gen_e_acsl__3);
- __gmpq_set_si(__gen_e_acsl__3,80L);
+ __gmpq_set_si(__gen_e_acsl__3,80L,1UL);
__gmpq_init(__gen_e_acsl_div);
__gmpq_div(__gen_e_acsl_div,
(__e_acsl_mpq_struct const *)(__gen_e_acsl__2),
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
index 91010d0c7a4..19175f48356 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
@@ -277,6 +277,82 @@ void __gen_e_acsl_k(int x)
return;
}
+double __gen_e_acsl_f2(double x)
+{
+ __e_acsl_mpq_t __gen_e_acsl__13;
+ __e_acsl_mpq_t __gen_e_acsl__14;
+ __e_acsl_mpq_t __gen_e_acsl_div;
+ double __gen_e_acsl__15;
+ __gmpq_init(__gen_e_acsl__13);
+ __gmpq_set_str(__gen_e_acsl__13,"1",10);
+ __gmpq_init(__gen_e_acsl__14);
+ __gmpq_set_d(__gen_e_acsl__14,x);
+ __gmpq_init(__gen_e_acsl_div);
+ __gmpq_div(__gen_e_acsl_div,
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__13),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__14));
+ __gen_e_acsl__15 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl_div));
+ __gmpq_clear(__gen_e_acsl__13);
+ __gmpq_clear(__gen_e_acsl__14);
+ __gmpq_clear(__gen_e_acsl_div);
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__15); */
+ return __gen_e_acsl__15;
+}
+
+int __gen_e_acsl_g(int x)
+{
+ int __gen_e_acsl_g_hidden_2;
+ __gen_e_acsl_g_hidden_2 = __gen_e_acsl_g_hidden(x);
+ return __gen_e_acsl_g_hidden_2;
+}
+
+mystruct __gen_e_acsl_t1(mystruct m)
+{
+ return m;
+}
+
+int __gen_e_acsl_p1(int x, int y)
+{
+ __e_acsl_mpz_t __gen_e_acsl_x;
+ __e_acsl_mpz_t __gen_e_acsl_y;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ int __gen_e_acsl_gt;
+ __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
+ __gmpz_init_set_si(__gen_e_acsl_y,(long)y);
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,(__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y));
+ __gmpz_init_set_si(__gen_e_acsl_,0L);
+ __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ int __retres = __gen_e_acsl_gt > 0;
+ __gmpz_clear(__gen_e_acsl_x);
+ __gmpz_clear(__gen_e_acsl_y);
+ __gmpz_clear(__gen_e_acsl_add);
+ __gmpz_clear(__gen_e_acsl_);
+ return __retres;
+}
+
+void __gen_e_acsl_t2(__e_acsl_mpz_t *__retres_arg, mystruct m)
+{
+ __e_acsl_mpz_t __gen_e_acsl__10;
+ __e_acsl_mpz_t __gen_e_acsl__11;
+ __e_acsl_mpz_t __gen_e_acsl_add_7;
+ __gmpz_init_set_si(__gen_e_acsl__10,(long)m.k);
+ __gmpz_init_set_si(__gen_e_acsl__11,(long)m.l);
+ __gmpz_init(__gen_e_acsl_add_7);
+ __gmpz_add(__gen_e_acsl_add_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__10),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_7));
+ __gmpz_clear(__gen_e_acsl__10);
+ __gmpz_clear(__gen_e_acsl__11);
+ __gmpz_clear(__gen_e_acsl_add_7);
+ return;
+}
+
int __gen_e_acsl_p2(int x, int y)
{
__e_acsl_mpz_t __gen_e_acsl_x_2;
@@ -401,80 +477,4 @@ int __gen_e_acsl_g_hidden(int x)
return x;
}
-double __gen_e_acsl_f2(double x)
-{
- __e_acsl_mpq_t __gen_e_acsl__13;
- __e_acsl_mpq_t __gen_e_acsl__14;
- __e_acsl_mpq_t __gen_e_acsl_div;
- double __gen_e_acsl__15;
- __gmpq_init(__gen_e_acsl__13);
- __gmpq_set_str(__gen_e_acsl__13,"1",10);
- __gmpq_init(__gen_e_acsl__14);
- __gmpq_set_d(__gen_e_acsl__14,x);
- __gmpq_init(__gen_e_acsl_div);
- __gmpq_div(__gen_e_acsl_div,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__13),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__14));
- __gen_e_acsl__15 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl_div));
- __gmpq_clear(__gen_e_acsl__13);
- __gmpq_clear(__gen_e_acsl__14);
- __gmpq_clear(__gen_e_acsl_div);
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__15); */
- return __gen_e_acsl__15;
-}
-
-int __gen_e_acsl_g(int x)
-{
- int __gen_e_acsl_g_hidden_2;
- __gen_e_acsl_g_hidden_2 = __gen_e_acsl_g_hidden(x);
- return __gen_e_acsl_g_hidden_2;
-}
-
-mystruct __gen_e_acsl_t1(mystruct m)
-{
- return m;
-}
-
-int __gen_e_acsl_p1(int x, int y)
-{
- __e_acsl_mpz_t __gen_e_acsl_x;
- __e_acsl_mpz_t __gen_e_acsl_y;
- __e_acsl_mpz_t __gen_e_acsl_add;
- __e_acsl_mpz_t __gen_e_acsl_;
- int __gen_e_acsl_gt;
- __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
- __gmpz_init_set_si(__gen_e_acsl_y,(long)y);
- __gmpz_init(__gen_e_acsl_add);
- __gmpz_add(__gen_e_acsl_add,(__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_y));
- __gmpz_init_set_si(__gen_e_acsl_,0L);
- __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- int __retres = __gen_e_acsl_gt > 0;
- __gmpz_clear(__gen_e_acsl_x);
- __gmpz_clear(__gen_e_acsl_y);
- __gmpz_clear(__gen_e_acsl_add);
- __gmpz_clear(__gen_e_acsl_);
- return __retres;
-}
-
-void __gen_e_acsl_t2(__e_acsl_mpz_t *__retres_arg, mystruct m)
-{
- __e_acsl_mpz_t __gen_e_acsl__10;
- __e_acsl_mpz_t __gen_e_acsl__11;
- __e_acsl_mpz_t __gen_e_acsl_add_7;
- __gmpz_init_set_si(__gen_e_acsl__10,(long)m.k);
- __gmpz_init_set_si(__gen_e_acsl__11,(long)m.l);
- __gmpz_init(__gen_e_acsl_add_7);
- __gmpz_add(__gen_e_acsl_add_7,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__10),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_7));
- __gmpz_clear(__gen_e_acsl__10);
- __gmpz_clear(__gen_e_acsl__11);
- __gmpz_clear(__gen_e_acsl_add_7);
- return;
-}
-
--
GitLab