diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml index 02b4b7faa95a33954802c207666dc309f3d2b669..ea222001d5afe9684ce9884697d338be1046d854 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 1486e115481a3c1e95490a6e96a9067ee68b3c17..bd7844b256330c5b79f58faa01035418cd8badc8 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 a3f4d9e50124dbb183eaff7132860ddd318073cd..02ad359e0ba34bad4969d2d64fb8b5683e473197 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 a47f1129d8e1199611cd4123a762848bb3d1b9c5..f75506955372aab36307edfac044ff9b5d2c7038 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: *)