From 804a29eecef1d6b816f08f56a5b74ebfeec55554 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 4 Dec 2019 16:30:02 +0100
Subject: [PATCH] [e-acsl:archi] fix bug with \at
---
src/plugins/e-acsl/src/code_generator/env.ml | 11 ++++---
.../e-acsl/src/code_generator/injector.ml | 2 +-
.../e-acsl/src/code_generator/label.ml | 29 ++++++++++---------
.../e-acsl/src/code_generator/label.mli | 10 ++-----
4 files changed, 24 insertions(+), 28 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index 02b4b7faa95..ea222001d5a 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -338,14 +338,13 @@ let add_stmt ?(post=false) ?before env kf stmt =
let extend_stmt_in_place env stmt ~label block =
let new_stmt = Cil.mkStmt ~valid_sid:true (Block block) in
let sk = stmt.skind in
- stmt.skind <-
- Block (Cil.mkBlock [ new_stmt; Cil.mkStmt ~valid_sid:true sk ]);
- let pre = match label with
+ stmt.skind <- Block (Cil.mkBlock [ new_stmt; Cil.mkStmt ~valid_sid:true sk ]);
+ let pre = match label with
| BuiltinLabel(Here | Post) -> true
| BuiltinLabel(Old | Pre | LoopEntry | LoopCurrent | Init)
| FormalLabel _ | StmtLabel _ -> false
- in
- if pre then
+ in
+ if pre then
let local_env, tl_env = top env in
let b_info = local_env.block_info in
let b_info = { b_info with pre_stmts = new_stmt :: b_info.pre_stmts } in
@@ -493,6 +492,6 @@ let pretty fmt env =
(*
Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index 1486e115481..bd7844b2563 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-module E_acsl_label = Label (* [Label] is hidden by opening [Cil_datatype *)
+module E_acsl_label = Label (* [Label] is hidden when opening [Cil_datatype *)
open Cil_types
open Cil_datatype
diff --git a/src/plugins/e-acsl/src/code_generator/label.ml b/src/plugins/e-acsl/src/code_generator/label.ml
index a3f4d9e5012..02ad359e0ba 100644
--- a/src/plugins/e-acsl/src/code_generator/label.ml
+++ b/src/plugins/e-acsl/src/code_generator/label.ml
@@ -35,8 +35,6 @@ module Labeled_stmts =
let self = Labeled_stmts.self
-let new_labeled_stmt stmt = try Labeled_stmts.find stmt with Not_found -> stmt
-
let move kf ~old new_stmt =
let labels = old.labels in
match labels with
@@ -64,19 +62,24 @@ let move kf ~old new_stmt =
in
List.iter mv_label f.sallstmts
-let get_stmt kf = function
- | StmtLabel { contents = stmt } -> stmt
- | BuiltinLabel Here -> Error.not_yet "Label 'Here'"
- | BuiltinLabel(Old | Pre) ->
- (try Kernel_function.find_first_stmt kf
- with Kernel_function.No_Statement -> assert false)
- | BuiltinLabel(Post) ->
- (try Kernel_function.find_return kf
- with Kernel_function.No_Statement -> assert false)
- | BuiltinLabel _ | FormalLabel _ -> assert false
+let get_stmt kf llabel =
+ let stmt = match llabel with
+ | StmtLabel { contents = stmt } -> stmt
+ | BuiltinLabel Here -> Error.not_yet "Label 'Here'"
+ | BuiltinLabel(Old | Pre) ->
+ (try Kernel_function.find_first_stmt kf
+ with Kernel_function.No_Statement -> assert false)
+ | BuiltinLabel(Post) ->
+ (try Kernel_function.find_return kf
+ with Kernel_function.No_Statement -> assert false)
+ | BuiltinLabel _ | FormalLabel _ -> assert false
+ in
+ (* the pointed statement has been visited and modified by the injector:
+ get its new version. *)
+ try Labeled_stmts.find stmt with Not_found -> stmt
(*
Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/code_generator/label.mli b/src/plugins/e-acsl/src/code_generator/label.mli
index a47f1129d8e..f7550695537 100644
--- a/src/plugins/e-acsl/src/code_generator/label.mli
+++ b/src/plugins/e-acsl/src/code_generator/label.mli
@@ -23,22 +23,16 @@
open Cil_types
val move: kernel_function -> old:stmt -> stmt -> unit
-(** Move all labels of the [old] stmt onto the new [stmt].
- Both stmts must be in the new project. *)
+(** Move all labels of the [old] stmt onto the new [stmt]. *)
val get_stmt: kernel_function -> logic_label -> stmt
(** @return the statement where the logic label points to. *)
-(* [TODO ARCHI] currently unused: *)
-val new_labeled_stmt: stmt -> stmt
-(** @return the labeled stmt to use instead of the given one (which
- previously contained a label *)
-
val self: State.t
(** Internal state *)
(*
Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
End:
*)
--
GitLab