[eacsl] Update call sites of `mk_runtime_check`

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

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"

src/plugins/e-acsl/src/code_generator/translate.ml

@@ -370,6 +370,7 @@ and context_insensitive_term_to_exp kf env t =
         assert (Gmp_types.Z.is_t ty);
         let cond =
           Constructor.mk_runtime_check
+            ~reverse:true
             (Env.annotation_kind env)
             kf
             guard
@@ -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

src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c

@@ -40,7 +40,8 @@ int main(void)
     __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);
+                    "!(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,7 +110,8 @@ int main(void)
     __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);
+                    "!(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));

src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c

@@ -55,7 +55,7 @@ int main(void)
     __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);
+                    "!(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_));

src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c

@@ -161,7 +161,7 @@ int main(void)
     __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);
+                    "!(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));
@@ -195,8 +195,8 @@ int main(void)
     __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);
+                    "!(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));
@@ -229,7 +229,7 @@ int main(void)
     __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);
+                    "!(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));
@@ -274,7 +274,7 @@ int main(void)
     __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);
+                    "!(-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));
@@ -316,7 +316,7 @@ int main(void)
     __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);
+                    "!(-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));
@@ -575,7 +575,7 @@ int main(void)
     __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);
+                    "!(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));
@@ -621,8 +621,8 @@ int main(void)
     __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);
+                    "!(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));