diff --git a/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml b/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
index c9b710bc924f95102ee9ab0a3773537682fe278d..371c3b8dfbf8f81e55b0f76b0403b40bbff700ff 100644
--- a/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
+++ b/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
@@ -203,8 +203,8 @@ let index_from_sizes_and_shifts ~loc sizes_and_shifts =
in
sum
-let put_block_at_label env block label =
- let stmt = Label.get_stmt label in
+let put_block_at_label env kf block label =
+ let stmt = Label.get_stmt kf label in
let env_ref = ref env in
let o = object
inherit Visitor.frama_c_inplace
@@ -336,7 +336,7 @@ let to_exp ~loc kf env pot label =
Env.After
in
(* Put at label *)
- let env = put_block_at_label env storing_loops_block label in
+ let env = put_block_at_label env kf storing_loops_block label in
(* Returning *)
let lval_at_index, env = lval_at_index ~loc kf env (e_at, vi_at, t_index) in
let e = Cil.new_exp ~loc (Lval lval_at_index) in
diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index b6c1f7742c8938d5d927fc025b0512df3cf10956..1042770c680c09015d363bdb5eb04e2bbd8b685e 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -311,23 +311,15 @@ module Logic_scope = struct
else env
end
-let _emitter = (* [TODO ARCHI] *)
+let emitter =
Emitter.create
"E_ACSL"
[ Emitter.Code_annot ]
~correctness:[ Options.Gmp_only.parameter ]
~tuning:[]
-(* [TODO ARCHI] to be reimplemented *)
-let add_assert _env _stmt _annot = assert false
-(*match current_kf env with
- | None -> assert false
- | Some _kf ->
-(* Queue.add
- (fun () -> Annotations.add_assert emitter ~kf stmt annot)
- env.visitor#get_filling_actions
- *)*)
-
+(* [TODO ARCHI] to be inlined? *)
+let add_assert kf stmt annot = Annotations.add_assert emitter ~kf stmt annot
let add_stmt ?(post=false) ?before env kf stmt =
if not post then
diff --git a/src/plugins/e-acsl/src/code_generator/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli
index bfc4a75da8cf0c9ca2ca94ad774b9e4b301246d8..489a6907275b71b32cb6b5b14c5133d4866a97c6 100644
--- a/src/plugins/e-acsl/src/code_generator/env.mli
+++ b/src/plugins/e-acsl/src/code_generator/env.mli
@@ -75,7 +75,7 @@ module Logic_binding: sig
end
-val add_assert: t -> stmt -> predicate -> unit
+val add_assert: kernel_function -> stmt -> predicate -> unit
(** [add_assert env s p] associates the assertion [p] to the statement [s] in
the environment [env]. *)
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index e52e2631f6aaf968c16282f58d3d4582c28eee15..a4503120fd679521759deba4890bcadfa59decf7 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -426,12 +426,13 @@ let rec inject_in_substmt env kf stmt = match stmt.skind with
let env = inject_in_block env kf blk2 in
skind, env
- | TryExcept(blk1, (instrs, e), blk2, loc) ->
- let env = inject_in_block env kf blk1 in
+ | TryExcept(_blk1, (_instrs, _e), _blk2, _loc) ->
+ Error.not_yet "try ... except ..."
+(* let env = inject_in_block env kf blk1 in
let e, env = replace_literal_string_in_exp false env kf e in
let env = inject_in_block env kf blk2 in
ignore (assert false) (* TODO ARCHI: instrs *);
- TryExcept(blk1, (instrs, e), blk2, loc), env
+ TryExcept(blk1, (instrs, e), blk2, loc), env*)
(* nothing to do: *)
| Throw(None, _)
diff --git a/src/plugins/e-acsl/src/code_generator/label.ml b/src/plugins/e-acsl/src/code_generator/label.ml
index f6638213b5a6a709d1a21b0bfda26048d0671a99..fbbb0c6b4dcbf3d63968e68b452a9534dea2b180 100644
--- a/src/plugins/e-acsl/src/code_generator/label.ml
+++ b/src/plugins/e-acsl/src/code_generator/label.ml
@@ -69,19 +69,15 @@ let move kf ~old new_stmt =
in
List.iter mv_labels f.sallstmts
-(* [TODO ARCHI] reimplement it *)
-let get_stmt = function
+let get_stmt kf = function
| StmtLabel { contents = stmt } -> stmt
- | BuiltinLabel Here ->
-(* (match vis#current_stmt with
- | None -> Error.not_yet "label \"Here\" in function contract"
- | Some s -> s)*) assert false
+ | BuiltinLabel Here -> Error.not_yet "Label 'Here'"
| BuiltinLabel(Old | Pre) ->
-(* (try Kernel_function.find_first_stmt (Extlib.the vis#current_kf)
- with Kernel_function.No_Statement -> assert false)*)assert false
+ (try Kernel_function.find_first_stmt kf
+ with Kernel_function.No_Statement -> assert false)
| BuiltinLabel(Post) ->
-(* (try Kernel_function.find_return (Extlib.the vis#current_kf)
- with Kernel_function.No_Statement -> assert false)*) assert false
+ (try Kernel_function.find_return kf
+ with Kernel_function.No_Statement -> assert false)
| BuiltinLabel _ | FormalLabel _ -> assert false
(*
diff --git a/src/plugins/e-acsl/src/code_generator/label.mli b/src/plugins/e-acsl/src/code_generator/label.mli
index 194e2d2589e71afdb5052025317b6ff10c09c6a6..33cda6f389600a2953097308a4d3fb5bbc826a0b 100644
--- a/src/plugins/e-acsl/src/code_generator/label.mli
+++ b/src/plugins/e-acsl/src/code_generator/label.mli
@@ -26,7 +26,7 @@ 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. *)
-val get_stmt: logic_label -> stmt
+val get_stmt: kernel_function -> logic_label -> stmt
(** @return the statement where the logic label points to. *)
val new_labeled_stmt: stmt -> stmt
diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
index 8ac2421c992837dd13ee58d2289c55b71f4c397a..066849bd09a4573576c97d5e4876c2a6fc96c188 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -177,10 +177,8 @@ let generate_kf ~loc fname env ret_ty params_ty li =
in
Cil.setMaxId fundec;
let spec = Cil.empty_funspec () in
- (*[TODO ARCHI] reimplement *)
-(* Queue.add
- (fun () -> Globals.Functions.replace_by_definition spec fundec loc)
- (Env.get_visitor env)#get_filling_actions;*)
+ (* register the definition *)
+ Globals.Functions.replace_by_definition spec fundec loc;
(* create the kernel function itself *)
let kf = { fundec = Definition(fundec, loc); spec } in
(* closure generating the function's body.
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 9433bd739e7fa507c0aa3edb577138cb1eb5feb5..b87da402318bb6e13171e6734d5e8e77da87756d 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -369,7 +369,7 @@ and context_insensitive_term_to_exp kf env t =
guard
(Logic_const.prel ~loc (Req, t2, zero))
in
- Env.add_assert env cond (Logic_const.prel (Rneq, t2, zero));
+ Env.add_assert kf cond (Logic_const.prel (Rneq, t2, zero));
let instr = Misc.mk_call ~loc name [ e; e1; e2 ] in
[ cond; instr ]
in
@@ -619,7 +619,7 @@ and comparison_to_exp
Error.not_yet "comparison involving real numbers"
and at_to_exp_no_lscope env kf t_opt label e =
- let stmt = E_acsl_label.get_stmt label in
+ let stmt = E_acsl_label.get_stmt kf label in
(* generate a new variable denoting [\at(t',label)].
That is this variable which is the resulting expression.
ACSL typing rule ensures that the type of this variable is the same as
@@ -660,9 +660,10 @@ and at_to_exp_no_lscope env kf t_opt label e =
Cil.ChangeTo stmt
end
in
- let _new_stmt = Visitor.visitFramacStmt o stmt in
- (* [TODO ARCHI] reimplement *)
- (*Visitor_behavior.Set.stmt bhv stmt new_stmt;*)
+ (* [TODO ARCHI] is it still useful? *)
+ ignore (Visitor.visitFramacStmt o stmt);
+ (*let _new_stmt = Visitor.visitFramacStmt o stmt in
+ Visitor_behavior.Set.stmt bhv stmt new_stmt;*)
res, !env_ref, C_number
and env_of_li li kf env loc =