diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 508230d7c8c933b49215876099e358da74ff20ed..906403ec31d7d23a95bc4be30992c333c53901f1 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -2487,10 +2487,10 @@ following.
~
\begin{ocamlcode}
-!Db.Value.compute();
-Kernel.feedback "%B" (Db.Value.is_computed ()); (* true *)
+Eva.Analysis.compute();
+Kernel.feedback "%B" (Eva.Analysis.is_computed ()); (* true *)
Globals.set_entry_point "f" true;
-Kernel.feedback "%B" (Db.Value.is_computed ()); (* false *)
+Kernel.feedback "%B" (Eva.Analysis.is_computed ()); (* false *)
\end{ocamlcode}
As the value analysis has been automatically reset when setting the entry point,
the above code outputs
@@ -2548,7 +2548,7 @@ let compute_info (kf,vi) = ...
let memoize s =
try Stmt.Hashtbl.find state s
with Not_found -> Stmt.Hashtbl.add state s (compute_info s)
-let run () = ... !Db.Value.compute (); ... memoize some_stmt ...
+let run () = ... Eva.Analysis.compute (); ... memoize some_stmt ...
\end{ocamlcode}
However, if one puts this code inside \framac, it does not work because this
@@ -2570,7 +2570,7 @@ module State =
end)
let compute_info (kf,vi) = ...
let memoize = State.memo compute_info
-let run () = ... !Db.Value.compute (); ... memoize some_stmt ...
+let run () = ... Eva.Analysis.compute (); ... memoize some_stmt ...
\end{ocamlcode}
A quick look on this code shows that the declaration of the state itself is more
complicated (it uses a functor application) but its use is
@@ -2870,14 +2870,14 @@ value analysis has never been computed previously)
\scodeidx{Project}{IOError}
\begin{ocamlcode}
let print_computed () =
- Kernel.feedback "%B" (Db.Value.is_computed ())
+ Kernel.feedback "%B" (Eva.Analysis.is_computed ())
in
print_computed (); (* false *)
let old = Project.current () in
try
let foo = Project.load ~name:"foo" "foo.sav" in
Project.set_current foo;
- !Db.Value.compute ();
+ Eva.Analysis.compute ();
print_computed (); (* true *)
Project.set_current old;
print_computed () (* false *)
@@ -2913,13 +2913,13 @@ The following code is equivalent to the one given in
Example~\ref{ex:set_current}.
\begin{ocamlcode}
let print_computed () =
- Value_parameters.feedback "%B" (Db.Value.is_computed ())
+ Value_parameters.feedback "%B" (Eva.Analysis.is_computed ())
in
print_computed (); (* false *)
try
let foo = Project.load ~name:"foo" "foo.sav" in
Project.on foo
- (fun () -> !Db.Value.compute (); print_computed () (* true *)) ();
+ (fun () -> Eva.Analysis.compute (); print_computed () (* true *)) ();
print_computed () (* false *)
with Project.IOError _ ->
exit 1
diff --git a/doc/developer/check_api/run.oracle b/doc/developer/check_api/run.oracle
index 769847618c69cf2f9ca6f482711374dd559b3953..c5b9bea960a39741875927a46cfaee4c321bb3ec 100644
--- a/doc/developer/check_api/run.oracle
+++ b/doc/developer/check_api/run.oracle
@@ -96,7 +96,7 @@ Logic_utils.expr_to_term/cast:bool -> Cil_types.exp -> Cil_types.term/translates
Journal/(string -> string) Pervasives.refend /Journalization of functions./
Cil.cilVisitor.vstmt/Cil_types.stmt -> Cil_types.stmt Cil.visitAction/Control-flow statement. The default DoChildren action does not create a new statement when the components change. Instead it updates the contents of the original statement. This is done to preserve the sharing with Goto and Case statements that point to the original statement. If you use the ChangeTo action then you should take care of preserving that sharing yourself./
Cil.get_varinfo/Cil.visitor_behavior -> Cil_types.varinfo -> Cil_types.varinfo/retrieve the representative of a given varinfo in the current state of the visitor/
-Db.Value.is_computed/unit -> bool/Return true iff the value analysis has been done./
+Eva.Analysis.is_computed/unit -> bool/Return true iff the value analysis has been done./
Kernel.Unicode/('a -> 'b) -> 'a -> 'bend /Behavior of option "-unicode"./
Design.register_extension/(Design.main_window_extension_points -> unit) -> unit/Register an extension to the main GUI. It will be invoked at initialization time./
Cil_types.global/ | GType of Cil_types.typeinfo * Cil_types.location | GCompTag of Cil_types.compinfo * Cil_types.location | GCompTagDecl of Cil_types.compinfo * Cil_types.location | GEnumTag of Cil_types.enuminfo * Cil_types.location | GEnumTagDecl of Cil_types.enuminfo * Cil_types.location | GVarDecl of Cil_types.varinfo * Cil_types.location | GFunDecl of Cil_types.funspec * Cil_types.varinfo * Cil_types.location | GVar of Cil_types.varinfo * Cil_types.initinfo * Cil_types.location | GFun of Cil_types.fundec * Cil_types.location | GAsm of string * Cil_types.location | GPragma of Cil_types.attribute * Cil_types.location | GText of string | GAnnot of Cil_types.global_annotation * Cil_types.location/The main type for representing global declarations and definitions. A list of these form a CIL file. The order of globals in the file is generally important./
diff --git a/doc/developer/tutorial/viewcfg/src/dump_function_memo_clear_cache.ml b/doc/developer/tutorial/viewcfg/src/dump_function_memo_clear_cache.ml
index 3a83c607bb9f1075517684d443f10c25305c122f..36eb30f11660c19bc89f3524067d71382e014733 100644
--- a/doc/developer/tutorial/viewcfg/src/dump_function_memo_clear_cache.ml
+++ b/doc/developer/tutorial/viewcfg/src/dump_function_memo_clear_cache.ml
@@ -1,5 +1,5 @@
let dump_function fundec fmt =
- if not (Value_is_computed.get ()) && Db.Value.is_computed () then begin
+ if not (Value_is_computed.get ()) && Eva.Analysis.is_computed () then begin
Value_is_computed.set true;
let selection = State_selection.with_dependencies Cfg_graph_state.self in
Project.clear ~selection ();
diff --git a/doc/developer/tutorial/viewcfg/src/print_cfg_vstmt_aux_value.ml b/doc/developer/tutorial/viewcfg/src/print_cfg_vstmt_aux_value.ml
index 04446722a1f84abc19e1553058e7cc6f4ad2a5f8..67038d53098490e5c6d7b14991dac834b5b9e9a9 100644
--- a/doc/developer/tutorial/viewcfg/src/print_cfg_vstmt_aux_value.ml
+++ b/doc/developer/tutorial/viewcfg/src/print_cfg_vstmt_aux_value.ml
@@ -1,6 +1,6 @@
method! vstmt_aux s =
let color =
- if Db.Value.is_computed () then
+ if Eva.Analysis.is_computed () then
let state = Db.Value.get_stmt_state s in
let reachable = Db.Value.is_reachable state in
if reachable then "fillcolor=\"#ccffcc\" style=filled"
diff --git a/doc/training/developer/project.tex b/doc/training/developer/project.tex
index 98e08c503c07304da355bff6274bb29fbcde8398..8af2d2bceb399a059fc13eeb0438d6119316513c 100644
--- a/doc/training/developer/project.tex
+++ b/doc/training/developer/project.tex
@@ -175,7 +175,7 @@ let main () =
~select_annot:false
~select_slice_pragma:false
in
- Project.on p !Db.Value.compute ()
+ Project.on p Eva.Analysis.compute ()
\end{ocamlcode}
\end{itemize}
diff --git a/doc/training/developer/sources/basic_script.ml b/doc/training/developer/sources/basic_script.ml
index a9160149a1cbdab32d79dd1d34a89a53c04ff4b1..fd83c661bb190de5faf19f44fb978f59641aa548 100644
--- a/doc/training/developer/sources/basic_script.ml
+++ b/doc/training/developer/sources/basic_script.ml
@@ -10,7 +10,7 @@ let run f () =
incr nb_entry_points;
Kernel.MainFunction.set f;
Kernel.LibEntry.on ();
- !Db.Value.compute ()
+ Eva.Analysis.compute ()
(*# Main driver function*)
let all_entry_points () =
diff --git a/doc/training/developer/sources/const_violation.ml b/doc/training/developer/sources/const_violation.ml
index e057b7fbf7701f7492ff6aebc14db153cfec0c57..2eadb5524debd6e35c3ca20913df90252636c07a 100644
--- a/doc/training/developer/sources/const_violation.ml
+++ b/doc/training/developer/sources/const_violation.ml
@@ -3,7 +3,7 @@ let run () =
let glob = Globals.Vars.find_from_astinfo "Glob" Cil_types.VGlobal in
let glob_expr = Cil.evar ~loc:Cil_datatype.Location.unknown glob in
let main = Globals.Functions.find_by_name "main" in
- let () = !Db.Value.compute () in
+ let () = Eva.Analysis.compute () in
let init_stmt = Kernel_function.find_first_stmt main in
let init_state = Db.Value.get_stmt_state init_stmt in
let end_stmt = Kernel_function.find_return main in