diff --git a/src/plugins/e-acsl/src/code_generator/constructor.ml b/src/plugins/e-acsl/src/code_generator/constructor.ml index 9c7e60f4979d262a98e8ea79da9a41a0aa9d699d..b39346ee6a9e04741cf4d01a4e7b610e572e19a7 100644 --- a/src/plugins/e-acsl/src/code_generator/constructor.ml +++ b/src/plugins/e-acsl/src/code_generator/constructor.ml @@ -163,8 +163,8 @@ let mk_runtime_check_with_msg ?(reverse=false) ~loc msg kind kf e = 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)) + then Cil.new_exp ~loc:e.eloc (UnOp(LNot, e, Cil.intType)) + else e in mk_rtl_call ~loc "assert" @@ -177,6 +177,11 @@ let mk_runtime_check_with_msg ?(reverse=false) ~loc msg kind kf e = let mk_runtime_check ?(reverse=false) 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