diff --git a/src/plugins/e-acsl/E_ACSL.mli b/src/plugins/e-acsl/E_ACSL.mli
index f76219af1d1bdbaddf5412166bb1a9b72ee503d2..6ffd281251f85218011c1c51049ad00a11772f88 100644
--- a/src/plugins/e-acsl/E_ACSL.mli
+++ b/src/plugins/e-acsl/E_ACSL.mli
@@ -22,10 +22,27 @@
 
 (** E-ACSL. *)
 
+open Cil_types
+
+module Error: sig
+  exception Typing_error of string
+  exception Not_yet of string
+end
+
+module Translate: sig
+  exception No_simple_translation of term
+  val term_to_exp: typ option -> term -> exp
+(** @raise Typing_error when the given term cannot be typed (something wrong
+    happends with this term)
+    @raise Not_yet when the given term contains an unsupported construct.
+    @raise No_simple_translation when the given term cannot be translated into
+    a single expression. *)
+end
+
 (** No function is directly exported: they are dynamically registered. *)
 
 (*
 Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make"
 End:
 *)
diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml
index 4e1ff363fbd6e7f4b17109d36fa0329b7212250a..8d401ba5e77d4e1ae295df6737b4b29f45646fb7 100644
--- a/src/plugins/e-acsl/env.ml
+++ b/src/plugins/e-acsl/env.ml
@@ -111,10 +111,15 @@ let empty v =
     loop_invariants = [];
     cpt = 0 }
 
+
 let top init env = 
   if init then env.init_env, []
   else match env.env_stack with [] -> assert false | hd :: tl -> hd, tl
 
+let has_no_new_stmt env =
+  let local, _ = top false env in
+  local.block_info = empty_block
+
 (* ************************************************************************** *)
 (** {2 Loop invariants} *)
 (* ************************************************************************** *)
diff --git a/src/plugins/e-acsl/env.mli b/src/plugins/e-acsl/env.mli
index 0343e789775531217db8b1aae191b479a5a6878d..1a0e13f07b09ac931a7fbb50a6e4edcbcd46b312 100644
--- a/src/plugins/e-acsl/env.mli
+++ b/src/plugins/e-acsl/env.mli
@@ -32,6 +32,10 @@ type t
 val dummy: t
 val empty: Visitor.frama_c_visitor -> t
 
+val has_no_new_stmt: t -> bool
+(** Assume that a local context has been previously pushed.
+    @return true iff the given env does not contain any new statement. *)
+
 val new_var:
   loc:location -> ?init:bool -> ?global:bool -> ?name:string -> 
   t -> term option -> typ -> 
diff --git a/src/plugins/e-acsl/error.mli b/src/plugins/e-acsl/error.mli
index 21cec1a235b102cc9a9c574fb907239f3e23c2ae..3352dc6f2d494a76bccf7ae834b4f431fa4e3985 100644
--- a/src/plugins/e-acsl/error.mli
+++ b/src/plugins/e-acsl/error.mli
@@ -22,6 +22,9 @@
 
 (** Handling errors. *)
 
+exception Typing_error of string
+exception Not_yet of string
+
 val untypable: string -> 'a
 (** Type error built from the given argument. *)
   
diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml
index ab53dc9251e105958f731f8f4bdd555420f87e17..35f6f19ca8cc34885c5b7e80fc2c5cf670e2c68a 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/src/plugins/e-acsl/misc.ml
@@ -53,10 +53,14 @@ let reset () = Datatype.String.Hashtbl.clear library_functions
 (** {2 Builders} *)
 (* ************************************************************************** *)
 
+exception Unregistered_library_function of string
 let mk_call ~loc ?result fname args =
   let vi =  
     try Datatype.String.Hashtbl.find library_functions fname
-    with Not_found -> Options.fatal "unregistered library function `%s'" fname
+    with Not_found ->
+      (* could not happen in normal mode, but coud be raised when E-ACSL is used
+         as a library *)
+      raise (Unregistered_library_function fname)
   in
   let f = Cil.evar ~loc vi in
   vi.vreferenced <- true;
diff --git a/src/plugins/e-acsl/misc.mli b/src/plugins/e-acsl/misc.mli
index 80efacdd1a9c70f64fd3a6037c9ac32e0aecb387..2a72f0d9e75e227d236a0b115eee248682fb4e74 100644
--- a/src/plugins/e-acsl/misc.mli
+++ b/src/plugins/e-acsl/misc.mli
@@ -29,7 +29,10 @@ open Cil_datatype
 (** {2 Builders} *)
 (* ************************************************************************** *)
 
+exception Unregistered_library_function of string
 val mk_call: loc:Location.t -> ?result:lval -> string -> exp list -> stmt
+(** @raise Unregistered_library_function *)
+
 val mk_debug_mmodel_stmt: stmt -> stmt
 
 type annotation_kind = 
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 7278782bab319cbd71b7b47d897348ba15897faa..1410745aa8b8c4d5eaa7c9dc148e96cd65c85565 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -723,6 +723,21 @@ let predicate_to_exp kf p =
   assert (Typ.equal (Cil.typeOf e) Cil.intType);
   e  
 
+exception No_simple_translation of term
+
+(* This function is used by plug-in [Cfp]. *)
+let term_to_exp ctx t =
+  Typing.type_term t;
+  let env = Env.empty (new Visitor.frama_c_copy Project_skeleton.dummy) in
+  let env = Env.push env in
+  let env = Env.rte env false in
+  let e, env =
+    try term_to_exp (Kernel_function.dummy ()) env ctx t
+    with Misc.Unregistered_library_function _ -> raise (No_simple_translation t)
+  in
+  if not (Env.has_no_new_stmt env) then raise (No_simple_translation t);
+  e
+
 (* ************************************************************************** *)
 (* [translate_*] translates a given ACSL annotation into the corresponding C
    statement (if any) for runtime assertion checking *)
diff --git a/src/plugins/e-acsl/translate.mli b/src/plugins/e-acsl/translate.mli
index 2ff7451334c3f48733c3d6e4c647dad4a0fbd150..0ae27eaab9dfc5efb8656522cc1c6d919221188c 100644
--- a/src/plugins/e-acsl/translate.mli
+++ b/src/plugins/e-acsl/translate.mli
@@ -43,6 +43,9 @@ val translate_rte_annots:
   code_annotation list ->
   Env.t
 
+exception No_simple_translation of term
+val term_to_exp: typ option -> term -> exp
+
 val predicate_to_exp: kernel_function -> predicate named -> exp
 
 val set_original_project: Project.t -> unit