diff --git a/src/plugins/e-acsl/env.mli b/src/plugins/e-acsl/env.mli
index ac510497cf293f7bca3afc2f0f5b2691e2063b6a..a5ff820a2d7c8ddf8d3857681c5c7db76ae51ed8 100644
--- a/src/plugins/e-acsl/env.mli
+++ b/src/plugins/e-acsl/env.mli
@@ -60,6 +60,10 @@ val add_stmt: t -> stmt -> t
   (** [add_stmt env s] extends [env] with the new statement [s] *)
 
 val extend_stmt_in_place: t -> stmt -> pre:bool -> block -> t
+(**  [extend_stmt_in_place env stmt ~pre b] modifies [stmt] in place in order to
+     add the given [block]. If [pre] is [true], then this block is guaranteed
+     to be at the first place of the resulting [stmt] whatever modification
+     will be done by the visitor later. *)
 
 val push: t -> t
 (** Push a new local context in the environment *)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
index 42f8891516ecf6aef1553d6d8ba96421deaddda5..e678905c8aa45ad17ed3d605850d79c92a7e0210 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
@@ -1,4 +1,4 @@
-tests/e-acsl-runtime/result.i:7:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
+tests/e-acsl-runtime/result.i:6:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/result.i b/src/plugins/e-acsl/tests/e-acsl-runtime/result.i
index b18c3c412ae8e50f930292988a25126907ee2bc2..2e7e3c1602314fe178a7c925084d375eafa8f87b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/result.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/result.i
@@ -1,9 +1,8 @@
 /* run.config
    COMMENT: \result
-   EXECNOW: LOG gen_result.c BIN gen_result.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/result.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_result.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_result.out ./tests/e-acsl-runtime/result/gen_result.c -lgmp
+   EXECNOW: LOG gen_result.c BIN gen_result.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/result.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_result.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_result.out ./tests/e-acsl-runtime/result/gen_result.c -lgmp && ./tests/e-acsl-runtime/result/gen_result.out
 */
 
-// && ./tests/e-acsl-runtime/result/gen_result.out
 /*@ ensures \result == (int)(x - x); */
 int f(int x) { 
   x = 0; 
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 1d852dd77ccf72c389d3e92479647584606dbd5e..9fabddae6f66471fb1fa7be3fc0934008ef88c26 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -363,8 +363,8 @@ and context_insensitive_term_to_exp env t =
   | Tbase_addr _ -> Misc.not_yet "\\base_addr"
   | Tblock_length _ -> Misc.not_yet "\\block_length"
   | Tnull -> mkCast (zero ~loc) (TPtr(TVoid [], [])), env, false
-  | TCoerce _ -> Misc.not_yet "coercion"
-  | TCoerceE _ -> Misc.not_yet "expression coercion"
+  | TCoerce _ -> Misc.not_yet "coercion" (* Jessie specific *)
+  | TCoerceE _ -> Misc.not_yet "expression coercion" (* Jessie specific *)
   | TUpdate _ -> Misc.not_yet "functional update"
   | Ttypeof _ -> Misc.not_yet "typeof"
   | Ttype _ -> Misc.not_yet "C type"
@@ -480,7 +480,7 @@ let rec named_predicate_to_exp env p =
   | Pvalid_index _ -> Misc.not_yet "\\valid_index"
   | Pvalid_range _ -> Misc.not_yet "\\valid_range"
   | Pfresh _ -> Misc.not_yet "\\fresh"
-  | Psubtype _ -> Misc.not_yet "subtyping relation"
+  | Psubtype _ -> Misc.not_yet "subtyping relation" (* Jessie specific? *)
   | Pinitialized _ -> Misc.not_yet "\\initialized"
 
 (* ************************************************************************** *)
@@ -706,11 +706,8 @@ class e_acsl_visitor prj generate = object (self)
 	  (* must generate [pre_block] which includes [stmt] before generating
 	     [post_block] *)
 	  let pre_block, env = 
-(*	  Options.feedback "HERE";*)
-	    (*Project.on prj*) (fun () -> Env.pop_and_get env stmt
-	      ~global_clear:false Env.After ) ()
+	    Env.pop_and_get env stmt ~global_clear:false Env.After
 	  in
-(*	  Options.feedback "DONE";*)
 	  let env = mk_post_env (Env.push env) in
 	  let post_block, env = 
 	    Env.pop_and_get