From 7cf1420c17a2833fa79a3d9493aeea29bfda378e Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Thu, 6 Aug 2020 17:15:57 +0200
Subject: [PATCH] [eacsl] Remove `reverse` parameter of `mk_runtime_check`
---
.../e-acsl/src/code_generator/constructor.ml | 16 +++-------------
.../e-acsl/src/code_generator/constructor.mli | 6 ++----
2 files changed, 5 insertions(+), 17 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/constructor.ml b/src/plugins/e-acsl/src/code_generator/constructor.ml
index b39346ee6a9..eb010f92eb6 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 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:
diff --git a/src/plugins/e-acsl/src/code_generator/constructor.mli b/src/plugins/e-acsl/src/code_generator/constructor.mli
index c309ad47804..676bfe14af6 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
--
GitLab