From 95b03c27d21522f43e19164269a92a05eb61af0f Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 24 Jun 2020 11:54:11 +0200
Subject: [PATCH] [eacsl] Fix `reverse` parameter of `mk_runtime_check`
---
src/plugins/e-acsl/src/code_generator/constructor.ml | 9 +++++++--
1 file changed, 7 insertions(+), 2 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/constructor.ml b/src/plugins/e-acsl/src/code_generator/constructor.ml
index 9c7e60f4979..b39346ee6a9 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
--
GitLab