diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 9d8eb9a550327225c832ef0d6707923cd868bd76..a44d27242911d78ca3342a8cac5779d96a85f5d7 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -44,6 +44,13 @@ SRC_LIBRARIES:= \
varname
SRC_LIBRARIES:=$(addprefix src/libraries/, $(SRC_LIBRARIES))
+# project initializer
+SRC_PROJECT_INITIALIZER:= \
+ rtl \
+ prepare_ast
+SRC_PROJECT_INITIALIZER:=\
+ $(addprefix src/project_initializer/, $(SRC_PROJECT_INITIALIZER))
+
# analyses
SRC_ANALYSES:= \
rte \
@@ -55,13 +62,6 @@ SRC_ANALYSES:= \
typing
SRC_ANALYSES:=$(addprefix src/analyses/, $(SRC_ANALYSES))
-# project initializer
-SRC_PROJECT_INITIALIZER:= \
- rtl \
- prepare_ast
-SRC_PROJECT_INITIALIZER:=\
- $(addprefix src/project_initializer/, $(SRC_PROJECT_INITIALIZER))
-
# code generator
SRC_CODE_GENERATOR:= \
constructor \
@@ -100,8 +100,8 @@ PLUGIN_NAME:=E_ACSL
PLUGIN_CMO:= src/local_config \
src/options \
$(SRC_LIBRARIES) \
- $(SRC_ANALYSES) \
$(SRC_PROJECT_INITIALIZER) \
+ $(SRC_ANALYSES) \
$(SRC_CODE_GENERATOR) \
src/main
diff --git a/src/plugins/e-acsl/src/analyses/mmodel_analysis.ml b/src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
index fb984d7073e8af16a1f9c17f529816e35631b8e6..c480e318b764410dc8acfd272b8c28d27d3f75f6 100644
--- a/src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
+++ b/src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
@@ -620,7 +620,7 @@ end = struct
let compute init_set kf =
Options.feedback ~dkey ~level:2 "entering in function %a."
Kernel_function.pretty kf;
- assert (not (Misc.is_library_loc (Kernel_function.get_location kf)));
+ assert (not (Rtl.Symbols.mem_kf kf));
let tbl, is_init =
try Env.find kf, true
with Not_found -> Stmt.Hashtbl.create 17, false
@@ -660,7 +660,7 @@ end = struct
tbl
let get ?init kf =
- if Misc.is_library_loc (Kernel_function.get_location kf) then
+ if Rtl.Symbols.mem_kf kf then
Varinfo.Hptset.empty
else
try
@@ -799,6 +799,6 @@ let use_model () =
(*
Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/analyses/mmodel_analysis.mli b/src/plugins/e-acsl/src/analyses/mmodel_analysis.mli
index 39090f0dfa07a4100864ff0c20883bd9d79e7f3a..8c4967c2797f9c936b3c230b40a9cb0d476f6a37 100644
--- a/src/plugins/e-acsl/src/analyses/mmodel_analysis.mli
+++ b/src/plugins/e-acsl/src/analyses/mmodel_analysis.mli
@@ -44,6 +44,6 @@ val must_model_exp: ?kf:kernel_function -> ?stmt:stmt -> exp -> bool
(*
Local Variables:
- compile-command: "make"
+ compile-command: "make -C ../../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index 3722be14ad4101f2cb7097d414683c0ca0065ed3..dd1222051d790f8757da083c9f9628ac3be4d877 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -123,9 +123,9 @@ let rename_caller loc args exp = match exp.enode with
let name = Functions.RTL.libc_replacement_name vi.vname in
(* variadic arguments descriptor *)
let fmt = Functions.Libc.get_printf_argument_str ~loc vi.vname args in
- (* get the name of the library function we need. Cannot just rewrite the
- name as AST check will then fail *)
- let vi = Misc.get_lib_fun_vi name in
+ (* get the library function we need. Cannot just rewrite the name as AST
+ check will then fail *)
+ let vi = try Rtl.Symbols.find_vi name with Not_found -> assert false in
Cil.evar vi, fmt :: args
| _ ->
@@ -589,6 +589,7 @@ let inject_in_fundec main fundec =
in
List.iter unghost_formal fundec.sformals;
(* update environments *)
+ (* TODO: do it only for built-ins *)
Builtins.update vi.vname vi;
(* track function addresses but the main function that is tracked internally
via RTL *)
@@ -628,17 +629,15 @@ let unghost_vi vi =
let inject_in_global (env, main) = function
(* library functions and built-ins *)
| GVarDecl(vi, _) | GVar(vi, _, _)
- | GFunDecl(_, vi, _) | GFun({ svar = vi }, _)
- when Misc.is_library_loc vi.vdecl || Builtins.mem vi.vname ->
- Misc.register_library_function vi;
- if Builtins.mem vi.vname then Builtins.update vi.vname vi;
+ | GFunDecl(_, vi, _) | GFun({ svar = vi }, _) when Builtins.mem vi.vname ->
+ Builtins.update vi.vname vi;
env, main
(* Cil built-ins and other library globals: nothing to do *)
| GVarDecl(vi, _) | GVar(vi, _, _) | GFun({ svar = vi }, _)
when Misc.is_fc_or_compiler_builtin vi ->
env, main
- | g when Misc.is_library_loc (Global.loc g) ->
+ | g when Rtl.Symbols.mem_global g ->
env, main
(* variable declarations *)
@@ -845,7 +844,6 @@ let reset_all ast =
Options.Run.off ();
(* reset all the E-ACSL environments to their original states *)
Mmodel_analysis.reset ();
- Misc.reset ();
Logic_functions.reset ();
Literal_strings.reset ();
Global_observer.reset ();
@@ -862,7 +860,6 @@ let inject () =
Options.feedback ~level:2
"injecting annotations as code in project %a"
Project.pretty (Project.current ());
- Misc.reorder_ast ();
Gmp_types.init ();
let ast = Ast.get () in
inject_in_file ast;
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index f3cb0dc8de11b567298a59bd2167bfc9d7ee6e00..5c470efe5a0fa3014f8d418209daa1c74bf94417 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -1128,7 +1128,7 @@ let term_to_exp typ t =
let env = Env.rte env false in
let e, env =
try term_to_exp (Kernel_function.dummy ()) env t
- with Misc.Unregistered_library_function _ -> raise (No_simple_translation t)
+ with Rtl.Symbols.Unregistered _ -> raise (No_simple_translation t)
in
if not (Env.has_no_new_stmt env) then raise (No_simple_translation t);
e
diff --git a/src/plugins/e-acsl/src/libraries/builtins.ml b/src/plugins/e-acsl/src/libraries/builtins.ml
index 9bfe9fe7d7bf79638487c00e265ee2a35b533a79..fa5d9adf70ae5c12f251f9ba96bbcea4bc56558c 100644
--- a/src/plugins/e-acsl/src/libraries/builtins.ml
+++ b/src/plugins/e-acsl/src/libraries/builtins.ml
@@ -83,6 +83,6 @@ let () = Cmdline.run_after_configuring_stage init
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/libraries/builtins.mli b/src/plugins/e-acsl/src/libraries/builtins.mli
index 95dce5b8aab5bc88615f90a2274bccc9b79d521c..d15f53f6ef5284904b9f4c709a95cb78e7c6d5fc 100644
--- a/src/plugins/e-acsl/src/libraries/builtins.mli
+++ b/src/plugins/e-acsl/src/libraries/builtins.mli
@@ -35,6 +35,6 @@ val update: string -> Cil_types.varinfo -> unit
(*
Local Variables:
-compile-command: "make"
+compile-command: "make -C ../../../../.."
End:
*)
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index 0f4d38ef3fb6f37bd2ab33dd37c1f0d1ff021063..3ef0b0452028f3c97a11f0ac1373de59d6be88a6 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/src/plugins/e-acsl/src/libraries/misc.ml
@@ -20,7 +20,6 @@
(* *)
(**************************************************************************)
-module RTL = Functions.RTL
open Cil_types
open Cil_datatype
@@ -28,20 +27,6 @@ open Cil_datatype
(** {2 Handling the E-ACSL's C-libraries, part I} *)
(* ************************************************************************** *)
-let library_files () =
- List.map
- (fun d -> Options.Share.get_file ~mode:`Must_exist d)
- [ "e_acsl_gmp_api.h";
- "e_acsl.h" ]
-
-let is_library_loc (loc, _) = List.mem loc.Filepath.pos_path (library_files ())
-
-let library_functions = Datatype.String.Hashtbl.create 17
-let register_library_function vi =
- Datatype.String.Hashtbl.add library_functions vi.vname vi
-
-let reset () = Datatype.String.Hashtbl.clear library_functions
-
let is_fc_or_compiler_builtin vi =
Cil.is_builtin vi
||
@@ -51,20 +36,6 @@ let is_fc_or_compiler_builtin vi =
let prefix = String.sub vi.vname 0 prefix_length in
Datatype.String.equal prefix "__builtin_")
-(* ************************************************************************** *)
-(** {2 Builders} *)
-(* ************************************************************************** *)
-
-exception Unregistered_library_function of string
-let get_lib_fun_vi fname =
- try Datatype.String.Hashtbl.find library_functions fname
- with Not_found ->
- try Builtins.find fname
- with Not_found ->
- (* should not happen in normal mode, but could be raised when E-ACSL is
- used as a library *)
- raise (Unregistered_library_function fname)
-
(* ************************************************************************** *)
(** {2 Handling \result} *)
(* ************************************************************************** *)
@@ -89,17 +60,6 @@ let result_vi kf = match result_lhost kf with
let term_addr_of ~loc tlv ty =
Logic_const.taddrof ~loc tlv (Ctype (TPtr(ty, [])))
-let reorder_ast () =
- let ast = Ast.get() in
- let is_from_library = function
- | GType(ti, _) when ti.tname = "size_t" || ti.tname = "FILE"
- || RTL.is_rtl_name ti.tname -> true
- | GCompTag (ci, _) when RTL.is_rtl_name ci.cname -> true
- | GFunDecl(_, _, loc) | GVarDecl(_, loc) when is_library_loc loc -> true
- | _ -> false in
- let rtl, other = List.partition is_from_library ast.globals in
- ast.globals <- rtl @ other
-
let cty = function
| Ctype ty -> ty
| lty -> Options.fatal "Expecting a C type. Got %a" Printer.pp_logic_type lty
diff --git a/src/plugins/e-acsl/src/libraries/misc.mli b/src/plugins/e-acsl/src/libraries/misc.mli
index 1d2359202f752f482e32557377726c0719f23d3f..1a66d8cf412a9c0c2ef315e7797ff7b26fa8627c 100644
--- a/src/plugins/e-acsl/src/libraries/misc.mli
+++ b/src/plugins/e-acsl/src/libraries/misc.mli
@@ -24,14 +24,6 @@
open Cil_types
-(* ************************************************************************** *)
-(** {2 Builders} *)
-(* ************************************************************************** *)
-
-exception Unregistered_library_function of string
-val get_lib_fun_vi: string -> varinfo
-(** @return varinfo corresponding to a name of a given library function *)
-
(* ************************************************************************** *)
(** {2 Handling \result} *)
(* ************************************************************************** *)
@@ -46,11 +38,6 @@ val result_vi: kernel_function -> varinfo
(** {2 Handling the E-ACSL's C-libraries} *)
(* ************************************************************************** *)
-val library_files: unit -> Datatype.Filepath.t list
-val is_library_loc: location -> bool
-val register_library_function: varinfo -> unit
-val reset: unit -> unit
-
val is_fc_or_compiler_builtin: varinfo -> bool
(* ************************************************************************** *)
@@ -59,11 +46,6 @@ val is_fc_or_compiler_builtin: varinfo -> bool
val term_addr_of: loc:location -> term_lval -> typ -> term
-val reorder_ast: unit -> unit
-(* Reorder current AST by bringing all global declarations belonging to the
- * E-ACSL runtime library and their dependencies (e.g., typedef size_t) to
- * the very top of the file. *)
-
val cty: logic_type -> typ
(** Assume that the logic type is indeed a C type. Just return it. *)
diff --git a/src/plugins/e-acsl/src/main.ml b/src/plugins/e-acsl/src/main.ml
index 0c5bd0e1f59093b176297a32026044a6b3b5db41..5b73604151c17d72ba7d43a6cecbd72540585d74 100644
--- a/src/plugins/e-acsl/src/main.ml
+++ b/src/plugins/e-acsl/src/main.ml
@@ -71,7 +71,8 @@ let generate_code =
Project.on
copied_prj
(fun () ->
- (* preparation of the AST does not concern the E-ACSL RTL *)
+ (* preparation of the AST does not concern the E-ACSL RTL:
+ do it first *)
Prepare_ast.prepare ();
Rtl.link rtl_prj;
(* the E-ACSL type system ensures the soundness of the generated
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
index f5e31c7949f347cb4d850ad9ceed30c119dbe2e4..5324a4ffd3b79ee9888500d626e0543072266d62 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -410,8 +410,6 @@ class prepare_visitor = object (self)
not (Datatype.String.Set.mem vi.vname unduplicable_functions)
&& (* it is not a variadic function *)
not (self#is_variadic_function vi)
- && (* it is not in the E-ACSL's RTL *)
- not (Misc.is_library_loc loc)
&& (* it is not a built-in *)
not (Misc.is_fc_or_compiler_builtin vi)
&&
@@ -484,8 +482,8 @@ class prepare_visitor = object (self)
[ new_decl; g ]
| _ -> assert false)
- | GVarDecl(vi, loc) | GFunDecl(_, vi, loc) | GFun({ svar = vi }, loc)
- when Misc.is_library_loc loc || Misc.is_fc_or_compiler_builtin vi ->
+ | GVarDecl(vi, _loc) | GFunDecl(_, vi, _loc) | GFun({ svar = vi }, _loc)
+ when Misc.is_fc_or_compiler_builtin vi ->
Cil.DoChildren
| _ ->