[eacsl] Remove `reverse` parameter of `mk_runtime_check`

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 Cil.new_exp ~loc:e.eloc (UnOp(LNot, e, Cil.intType))
-    else e
-  in
   mk_rtl_call ~loc
     "assert"
     [ e;
@@ -175,18 +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 p =
-    if reverse
-    then Logic_const.pnot ~loc p
-    else p
-  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:

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