From dbf302f475e1504a4d03b5c6d12e8bb535ca2ee6 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 17 Dec 2014 15:50:15 +0100
Subject: [PATCH] [API] cleaner exported API
---
src/plugins/e-acsl/E_ACSL.mli | 19 ++++++++++++++++++-
src/plugins/e-acsl/env.ml | 5 +++++
src/plugins/e-acsl/env.mli | 4 ++++
src/plugins/e-acsl/error.mli | 3 +++
src/plugins/e-acsl/misc.ml | 6 +++++-
src/plugins/e-acsl/misc.mli | 3 +++
src/plugins/e-acsl/translate.ml | 15 +++++++++++++++
src/plugins/e-acsl/translate.mli | 3 +++
8 files changed, 56 insertions(+), 2 deletions(-)
diff --git a/src/plugins/e-acsl/E_ACSL.mli b/src/plugins/e-acsl/E_ACSL.mli
index f76219af1d1..6ffd281251f 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 4e1ff363fbd..8d401ba5e77 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 0343e789775..1a0e13f07b0 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 21cec1a235b..3352dc6f2d4 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 ab53dc9251e..35f6f19ca8c 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 80efacdd1a9..2a72f0d9e75 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 7278782bab3..1410745aa8b 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 2ff7451334c..0ae27eaab9d 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
--
GitLab