diff --git a/src/plugins/e-acsl/src/code_generator/constructor.ml b/src/plugins/e-acsl/src/code_generator/constructor.ml
index 9c7e60f4979d262a98e8ea79da9a41a0aa9d699d..eb010f92eb65a2cf9cacdd39a3e5ea53a47dd8d4 100644
--- a/src/plugins/e-acsl/src/code_generator/constructor.ml
+++ b/src/plugins/e-acsl/src/code_generator/constructor.ml
@@ -158,14 +158,9 @@ let mk_mark_readonly vi =
let loc = vi.vdecl in
mk_rtl_call ~loc "mark_readonly" [ Cil.evar ~loc vi ]
-let mk_runtime_check_with_msg ?(reverse=false) ~loc msg kind kf e =
+let mk_runtime_check_with_msg ~loc msg kind kf e =
let file = (fst loc).Filepath.pos_path in
let line = (fst loc).Filepath.pos_lnum in
- let e =
- if reverse
- then e
- else Cil.new_exp ~loc:e.eloc (UnOp(LNot, e, Cil.intType))
- in
mk_rtl_call ~loc
"assert"
[ e;
@@ -175,13 +170,13 @@ let mk_runtime_check_with_msg ?(reverse=false) ~loc msg kind kf e =
Cil.mkString ~loc (Filepath.Normalized.to_pretty_string file);
Cil.integer loc line ]
-let mk_runtime_check ?(reverse=false) kind kf e p =
+let mk_runtime_check kind kf e p =
let loc = p.pred_loc in
let msg =
Kernel.Unicode.without_unicode
(Format.asprintf "%a@?" Printer.pp_predicate) p
in
- mk_runtime_check_with_msg ~reverse ~loc msg kind kf e
+ mk_runtime_check_with_msg ~loc msg kind kf e
(*
Local Variables:
diff --git a/src/plugins/e-acsl/src/code_generator/constructor.mli b/src/plugins/e-acsl/src/code_generator/constructor.mli
index c309ad478045a7e41d6582ae886931bce1b0fdcd..676bfe14af6286cc19179f2d0c8c0aa1a6badc4e 100644
--- a/src/plugins/e-acsl/src/code_generator/constructor.mli
+++ b/src/plugins/e-acsl/src/code_generator/constructor.mli
@@ -80,16 +80,14 @@ type annotation_kind =
| RTE
val mk_runtime_check:
- ?reverse:bool -> annotation_kind -> kernel_function -> exp -> predicate ->
- stmt
+ annotation_kind -> kernel_function -> exp -> predicate -> stmt
(** [mk_runtime_check kind kf e p] generates a runtime check for predicate [p]
by building a call to [__e_acsl_assert]. [e] (or [!e] if [reverse] is set to
[true]) is the C translation of [p], [kf] is the current kernel_function and
[kind] is the annotation kind of [p]. *)
val mk_runtime_check_with_msg:
- ?reverse:bool -> loc:location -> string -> annotation_kind ->
- kernel_function -> exp -> stmt
+ loc:location -> string -> annotation_kind -> kernel_function -> exp -> stmt
(** [mk_runtime_check_with_msg kind kf e msg] generates a runtime check for [e]
(or [!e] if [reverse] is [true]) by building a call to [__e_acsl_assert].
[msg] is the message printed if the runtime check fails. [loc] is the
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index fe84f48fc299b5204eeb39a5439468e6b6110a5c..d76bac69fc4f89b825141d83ccc88461fb9f0289 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -253,7 +253,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
| Some p ->
let e, env = !named_predicate_ref kf (Env.push env) p in
let stmt, env =
- Constructor.mk_runtime_check ~reverse:true Constructor.RTE kf e p, env
+ Constructor.mk_runtime_check Constructor.RTE kf e p, env
in
let b, env = Env.pop_and_get env stmt ~global_clear:false Env.After in
let guard_for_small_type = Cil.mkStmt ~valid_sid:true (Block b) in
diff --git a/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml b/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
index 79332b5913879d1d17cb36cc878279dde66f5669..41a1245eed32cade67ec277a16e931e21de66282 100644
--- a/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
@@ -159,7 +159,7 @@ let gmp_to_sizet ~loc kf env size p =
None
sizet
(fun vi _ ->
- [ Constructor.mk_runtime_check ~reverse:true Constructor.RTE kf guard p;
+ [ Constructor.mk_runtime_check Constructor.RTE kf guard p;
Constructor.mk_lib_call ~loc
~result:(Cil.var vi)
"__gmpz_get_ui"
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 76d59a3eb9f1ac40038bf5a415dba121d6f77555..4e310e1b4adfbc577e2aaa98178f4be15ed50693 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -364,8 +364,9 @@ 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 =
@@ -373,9 +374,9 @@ and context_insensitive_term_to_exp kf env t =
(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
@@ -454,7 +455,6 @@ and context_insensitive_term_to_exp kf env t =
let pname = bop_name ^ "_rhs_fits_in_mp_bitcnt_t" in
let pred = { pred with pred_name = pname :: pred.pred_name } in
let cond = Constructor.mk_runtime_check
- ~reverse:true
Constructor.RTE
kf
coerce_guard
@@ -516,7 +516,6 @@ and context_insensitive_term_to_exp kf env t =
let e1_guard_cond =
let pred = Logic_const.prel ~loc (Rge, t1, zero) in
let cond = Constructor.mk_runtime_check
- ~reverse:true
Constructor.RTE
kf
e1_guard
@@ -1058,7 +1057,6 @@ and translate_named_predicate kf env p =
env
kf
(Constructor.mk_runtime_check
- ~reverse:true
(Env.annotation_kind env)
kf
e
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 6677db53488571ae0cb179d7c6504944131f9cd8..249a2e3366637540cf22f0fbbc67c8468d49a72d 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,8 +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_));
@@ -108,8 +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 7ee8de540851b4cfc13f744c22e4e0271e5e0561..0720b6503aa754f974b9df3eb49a3e708e503dd3 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 9899c99482fd3a9ee9baba785b2fe903ce547253..9db467e05fce5f01652cb191a4ef603018c77832 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,8 +194,8 @@ 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",
+ __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),
@@ -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,8 +620,8 @@ 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",
+ __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),