diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index d00b9eb32854b05999f4b7bd96fa219a8b78f947..9ffefdf917e713a53bbed1c6b3f3581244ee39af 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -27,6 +27,8 @@ Plugin E-ACSL 21.0 (Scandium)
-* E-ACSL [2020-06-10] Fix ##13: bug when mixing integers and floats in
annotations while -e-acsl-gmp-only is activated.
+-* E-ACSL [2020-06-10] Fix a soundness bug (##14) when initializing
+ rationals from integers.
-* E-ACSL [2020-03-24] Fix automatic deactivation of plug-in Variadic when
E-ACSL is directly called from Frama-C without using
e-acsl-gcc.sh.
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 829f7cf15b4d20b25f6e62e3623fb91def86b629..625d41ea3e4a89d66a369913c8b75db81ec1c4bd 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,13 @@ 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_ui(mpq_t q, unsigned long int n, unsigned long int d)
+ __attribute__((FC_BUILTIN));
+
+/*@ requires \valid(q);
+ @ 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,7 +163,6 @@ 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)
__attribute__((FC_BUILTIN));
diff --git a/src/plugins/e-acsl/src/code_generator/gmp.ml b/src/plugins/e-acsl/src/code_generator/gmp.ml
index dd373192bd113630f469a3c4d6d468bc51acf3a8..89ea82b0bdf32a031d9fe4c25795decb950b0e39 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 d2b467d7fbcce7824d7afc25407a44a04bf575ca..db4811dbeca2f1b6925cdc933215ea28c7a5cded 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 8a80b25247831cfca43226478f5dced6e8568b54..80def032755930359080079ccbadfa15976977d8 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,62 +232,6 @@ void __gen_e_acsl_k(int x)
return;
}
-int __gen_e_acsl_p2(int x, int y)
-{
- int __retres = x + (long)y > 0L;
- return __retres;
-}
-
-int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y)
-{
- __e_acsl_mpz_t __gen_e_acsl_x;
- __e_acsl_mpz_t __gen_e_acsl_add;
- __e_acsl_mpz_t __gen_e_acsl__2;
- int __gen_e_acsl_gt;
- __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
- __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 *)(y));
- __gmpz_init_set_si(__gen_e_acsl__2,0L);
- __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- int __retres = __gen_e_acsl_gt > 0;
- __gmpz_clear(__gen_e_acsl_x);
- __gmpz_clear(__gen_e_acsl_add);
- __gmpz_clear(__gen_e_acsl__2);
- return __retres;
-}
-
-int __gen_e_acsl_p2_5(int x, long y)
-{
- __e_acsl_mpz_t __gen_e_acsl_x_2;
- __e_acsl_mpz_t __gen_e_acsl_y;
- __e_acsl_mpz_t __gen_e_acsl_add_2;
- __e_acsl_mpz_t __gen_e_acsl__3;
- int __gen_e_acsl_gt_2;
- __gmpz_init_set_si(__gen_e_acsl_x_2,(long)x);
- __gmpz_init_set_si(__gen_e_acsl_y,y);
- __gmpz_init(__gen_e_acsl_add_2);
- __gmpz_add(__gen_e_acsl_add_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_y));
- __gmpz_init_set_si(__gen_e_acsl__3,0L);
- __gen_e_acsl_gt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
- int __retres = __gen_e_acsl_gt_2 > 0;
- __gmpz_clear(__gen_e_acsl_x_2);
- __gmpz_clear(__gen_e_acsl_y);
- __gmpz_clear(__gen_e_acsl_add_2);
- __gmpz_clear(__gen_e_acsl__3);
- return __retres;
-}
-
-int __gen_e_acsl_k_pred(int x)
-{
- int __retres = x > 0;
- return __retres;
-}
-
long __gen_e_acsl_f1(int x, int y)
{
long __retres = x + (long)y;
@@ -384,4 +328,60 @@ long __gen_e_acsl_t2(mystruct m)
return __retres;
}
+int __gen_e_acsl_p2(int x, int y)
+{
+ int __retres = x + (long)y > 0L;
+ return __retres;
+}
+
+int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y)
+{
+ __e_acsl_mpz_t __gen_e_acsl_x;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ int __gen_e_acsl_gt;
+ __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
+ __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 *)(y));
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
+ __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ int __retres = __gen_e_acsl_gt > 0;
+ __gmpz_clear(__gen_e_acsl_x);
+ __gmpz_clear(__gen_e_acsl_add);
+ __gmpz_clear(__gen_e_acsl__2);
+ return __retres;
+}
+
+int __gen_e_acsl_p2_5(int x, long y)
+{
+ __e_acsl_mpz_t __gen_e_acsl_x_2;
+ __e_acsl_mpz_t __gen_e_acsl_y;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
+ __e_acsl_mpz_t __gen_e_acsl__3;
+ int __gen_e_acsl_gt_2;
+ __gmpz_init_set_si(__gen_e_acsl_x_2,(long)x);
+ __gmpz_init_set_si(__gen_e_acsl_y,y);
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y));
+ __gmpz_init_set_si(__gen_e_acsl__3,0L);
+ __gen_e_acsl_gt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
+ int __retres = __gen_e_acsl_gt_2 > 0;
+ __gmpz_clear(__gen_e_acsl_x_2);
+ __gmpz_clear(__gen_e_acsl_y);
+ __gmpz_clear(__gen_e_acsl_add_2);
+ __gmpz_clear(__gen_e_acsl__3);
+ return __retres;
+}
+
+int __gen_e_acsl_k_pred(int x)
+{
+ int __retres = x > 0;
+ 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 d7e6ba9cda321e94b0312fcf67ef5007ba3a8486..df6e9ac544b3ee77be4bebf10abcd8e6477d8f4a 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,18 +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;
@@ -317,4 +305,16 @@ 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;
+}
+
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 7943b9907d694f73cfb478d604c04ca8a7ded3e2..ab25e5f5395d1d1648a723cd7583b42285a50201 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 6b6e958fe3307d88f08470895bdaf3de1960c169..579fe2293bd7fa3291abc370fd91f851bfda71fd 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 18ed5111f7089b4cb079af9d45d206907818ee31..dbd2704d9a182eddc59ef1bef383fca8b45ce2d9 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 dddabbabf17a85dca959564d00be7bd85e1a3ae4..7ecbe49081f97141b4826d44f36fe9f8ff8e1acd 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 f06e60821c04add5c9810dbadc3719b7def1ed9d..585642b7869b6a307e48864ea886e06469894f5d 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
@@ -288,66 +288,6 @@ void __gen_e_acsl_k(int x)
return;
}
-int __gen_e_acsl_p2(int x, int y)
-{
- __e_acsl_mpz_t __gen_e_acsl_x_2;
- __e_acsl_mpz_t __gen_e_acsl_y_2;
- __e_acsl_mpz_t __gen_e_acsl_add_2;
- __e_acsl_mpz_t __gen_e_acsl__2;
- int __gen_e_acsl_gt_2;
- __gmpz_init_set_si(__gen_e_acsl_x_2,(long)x);
- __gmpz_init_set_si(__gen_e_acsl_y_2,(long)y);
- __gmpz_init(__gen_e_acsl_add_2);
- __gmpz_add(__gen_e_acsl_add_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_2));
- __gmpz_init_set_si(__gen_e_acsl__2,0L);
- __gen_e_acsl_gt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- int __retres = __gen_e_acsl_gt_2 > 0;
- __gmpz_clear(__gen_e_acsl_x_2);
- __gmpz_clear(__gen_e_acsl_y_2);
- __gmpz_clear(__gen_e_acsl_add_2);
- __gmpz_clear(__gen_e_acsl__2);
- return __retres;
-}
-
-int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y)
-{
- __e_acsl_mpz_t __gen_e_acsl_x_3;
- __e_acsl_mpz_t __gen_e_acsl_add_3;
- __e_acsl_mpz_t __gen_e_acsl__4;
- int __gen_e_acsl_gt_3;
- __gmpz_init_set_si(__gen_e_acsl_x_3,(long)x);
- __gmpz_init(__gen_e_acsl_add_3);
- __gmpz_add(__gen_e_acsl_add_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
- (__e_acsl_mpz_struct const *)(y));
- __gmpz_init_set_si(__gen_e_acsl__4,0L);
- __gen_e_acsl_gt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
- int __retres = __gen_e_acsl_gt_3 > 0;
- __gmpz_clear(__gen_e_acsl_x_3);
- __gmpz_clear(__gen_e_acsl_add_3);
- __gmpz_clear(__gen_e_acsl__4);
- return __retres;
-}
-
-int __gen_e_acsl_k_pred(int x)
-{
- __e_acsl_mpz_t __gen_e_acsl_x;
- __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_,0L);
- __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
- (__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_);
- return __retres;
-}
-
void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int x, int y)
{
__e_acsl_mpz_t __gen_e_acsl_x_4;
@@ -488,4 +428,64 @@ void __gen_e_acsl_t2(__e_acsl_mpz_t *__retres_arg, mystruct m)
return;
}
+int __gen_e_acsl_p2(int x, int y)
+{
+ __e_acsl_mpz_t __gen_e_acsl_x_2;
+ __e_acsl_mpz_t __gen_e_acsl_y_2;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ int __gen_e_acsl_gt_2;
+ __gmpz_init_set_si(__gen_e_acsl_x_2,(long)x);
+ __gmpz_init_set_si(__gen_e_acsl_y_2,(long)y);
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_2));
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
+ __gen_e_acsl_gt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ int __retres = __gen_e_acsl_gt_2 > 0;
+ __gmpz_clear(__gen_e_acsl_x_2);
+ __gmpz_clear(__gen_e_acsl_y_2);
+ __gmpz_clear(__gen_e_acsl_add_2);
+ __gmpz_clear(__gen_e_acsl__2);
+ return __retres;
+}
+
+int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y)
+{
+ __e_acsl_mpz_t __gen_e_acsl_x_3;
+ __e_acsl_mpz_t __gen_e_acsl_add_3;
+ __e_acsl_mpz_t __gen_e_acsl__4;
+ int __gen_e_acsl_gt_3;
+ __gmpz_init_set_si(__gen_e_acsl_x_3,(long)x);
+ __gmpz_init(__gen_e_acsl_add_3);
+ __gmpz_add(__gen_e_acsl_add_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
+ (__e_acsl_mpz_struct const *)(y));
+ __gmpz_init_set_si(__gen_e_acsl__4,0L);
+ __gen_e_acsl_gt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+ int __retres = __gen_e_acsl_gt_3 > 0;
+ __gmpz_clear(__gen_e_acsl_x_3);
+ __gmpz_clear(__gen_e_acsl_add_3);
+ __gmpz_clear(__gen_e_acsl__4);
+ return __retres;
+}
+
+int __gen_e_acsl_k_pred(int x)
+{
+ __e_acsl_mpz_t __gen_e_acsl_x;
+ __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_,0L);
+ __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
+ (__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_);
+ return __retres;
+}
+