From 57a28d8882e3313bf1a9d73a00d9b865a7d54116 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 28 Jul 2020 14:20:27 +0200
Subject: [PATCH] [eacsl] Update div by zero guard to not use `~reverse:true`
---
.../e-acsl/src/code_generator/translate.ml | 8 ++---
.../e-acsl/tests/arith/oracle_ci/gen_arith.c | 10 +++---
.../tests/arith/oracle_ci/gen_longlong.c | 4 +--
.../tests/gmp-only/oracle_ci/gen_arith.c | 32 +++++++++----------
4 files changed, 26 insertions(+), 28 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 341cd3d6f56..4e310e1b4ad 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -364,19 +364,19 @@ and context_insensitive_term_to_exp kf env t =
let guard, env =
let name = Misc.name_of_binop bop ^ "_guard" in
comparison_to_exp
- ~loc kf env Typing.gmpz ~e1:e2 ~name Eq t2 zero t
+ ~loc kf env Typing.gmpz ~e1:e2 ~name Ne t2 zero t
in
+ let p = Logic_const.prel ~loc (Rneq, t2, zero) in
let mk_stmts _v e =
assert (Gmp_types.Z.is_t ty);
let cond =
Constructor.mk_runtime_check
- ~reverse:true
(Env.annotation_kind env)
kf
guard
- (Logic_const.prel ~loc (Req, t2, zero))
+ p
in
- Env.add_assert kf cond (Logic_const.prel (Rneq, t2, zero));
+ Env.add_assert kf cond p;
let instr = Constructor.mk_lib_call ~loc name [ e; e1; e2 ] in
[ cond; instr ]
in
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c
index 2dd0194bc1b..249a2e33666 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c
@@ -39,9 +39,8 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
__gmpz_init(__gen_e_acsl_div);
/*@ assert E_ACSL: 0xffffffffffffffffffffff ≢ 0; */
- __e_acsl_assert(! (__gen_e_acsl_div_guard == 0),"Assertion","main",
- "!(0xffffffffffffffffffffff == 0)","tests/arith/arith.i",
- 18);
+ __e_acsl_assert(__gen_e_acsl_div_guard != 0,"Assertion","main",
+ "0xffffffffffffffffffffff != 0","tests/arith/arith.i",18);
__gmpz_tdiv_q(__gen_e_acsl_div,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_));
@@ -109,9 +108,8 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
__gmpz_init(__gen_e_acsl_div_2);
/*@ assert E_ACSL: y - 123456789123456789 ≢ 0; */
- __e_acsl_assert(! (__gen_e_acsl_div_guard_2 == 0),"Assertion","main",
- "!(y - 123456789123456789 == 0)","tests/arith/arith.i",
- 34);
+ __e_acsl_assert(__gen_e_acsl_div_guard_2 != 0,"Assertion","main",
+ "y - 123456789123456789 != 0","tests/arith/arith.i",34);
__gmpz_tdiv_q(__gen_e_acsl_div_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c
index 49e97395390..0720b6503aa 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c
@@ -54,8 +54,8 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
__gmpz_init(__gen_e_acsl_mod);
/*@ assert E_ACSL: 2 ≢ 0; */
- __e_acsl_assert(! (__gen_e_acsl_mod_guard == 0),"Assertion","main",
- "!(2 == 0)","tests/arith/longlong.i",17);
+ __e_acsl_assert(__gen_e_acsl_mod_guard != 0,"Assertion","main","2 != 0",
+ "tests/arith/longlong.i",17);
__gmpz_tdiv_r(__gen_e_acsl_mod,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_));
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
index efc5103682b..9db467e05fc 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
@@ -160,8 +160,8 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
__gmpz_init(__gen_e_acsl_div);
/*@ assert E_ACSL: 3 ≢ 0; */
- __e_acsl_assert(! (__gen_e_acsl_div_guard == 0),"Assertion","main",
- "!(3 == 0)","tests/gmp-only/arith.i",17);
+ __e_acsl_assert(__gen_e_acsl_div_guard != 0,"Assertion","main","3 != 0",
+ "tests/gmp-only/arith.i",17);
__gmpz_tdiv_q(__gen_e_acsl_div,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_x_6),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
@@ -194,9 +194,9 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__14));
__gmpz_init(__gen_e_acsl_div_2);
/*@ assert E_ACSL: 0xffffffffffffffffffffff ≢ 0; */
- __e_acsl_assert(! (__gen_e_acsl_div_guard_2 == 0),"Assertion","main",
- "!(0xffffffffffffffffffffff == 0)",
- "tests/gmp-only/arith.i",18);
+ __e_acsl_assert(__gen_e_acsl_div_guard_2 != 0,"Assertion","main",
+ "0xffffffffffffffffffffff != 0","tests/gmp-only/arith.i",
+ 18);
__gmpz_tdiv_q(__gen_e_acsl_div_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl__13),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__13));
@@ -228,8 +228,8 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__17));
__gmpz_init(__gen_e_acsl_mod);
/*@ assert E_ACSL: 2 ≢ 0; */
- __e_acsl_assert(! (__gen_e_acsl_mod_guard == 0),"Assertion","main",
- "!(2 == 0)","tests/gmp-only/arith.i",19);
+ __e_acsl_assert(__gen_e_acsl_mod_guard != 0,"Assertion","main","2 != 0",
+ "tests/gmp-only/arith.i",19);
__gmpz_tdiv_r(__gen_e_acsl_mod,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_x_7),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__16));
@@ -273,8 +273,8 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__21));
__gmpz_init(__gen_e_acsl_mod_2);
/*@ assert E_ACSL: -2 ≢ 0; */
- __e_acsl_assert(! (__gen_e_acsl_mod_guard_2 == 0),"Assertion","main",
- "!(-2 == 0)","tests/gmp-only/arith.i",20);
+ __e_acsl_assert(__gen_e_acsl_mod_guard_2 != 0,"Assertion","main",
+ "-2 != 0","tests/gmp-only/arith.i",20);
__gmpz_tdiv_r(__gen_e_acsl_mod_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_neg_8),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_neg_9));
@@ -315,8 +315,8 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__25));
__gmpz_init(__gen_e_acsl_mod_3);
/*@ assert E_ACSL: -2 ≢ 0; */
- __e_acsl_assert(! (__gen_e_acsl_mod_guard_3 == 0),"Assertion","main",
- "!(-2 == 0)","tests/gmp-only/arith.i",21);
+ __e_acsl_assert(__gen_e_acsl_mod_guard_3 != 0,"Assertion","main",
+ "-2 != 0","tests/gmp-only/arith.i",21);
__gmpz_tdiv_r(__gen_e_acsl_mod_3,
(__e_acsl_mpz_struct const *)(__gen_e_acsl__23),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_neg_11));
@@ -574,8 +574,8 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__55));
__gmpz_init(__gen_e_acsl_div_3);
/*@ assert E_ACSL: y ≢ 0; */
- __e_acsl_assert(! (__gen_e_acsl_div_guard_3 == 0),"Assertion","main",
- "!(y == 0)","tests/gmp-only/arith.i",31);
+ __e_acsl_assert(__gen_e_acsl_div_guard_3 != 0,"Assertion","main",
+ "y != 0","tests/gmp-only/arith.i",31);
__gmpz_tdiv_q(__gen_e_acsl_div_3,
(__e_acsl_mpz_struct const *)(__gen_e_acsl__54),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_y_2));
@@ -620,9 +620,9 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__59));
__gmpz_init(__gen_e_acsl_div_4);
/*@ assert E_ACSL: y - 123456789123456789 ≢ 0; */
- __e_acsl_assert(! (__gen_e_acsl_div_guard_4 == 0),"Assertion","main",
- "!(y - 123456789123456789 == 0)",
- "tests/gmp-only/arith.i",34);
+ __e_acsl_assert(__gen_e_acsl_div_guard_4 != 0,"Assertion","main",
+ "y - 123456789123456789 != 0","tests/gmp-only/arith.i",
+ 34);
__gmpz_tdiv_q(__gen_e_acsl_div_4,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add_5),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_4));
--
GitLab