[API] cleaner exported API

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:
 *)

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} *)
 (* ************************************************************************** *)

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 -> 

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. *)
   

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;

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 = 

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 *)

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