From e85ce72eacbe745b5b7f9a794ad6a2cb628830ae Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Mon, 7 Feb 2022 16:51:46 +0100
Subject: [PATCH] [Doc] Update wrt the new Eva API
---
doc/developer/advance.tex | 18 +++++++++---------
doc/developer/check_api/run.oracle | 2 +-
.../src/dump_function_memo_clear_cache.ml | 2 +-
.../viewcfg/src/print_cfg_vstmt_aux_value.ml | 2 +-
doc/training/developer/project.tex | 2 +-
doc/training/developer/sources/basic_script.ml | 2 +-
.../developer/sources/const_violation.ml | 2 +-
7 files changed, 15 insertions(+), 15 deletions(-)
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 508230d7c8c..906403ec31d 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 769847618c6..c5b9bea960a 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 3a83c607bb9..36eb30f1166 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 04446722a1f..67038d53098 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 98e08c503c0..8af2d2bceb3 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 a9160149a1c..fd83c661bb1 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 e057b7fbf77..2eadb5524de 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
--
GitLab