diff --git a/bin/migration_scripts/nickel2copper.sh b/bin/migration_scripts/nickel2copper.sh
new file mode 100755
index 0000000000000000000000000000000000000000..ca68ca2502c4ee30c4ef5dae9e003a44ed787473
--- /dev/null
+++ b/bin/migration_scripts/nickel2copper.sh
@@ -0,0 +1,173 @@
+#!/bin/bash
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2023 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+#
+# Converts a Frama-C plugin from Frama-C 28 Nickel to Frama-C 29 Copper,
+# on a best-efforts basis (no guarantee that the result is fully compatible).
+#
+# known missing features:
+# - doesn't follow symbolic links to directories
+
+DIR=
+
+# verbose on by default
+VERBOSE="v"
+
+# test once if sed supports -i (BSD/macOS does not)
+SED_HAS_I=$(sed --help 2>/dev/null | grep '\-i' 2>/dev/null)
+
+# [sedi file expressions] runs 'sed -i expressions' on the specified file;
+# if '-i' is not supported, creates a temporary file and overwrites the
+# original, like '-i' does.
+sedi ()
+{
+ file="$1"
+ shift
+ if [ -n "$SED_HAS_I" ]; then
+ sed -i "$@" "$file"
+ else
+ # option '-i' is not recognized by sed: use a tmp file
+ new_temp=`mktemp /tmp/frama-c.XXXXXXX` || exit 1
+ sed "$@" "$file" > "$new_temp"
+ mv -f "$new_temp" "$file"
+ fi
+}
+
+dirs ()
+{
+ if [ -z "$DIR" ]; then
+ DIR=.
+ fi
+}
+
+# [safe_goto d1 d2 cmd] goes to d1, runs cmd, and returns to d2
+safe_goto ()
+{
+ dir="$1"
+ cd "$dir"
+ $3
+ cd "$2"
+}
+
+goto ()
+{
+ if [ -d "$1" ]; then
+ safe_goto "$1" "$2" "$3"
+ else
+ echo "Directory '$1' does not exist. Omitted."
+ fi
+}
+
+process_file ()
+{
+ file="$1"
+ if [ "$VERBOSE" ]; then
+ echo "Processing file $file"
+ fi
+ sedi "$file" \
+ -e 's/Db\.on_progress/Async.on_progress/g' \
+ -e 's/Db\.off_progress/Async.off_progress/g' \
+ -e 's/Db\.while_progress/Async.while_progress/g' \
+ -e 's/Db\.with_progress/Async.with_progress/g' \
+ -e 's/Db\.flush/Async.flush/g' \
+ -e 's/Db\.yield/Async.yield/g' \
+ -e 's/Db\.sleep/Async.sleep/g' \
+ -e 's/Db\.cancel/Async.cancel/g' \
+ -e 's/Db\.daemon/Async.daemon/g' \
+ -e 's/Db\.Main/Boot.Main/g'
+ # this line left empty on purpose
+}
+
+apply_one_dir ()
+{
+ if [ "$VERBOSE" ]; then
+ echo "Processing directory `pwd`"
+ fi
+ for f in $(find . -maxdepth 1 -type f -name "*.ml*" 2> /dev/null); do
+ process_file "$f"
+ done
+}
+
+apply_recursively ()
+{
+ apply_one_dir
+ while IFS= read -r -d $'\0' d; do
+ if [ "$d" = "." ]; then
+ continue
+ fi
+ safe_goto "$d" .. apply_recursively
+ done < <(find . -maxdepth 1 -type d -print0)
+}
+
+applying_to_list ()
+{
+ dirs
+ tmpdir=`pwd`
+ for d in $DIR; do
+ goto "$d" "$tmpdir" "$1"
+ done
+}
+
+help ()
+{
+ echo "Usage: $0 [options | directories]
+
+Options are:
+ -r | --recursive Check subdirectories recursively
+ -h | --help Display help message
+ -q | --quiet Quiet mode (i.e. non-verbose mode)
+ -v | --verbose Verbose mode (default)"
+ exit 0
+}
+
+error ()
+{
+ echo "$1.
+Do \"$0 -h\" for help."
+ exit 1
+}
+
+FN="apply_one_dir"
+
+parse_arg ()
+{
+ case $1 in
+ -r | --recursive) FN="apply_recursively";;
+ -h | -help ) help; exit 0;;
+ -q | --quiet ) VERBOSE=;;
+ -v | --verbose ) VERBOSE="v";;
+ -* ) error "Invalid option $1";;
+ * ) DIR="$DIR $1";;
+ esac
+}
+
+cmd_line ()
+{
+ for s in "$@"; do
+ parse_arg "$s"
+ done
+ applying_to_list $FN
+}
+
+cmd_line "$@"
+exit 0
diff --git a/dev/size_states.ml b/dev/size_states.ml
index ad62726e2b8427127497eea54cc0526c00ae650b..020f68ab4c2b4c7abe1cd1f60821069c1f91f7d8 100644
--- a/dev/size_states.ml
+++ b/dev/size_states.ml
@@ -109,4 +109,4 @@ let all_sizes () =
Kernel.result "## Sizes ##@.%a"
(Pretty_utils.pp_list ~pre:"@[<v>" ~suf:"@]" ~sep:"@ " pp) res
-let () = Db.Main.extend all_sizes
+let () = Boot.Main.extend all_sizes
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 54830c6fdf0b5bc891722028c19252fe59155e06..8b2f40e98002ef86ee6ff19b3815ff0a2aa7001b 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -95,20 +95,11 @@ via \verb|ocamlfind|.
\subsection{Declaring dependencies}
-Optional dependencies can be detected and disabled in different ways:
-
-\begin{itemize}
-\item If the module is dynamically accessible via \verb|Db| (see
- Section~\ref{adv:static-registration} for more details), the detection
- can be done directly in OCaml and requires no special handling in the
- \verb|dune| file;
-\item Otherwise, you can define two versions of the implementation
- (both implementing the same interface), in two different files.
- One of these files will use the required module, while the other will
- implement a dummy version without it.
- The \verb|select| notation from the \verb|library| stanza allows telling
- Dune which file to compile.
-\end{itemize}
+For optional dependencies, you can define two versions of the implementation
+(both implementing the same interface), in two different files. One of these
+files will use the required module, while the other will implement a dummy
+version without it. The \verb|select| notation from the \verb|library| stanza
+allows telling Dune which file to compile.
Here is an example of \verb|select| from the \textsf{Aoraï} plug-in,
which defines an optional dependency on the \textsf{Eva} plug-in:
@@ -1145,7 +1136,7 @@ plug-in general services.
\begin{example}
A minimal example of a plug-in using the logging services:
\scodeidx{Plugin}{Register}
-\sscodeidx{Db}{Main}{extend}
+\sscodeidx{Boot}{Main}{extend}
\begin{ocamlcode}
module Self = Plugin.Register
(struct
@@ -1164,7 +1155,7 @@ let run () =
Self.debug ~level:1 "If you read this, %a." pp_dg 1;
Self.debug ~level:3 "If you read this, %a." pp_dg 3;
-let () = Db.Main.extend run ()
+let () = Boot.Main.extend run ()
\end{ocamlcode}
\end{example}
@@ -1896,10 +1887,8 @@ Actually, there are three different ways, but the recommended one is through a
\texttt{.mli} file.
Section~\ref{adv:standard-registration} indicates how to register and access a
-plug-in through a \texttt{.mli} file. Section~\ref{adv:static-registration}
-indicates how to register and access a \emph{kernel-integrated} plug-in while
-Section~\ref{adv:dynamic-registration} details how to register and access a
-\emph{standard} plug-in.
+plug-in through a \texttt{.mli} file. Section~\ref{adv:dynamic-registration}
+details how to register and access a \emph{standard} plug-in.
\subsection{Registration through a \texttt{.mli} File}
\label{adv:standard-registration}
@@ -1916,96 +1905,6 @@ contain in its \texttt{libraries} clause \texttt{frama-c-a.core}
(see Section~\ref{adv:dependencies}), or more generally the \texttt{public\_name}
under which \texttt{A} is declared.
-\subsection{Kernel-integrated Registration and Access}
-\label{adv:static-registration}
-
-\begin{target}kernel-integrated plug-in developers.\end{target}
-
-\begin{prereq}
- Accepting to modify the \framac kernel. Otherwise, you can still register
- your plug-in as any standard plug-in (see
- Section~\ref{adv:dynamic-registration} for details).
-\end{prereq}
-
-\begin{important}
-This registration method is deprecated and only kept here for historical purpose.
-No new entry point should be added in the \texttt{Db}, which will be removed in
-a future version of \framac.
-\end{important}
-
-A database, called \texttt{Db}\codeidxdef{Db} (in directory
-\texttt{src/kernel\_services/plugin\_entry\_points}), groups together
-the API of all kernel-integrated
-plug-ins. So it permits easy plug-in collaborations. Each kernel-integrated
-plug-in is only visible through \texttt{Db}. For example, if a plug-in
-\texttt{A} wants to know the results of another plug-in \texttt{B}, it uses the
-part of \texttt{Db} corresponding to \texttt{B}. A consequence of this design
-is that each plug-in has to register in \texttt{Db} by setting a function
-pointer to the right value in order to be usable from others plug-ins.
-
-\begin{example}
-Plug-in \texttt{Impact} registers function \texttt{compute\_pragmas} in the
-following way.
-
-\listingname{src/plugins/impact/register.ml}
-\scodeidx{Db}{Impact.compute\_pragmas}
-\begin{ocamlcode}
-let compute_pragmas () = ...
-let () = Db.Impact.compute_pragmas := compute_pragmas
-\end{ocamlcode}
-Thus each developer who wants to use this function calls it by pointer
-dereferencing like this.
-\begin{ocamlcode}
-let () = !Db.Impact.compute_pragmas ()
-\end{ocamlcode}
-\end{example}
-
-If a kernel-integrated plug-in has to export some datatypes usable by other
-plug-ins, such datatypes have to be visible from module
-\texttt{Db}\codeidx{Db}. Thus they cannot be declared in the plug-in
-implementation itself like any other plug-in declaration because postponed type
-declarations are not possible in \ocaml.
-
-Such datatypes are called \emph{plug-in types}\index{Plug-in!Types|bfit}. The
-solution is to put these plug-ins types in some files linked before
-\texttt{Db}; hence you have to put them in another directory than the plug-in
-directory. The best way is to create a directory dedicated to types.
-
-\begin{convention}
- The suggested name for this directory is
- \texttt{$p$\_types}\index{plug-in\_types@\texttt{$plugin$\_types}|bfit} for a
- plug-in $p$.
-\end{convention}
-
-\begin{example}
-Suppose you are writing a plug-in \texttt{p} which exports a specific type
-\texttt{t} corresponding to the result of the plug-in analysis. The standard way
-to proceed is the following.
-
-\listingname{src/plugins/p\_types/p\_types.mli}
-\begin{ocamlcode}
-type t = ...
-\end{ocamlcode}
-
-\listingname{src/kernel\_services/plugin\_entry\_points/db.mli}
-\begin{ocamlcode}
-module P : sig
- val run_and_get: (unit -> P_types.t) ref
- (** Run plugin analysis (if it was never launched before).
- @return result of the analysis. *)
-end
-\end{ocamlcode}
-\end{example}
-
-This design choice has a side effect : it reveals exported types.
-You can always hide them using a module to encapsulate the types
-(and provide corresponding getters and setters to access them).
-
-At this point, part of the plug-in code is outside the plug-in
-implementation. This code should be linked before \texttt{Db}
-\codeidx{Db}\footnote{A direct consequence is that you cannot use the whole
-\framac functionalities, such as module \texttt{Db}, inside this code.}.
-
\subsection{Dynamic Registration and Access}
\label{adv:dynamic-registration}
\index{Plug-in!Registration}\index{Plug-in!Access}\index{Plug-in!API}
@@ -2017,11 +1916,8 @@ Dynamic registration is obsolete. Newer development should favor exporting
a static API, as explained in Section~\ref{adv:standard-registration}.
\end{important}
-Registration of kernel-integrated plug-ins requires to modify module
-\texttt{Db}\codeidx{Db} which belongs to the \framac kernel. Such a
-modification is not possible for standard plug-ins which are fully independent
-of \framac. Consequently, the \framac kernel provides another way for
-registering a plug-in through the module \texttt{Dynamic}\codeidxdef{Dynamic}.
+The \framac kernel provides another way for registering a plug-in through the
+module \texttt{Dynamic}\codeidxdef{Dynamic}.
In short, you have to use the function
\texttt{Dynamic.register}\scodeidxdef{Dynamic}{register} in order to register a
@@ -2312,7 +2208,7 @@ information attached to statements would result in the following piece of code.
\codeidx{Kernel\_function}\sscodeidx{Datatype}{Ty}{t}
\scodeidx{Cil\_types}{varinfo}
\scodeidx{Cil\_datatype}{Stmt}\sscodeidx{Datatype}{S\_with\_collections}{Hashtbl}
-\sscodeidx{Db}{Value}{compute}
+\sscodeidx{Eva}{Analysis}{compute}
\begin{ocamlcode}
open Cil_datatype
type info = Kernel_function.t * Cil_types.varinfo
@@ -2330,8 +2226,8 @@ the disk\index{Saving} and its value is never changed when setting the current
project to a new one. For this purpose, one has to transform the above code into
the following one. \scodeidx{Cil\_state\_builder}{Stmt\_hashtbl}
\scodeidx{Datatype}{Pair} \codeidx{Kernel\_function}
-\scodeidx{Cil\_datatype}{Varinfo} \sscodeidx{Db}{Value}{self}
-\sscodeidx{Db}{Value}{compute} \codeidx{memo}
+\scodeidx{Cil\_datatype}{Varinfo} \sscodeidx{Eva}{Analysis}{self}
+\sscodeidx{Eva}{Analysis}{compute} \codeidx{memo}
\begin{ocamlcode}
module State =
Cil_state_builder.Stmt_hashtbl
@@ -2398,32 +2294,13 @@ the right way to do this is the use of the function
Section~\ref{adv:init} for advanced explanation about the way \framac is
initialized).
\begin{example}
-Plug-in \texttt{from}\index{From} puts a reference to its state kind in the
-following way. This reference is initialized at module initialization time.
-
-\listingname{src/kernel\_services/plugin\_entry\_points/db.mli}
-\codeidx{State}
-\scodeidx{State}{dummy}
-\scodeidx{Db}{From.self}
-\begin{ocamlcode}
-module From = struct
- ...
- val self: State.t ref
-end
-\end{ocamlcode}
-
-\listingname{src/kernel\_services/plugin\_entry\_points/db.ml}
-\begin{ocamlcode}
-module From = struct
- ...
- val self = ref State.dummy (* postponed *)
-end
-\end{ocamlcode}
+Plug-in \texttt{from}\index{From} creates a \texttt{State}\index{State} exposed
+via its API.
-\scodeidx{Kernel\_function}{Make\_Table}
-\sscodeidx{Db}{Value}{self}
-\scodeidx{Db}{From.self}
+\noindent
\listingname{src/plugins/from/functionwise.ml}
+\scodeidx{Kernel\_function}{Make\_Table}
+\sscodeidx{Eva}{Analysis}{self}
\begin{ocamlcode}
module Tbl =
Kernel_function.Make_Table
@@ -2433,34 +2310,40 @@ module Tbl =
let size = 97
let dependencies = [ Eva.Analysis.self ]
end)
-let () =
- (* performed at module initialization runtime. *)
- Db.From.self := Tbl.self
+let self = Tbl.self
+\end{ocamlcode}
+\listingname{src/plugins/from/from.ml}
+\begin{ocamlcode}
+let self = Functionwise.self
\end{ocamlcode}
+
Plug-in \texttt{pdg}\index{Plug-in!Pdg|see{Pdg}}\index{Pdg} uses
\texttt{from}\index{From} for computing its own internal state. So it declares
this dependency as follows.
-\listingname{src/plugins/pdg/register.ml}
+\noindent\listingname{src/plugins/pdg/pdg\_tbl.ml}
\scodeidx{Kernel\_function}{Make\_Table}
-\scodeidx{State\_dependency\_graph}{S.add\_codependencies}
-\scodeidx{Cmdline}{run\_after\_extended\_stage}
\begin{ocamlcode}
module Tbl =
Kernel_function.Make_Table
(PdgTypes.Pdg)
(struct
let name = "Pdg.State"
- let dependencies = [] (* postponed because !Db.From.self may
- not exist yet *)
+ let dependencies = [] (* postponed because From.self may not exist yet *)
let size = 97
end)
+let self = Tbl.self
+\end{ocamlcode}
+\listingname{src/plugins/pdg/register.ml}
+\scodeidx{State\_dependency\_graph}{S.add\_codependencies}
+\scodeidx{Cmdline}{run\_after\_extended\_stage}
+\begin{ocamlcode}
let () =
Cmdline.run_after_extended_stage
(fun () ->
State_dependency_graph.add_codependencies
- ~onto:Tbl.self
- [ !Db.From.self ])
+ ~onto:Pdg_tbl.self
+ [ From.self ])
\end{ocamlcode}
\end{example}
@@ -2635,11 +2518,11 @@ Project.save "foo.sav"
\end{ocamlcode}
In a new \framac session, executing the following lines of code (assuming the
value analysis has never been computed previously)
-\sscodeidx{Db}{Value}{is\_computed}
+\sscodeidx{Eva}{Analysis}{is\_computed}
\scodeidx{Project}{current}
\scodeidx{Project}{load}
\scodeidx{Project}{set\_current}
-\sscodeidx{Db}{Value}{compute}
+\sscodeidx{Eva}{Analysis}{compute}
\scodeidx{Project}{IOError}
\begin{ocamlcode}
let print_computed () =
@@ -2720,7 +2603,7 @@ consistently handle state dependencies\index{State!Dependency}.
its dependencies in the current project.\index{State!Cleaning}
\scodeidx{Project}{clear}
\scodeidx{State\_selection}{with\_dependencies}
- \sscodeidx{Db}{Value}{self}
+ \sscodeidx{Eva}{Analysis}{self}
\begin{ocamlcode}
let selection = State_selection.with_dependencies Eva.Analysis.self in
Project.clear ~selection ()
@@ -2983,7 +2866,7 @@ ones.
From the plug-in developer point of view, the hooks are registered by
calling the \texttt{run\_after\_$xxx$\_stage} routines in
\texttt{Cmdline}\codeidx{Cmdline} module and \texttt{extend} routine
-in the \texttt{Db.Main}\sscodeidx{Db}{Main}{extend} module.
+in the \texttt{Boot.Main}\sscodeidx{Boot}{Main}{extend} module.
The initialization phases and stages of \framac are described below, in
their execution order.
@@ -3150,7 +3033,7 @@ their execution order.
\item \textbf{The Main Stage:} this is the step where plug-ins actually run
their main entry points registered through
- \texttt{Db.Main.extend}\sscodeidx{Db}{Main}{extend}. For all intents and purposes, you should consider
+ \texttt{Boot.Main.extend}\sscodeidx{Boot}{Main}{extend}. For all intents and purposes, you should consider
that this stage is the one where these hooks are executed.
\end{enumerate}
@@ -3754,7 +3637,7 @@ division in the program, stating that the divisor is not zero:
\sscodeidx{Cil}{visitAction}{DoChildren}
\scodeidx{File}{create\_project\_from\_visitor}
\scodeidx{Annotations}{add\_assert}
-\sscodeidx{Db}{Main}{extend}
+\sscodeidx{Boot}{Main}{extend}
\sscodeidx{Visitor\_behavior}{Get}{stmt}
\sscodeidx{Visitor\_behavior}{Get}{kernel\_function}
\sscodeidx{Cil}{cilVisitor}{behavior}
@@ -4263,7 +4146,7 @@ points. The documentation of the class type
source documentation (see Section~\ref{tut2:doc}).
Besides time-consuming computations have to call the function
-\texttt{Db.yield}\scodeidx{Db}{yield} from time to time in order to keep the GUI reactive.
+\texttt{Async.yield}\scodeidx{Async}{yield} from time to time in order to keep the GUI reactive.
%Mainly that's all!
The GUI implementation uses
diff --git a/doc/developer/architecture.tex b/doc/developer/architecture.tex
index d1de7b6f1945e40f3c2ea63fde9aaae929508afb..8a942667de7332adddf4a4a32dc27aa57651395f 100644
--- a/doc/developer/architecture.tex
+++ b/doc/developer/architecture.tex
@@ -196,12 +196,10 @@ has to be registered through \texttt{Plugin.Register}\scodeidx{Plugin}{Register}
a plug-in $p$ can use a list of plug-ins $p_1$, \dots, $p_n$ and
conversely. Mutual dependences between plug-ins are even possible. If a plug-in
is designed to be used by another plug-in, it has to register its API either by
-providing a \texttt{.mli} file, or through modules
-\texttt{Dynamic}\codeidx{Dynamic} or \texttt{Db}\codeidx{Db}. The first method
+providing a \texttt{.mli} file or through module
+\texttt{Dynamic}\codeidx{Dynamic}. The first method
is the preferred one, the second one (through module \texttt{Dynamic}) is the
-only possible one to define mutually dependent plug-ins while the third one
-(through module \texttt{Db}) is now fully deprecated even if most of the older
-\framac plug-ins are still defined this way.
+only possible one to define mutually dependent plug-ins.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -271,12 +269,12 @@ with the \framac kernel or other plug-ins.
Next, \framac provides predefined ways to visit the ASTs, in particular through
object-oriented visitors defined in directory
-\texttt{src/kernel\_services/visitors} (see Section~\ref{adv:visitors}).
+\texttt{src/kernel\_services/visitors} (see Section~\ref{adv:visitors}).
Some predefined analyzers, such as a multiple generic dataflow analysis
are provided in directory \texttt{src/kernel\_services/analysis}, while some
predefined program transformation, such as cloning a function, are provided in
directory \texttt{src/kernel\_services/ast\_transformations}.
-Finally, \framac provides an abstract interpretation
+Finally, \framac provides an abstract interpretation
toolbox\index{Abstract Interpretation}
with various lattices in directory \texttt{abstract\_interp}.
diff --git a/doc/developer/changes.tex b/doc/developer/changes.tex
index d0ee85277359173857a81b900decd4ab713eb009..6395dc53dcf44833ff1413475f562443346dfa9e 100644
--- a/doc/developer/changes.tex
+++ b/doc/developer/changes.tex
@@ -5,7 +5,17 @@
This chapter summarizes the major changes in this documentation between each
\framac release, from newest to oldest.
-%\section*{Frama-C+dev}
+\section*{Frama-C+dev}
+\begin{itemize}
+\item There is no more \texttt{Db} module:
+ \begin{itemize}
+ \item Whole document: \texttt{Db.Main.extend} is now \texttt{Boot.Main.extend}
+ \item \textbf{Declaring dependencies}: removed section about \texttt{Db}
+ \item \textbf{Kernel-integrated Registration and Access}: removed section
+ \item \textbf{Registering a New State}: adapted example on postponed dependencies
+ \item \textbf{GUI Extension}: \texttt{Db.yield} is now \texttt{Async.yield}
+ \end{itemize}
+\end{itemize}
\section*{27.0 (Cobalt)}
\begin{itemize}
diff --git a/doc/developer/check_api/run.oracle b/doc/developer/check_api/run.oracle
index 4aef5e8b54bf2467c1b89110be6cbb4dbbfea258..e62628e21c6c5eab02924e3f4c703991afe8a447 100644
--- a/doc/developer/check_api/run.oracle
+++ b/doc/developer/check_api/run.oracle
@@ -24,10 +24,9 @@ Cil_types.stmtkind.UnspecifiedSequence/ of (Cil_types.stmt * Cil_types.lval list
Cil_types.stmtkind.Break/ of Cil_types.location/A break to the end of the nearest enclosing Loop or Switch./
Datatype.unit/unit Type.t/Add sets, maps and hashtables modules to an existing datatype, provided the equal, compare and hash functions are not Datatype.undefined./
Globals/(Cil_types.stmt -> Cil_types.kernel_function) Stdlib.refend /Operations on globals./
-Db.Main/(unit -> unit) Stdlib.refend /Frama-C main interface./
+Boot.Main/(unit -> unit) Stdlib.refend /Frama-C main interface./
Visitor_behavior.Get/Visitor_behavior.Get/Get operations on behaviors, allows to get the representative of an AST element in the current state of the visitor. Get.ast_element vis e with e of type ast_element gets the representative of e in vis. For example for Cil_types.varinfo: Get.varinfo vis vi./
Visitor_behavior.Set/Visitor_behavior.Set/Set operations on behaviors, allows to change the representative of a given AST element in the current state of the visitor. Use with care (i.e. makes sure that the old one is not referenced anywhere in the AST, or sharing will be lost). Set.ast_element vis e s with e and s of type ast_element changes the representative of e to s in vis. For example, for Cil_types.varinfo: Set.varinfo vis vi new_representative./
-Db.Properties/Emitter.t -> Cil_types.kernel_function -> Cil_types.stmt -> string -> unitend /Dealing with logical properties./
Visitor_behavior.Reset/Visitor_behavior.t -> unitend /Reset operations on behaviors, allows to reset the tables associated to a given kind of AST elements. If you use fresh instances of visitor for each round of transformation, you should not need this module. In place modifications do not need this at all. Reset.ast_element vis resets the tables associated to the considered type of AST elements in vis. For example for Cil_types.varinfo: Reset.varinfo vis./
Cil_types.enuminfo//Information about an enumeration./
Datatype.Polymorphic/((Project_skeleton.t -> bool) -> 'a -> bool) -> (Project_skeleton.t -> bool) -> 'a Datatype.t -> bool end ) -> Datatype.Polymorphic with type 'a poly = 'a P.t/Functor for polymorphic types with only 1 type variable./
@@ -41,18 +40,16 @@ Cmdline.stage.Extended//The stage where plug-ins are loaded. It is also the
Pretty_source.localizable.PVDecl/ of (Cil_types.kernel_function option * Cil_types.kinstr * Cil_types.varinfo)/Declaration and definition of variables and function. Check the type of the varinfo to distinguish between the various possibilities. If the varinfo is a global or a local, the kernel_function is the one in which the variable is declared. The kinstr argument is given for local variables with an explicit initializer./
Locations.Location/Datatype.S with type t = location/Misc/
Parameter_sig.Builder.Int/int end ) -> Parameter_sig.Int/To be used by the plugin to output the results of the option in a controlled way. See set_output_dependencies details./
-Db.Main.extend/(unit -> unit) -> unit/Register a function to be called by the Frama-C main entry point./
+Boot.Main.extend/(unit -> unit) -> unit/Register a function to be called by the Frama-C main entry point./
Annotations/State.tend /Annotations in the AST. The AST should be computed before calling functions of this module./
Cmdline.run_after_exiting_stage/(unit -> Cmdline.exit) -> unit/Register an action to be executed at the end of the exiting stage. The guarded action must finish by exit n./
Cil.cilVisitor.vvrbl/Cil_types.varinfo -> Cil_types.varinfo Cil.visitAction/Invoked on each variable use. Here only the SkipChildren and ChangeTo actions make sense since there are no subtrees. Note that the type and attributes of the variable are not traversed for a variable use./
Cil_types.varinfo//Information about a variable./
Lmap_bitwise/functor (V : Lmap_bitwise.With_default ) -> Lmap_bitwise.Location_map_bitwise with type v = V.tend /Functors making map indexed by zone./
Cil.cilVisitor.behavior/Visitor_behavior.t/the kind of behavior expected for the behavior./
-Eva.Analysis.compute/unit -> unit/Computes the Eva analysis, if not already computed, using the entry point of the current project. You may set it with Globals.set_entry_point. raised exceptions: , if the entry point is incorrect, if some arguments are specified for the entry point using Db.Value.fun_set_args, and an incorrect number of them is given./
Datatype.Serializable_undefined/Datatype.Undefined/Same as Datatype.Undefined, but the type is supposed to be marshallable by the standard OCaml way (in particular, no hash-consing or projects inside the type)./
Log.Messages.feedback/?ontty:Log.ontty -> ?level:int -> ?dkey:Log.Messages.category -> 'a Log.pretty_printer/Progress and feedback. Level is tested against the verbosity level./
Log.set_echo/?plugin:string -> ?kind:Log.kind list -> bool -> unit/Turns echo on or off. Applies to all channel unless specified, and all kind of messages unless specified./
-Db.Value.self/State.t/Internal state of the value analysis from projects viewpoint./
Log.new_channel/string -> Log.channel/Send an event over the associated listeners./
Log.Messages.warning/?wkey:Log.Messages.warn_category -> 'a Log.pretty_printer/Hypothesis and restrictions./
Datatype.Undefined/Datatype.Undefined/Sub-signature of Datatype.S./
@@ -118,7 +115,6 @@ Log.Messages.logwith/(Log.event option -> 'b) -> ?wkey:Log.Messages.warn_categor
Logic_utils.expr_to_term/?coerce:bool -> Cil_types.exp -> Cil_types.term/Returns a logic term that has exactly the same semantics as the original C-expression. The type of the resulting term is determined by the ~coerce flag as follows:- when ~coerce:false is given (the default) the term has the same c-type as the original expression.- when ~coerce:true is given, if the original expression has an int or float type, then the returned term is coerced into the integer or real logic type, respectively. Remark: when the original expression is a comparison, it is evaluated as an int or an integer depending on the ~coerce flag. To obtain a boolean or predicate, use expr_to_boolean or expr_to_predicate instead./
Journal/(string -> Datatype.Filepath.t) Stdlib.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./
-Db.Value.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//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./
@@ -127,7 +123,6 @@ Datatype.func3/?label1:string * (unit -> 'a) option -> 'a Type.t -> ?label2:stri
Cmdline.stage.Loading//After Extended, the stage where a previous Frama-C internal states is restored (e.g. the one specified by -load or by running the journal)./
Cil.cilVisitor//A visitor interface for traversing CIL trees. Create instantiations of this type by specializing the class Cil.nopCilVisitor. Each of the specialized visiting functions can also call the queueInstr to specify that some instructions should be inserted before the current statement. Use syntax like self#queueInstr to call a method associated with the current object. Important Note for Frama-C Users: Unless you really know what you are doing, you should probably inherit from the Visitor.generic_frama_c_visitor instead of Cil.genericCilVisitor or Cil.nopCilVisitor/
Cil.lzero/?loc:Cil_types.location -> unit -> Cil_types.term/The constant logic term zero./
-Db.Value.is_reachable/Db.Value.state -> bool/add_formals_to_state state kf exps evaluates exps in state and binds them to the formal arguments of kf in the resulting state/
Cil_types.compinfo//The definition of a structure or union type. Use Cil.mkCompInfo to make one and use Cil.copyCompInfo to copy one (this ensures that a new key is assigned and that the fields have the right pointers to parents.)./
Cil_types.logic_type_info//Description of a logic type./
Cmdline.run_after_loading_stage/(unit -> unit) -> unit/Register an action to be executed at the end of the loading stage./
@@ -143,7 +138,6 @@ Cil_types.binop.Div////
Parameter_sig.Bool/Parameter_sig.Bool/Signature for a boolean parameter./
Cil_types.stmtkind.Instr/ of Cil_types.instr/An instruction that does not contain control flow. Control implicitly falls through./
Visitor.generic_frama_c_visitor/Visitor_behavior.t -> /Generic class that abstracts over frama_c_inplace and frama_c_copy./
-Db.Value.get_stmt_state/?after:bool -> Cil_types.stmt -> Db.Value.state/after is false by default./
Logic_typing.typing_context//Functions that can be called when type-checking an extension of ACSL./
Parameter_sig.Builder.False/functor (X : Parameter_sig.Input ) -> Parameter_sig.Bool/Set the boolean to false./
Cil.cilVisitor.vglob/Cil_types.global -> Cil_types.global list Cil.visitAction/Global (vars, types, etc.)/
@@ -203,7 +197,6 @@ Cil_types.stmt//Statements./
Cil.visitCilFileSameGlobals/Cil.cilVisitor -> Cil_types.file -> unit/A visitor for the whole file that does not *physically* change the globals (but maybe changes things inside the globals through side-effects). Use this function instead of Cil.visitCilFile whenever appropriate because it is more efficient for long files./
Datatype.S_with_collections/Datatype.S_with_collections/A datatype for a type t extended with predefined set, map and hashtbl over t./
Cmdline.run_after_extended_stage/(unit -> unit) -> unit/Register an action to be executed at the end of the extended stage./
-Db.Value.compute/(unit -> unit) Stdlib.ref/Compute the value analysis using the entry point of the current project. You may set it with Globals.set_entry_point. raised exceptions: , if the entry point is incorrect, if some arguments are specified for the entry point using Db.Value.fun_set_args, and an incorrect number of them is given./
Visitor_behavior.Get_orig/Visitor_behavior.Get/Get operations on behaviors, allows to get the original representative of an element of the new AST in the curent state of the visitor. Get_orig.ast_element vis new_e with new_e of type ast_element gets the original representative of new_e in vis. For example for Cil_types.varinfo: Get_orig.varinfo vis new_vi./
Cil_types.stmtkind.TryFinally/ of Cil_types.block * Cil_types.block * Cil_types.location/On MSVC we support structured exception handling. This is what you might expect. Control can get into the finally block either from the end of the body block, or if an exception is thrown./
Cil_types.logic_info//description of a logic function or predicate./
@@ -258,7 +251,7 @@ Cil_types.logic_var//description of a logic variable/
Cil_types.exp_node.BinOp/ of Cil_types.binop * Cil_types.exp * Cil_types.exp * Cil_types.typ/Binary operation. Includes the type of the result. The arithmetic conversions are made explicit for the arguments./
Log.log_channel/Log.channel -> ?kind:Log.kind -> 'a Log.pretty_printer/logging function to user-created channel./
Cil_types.stmtkind.Loop/ of Cil_types.code_annotation list * Cil_types.block * Cil_types.location * Cil_types.stmt option * Cil_types.stmt option/A while(1) loop. The termination test is implemented in the body of a loop using a Break statement. If Cfg.prepareCFG has been called, the first stmt option will point to the stmt containing the continue label for this loop and the second will point to the stmt containing the break label for this loop./
-Db.yield/(unit -> unit) Stdlib.ref/This function should be called from time to time by all analysers taking time. In GUI mode, this will make the interface reactive./
+Async.yield/(unit -> unit) Stdlib.ref/This function should be called from time to time by all analysers taking time. In GUI mode, this will make the interface reactive./
Kernel_function.get_definition/t -> Cil_types.fundec/Returns the list of static variables declared inside the function. raised exception: No_Definition./
Datatype.char/char Type.t//
Visitor_behavior.Get.stmt/Visitor_behavior.t -> Cil_types.stmt -> Cil_types.stmt/Fold operations on table of a given type of AST elements. Fold.ast_element vis f, folds f over each pair of ast_element registered in vis. The ast_element in the old AST is presented to f first (that is, f looks like: let f old_e new_e acc = .... For example for Cil_types.varinfo: Fold.varinfo vis (fun old_vi new_vi acc -> ... )./
@@ -284,9 +277,7 @@ Visitor_behavior.Get.kernel_function/Visitor_behavior.t -> Cil_types.kernel_func
Cmdline.stage.Configuring//The stage where all the parameters which were not already set may be modified to take into account cmdline options. Just after this stage, Frama-C will run the plug-in mains./
Acsl_extension.register_global/string -> ?preprocessor:Acsl_extension.extension_preprocessor -> Acsl_extension.extension_typer -> ?visitor:Acsl_extension.extension_visitor -> ?printer:Acsl_extension.extension_printer -> ?short_printer:Acsl_extension.extension_printer -> bool -> unit/Registers extension for global annotation. See register_behavior./
File.add_code_transformation_before_cleanup/?deps:(module Parameter_sig.S) list -> ?before:File.code_transformation_category list -> ?after:File.code_transformation_category list -> File.code_transformation_category -> (Cil_types.file -> unit) -> unit/add_code_transformation_before_cleanup name hook adds an hook in the corresponding category that will be called during the normalization of a linked file, before clean up and removal of temps and unused declarations. If this transformation involves changing statements of a function f, f must be flagged with File.must_recompute_cfg. The optional before (resp after) categories indicates that current transformation must be executed before (resp after) the corresponding ones, if they exist. In case of dependencies cycle, an arbitrary order will be chosen for the transformations involved in the cycle. The optional deps argument gives the list of options whose change (e.g. after a -then) will trigger the transformation over the already computed AST. If several transformations are triggered by the same option, their relative order is preserved. At this level, globals and ACSL annotations have not been registered./
-Db/end /Database in which static plugins are registered./
Cmdline.stage.Extending//Before loading plug-ins. Run only once./
-Analysis.compute/unit -> unit/Computes the Eva analysis, if not already computed, using the entry point of the current project. You may set it with Globals.set_entry_point. raised exceptions: , if the entry point is incorrect, if some arguments are specified for the entry point using Db.Value.fun_set_args, and an incorrect number of them is given./
Type.precedence.Basic//Normal precedence/
FCHashtbl/int -> int -> 'a -> intend /Extension of OCaml's Hashtbl module./
Cil_datatype.Fundec/Cil_datatype.S_with_collections_pretty with type t = fundec//
diff --git a/doc/developer/examples/populate_spec/populate.ml b/doc/developer/examples/populate_spec/populate.ml
index 9038698de7d93433908feafd913dbcf4e54507cc..3c6830100175cb5c8113e2731e20c9d196b6b9dc 100644
--- a/doc/developer/examples/populate_spec/populate.ml
+++ b/doc/developer/examples/populate_spec/populate.ml
@@ -72,4 +72,4 @@ let create_mode () =
frama-c. *)
let () = Cmdline.run_after_configuring_stage create_mode
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/examples/populate_spec/tests/example/oracle/populate.res.oracle b/doc/developer/examples/populate_spec/tests/example/oracle/populate.res.oracle
index e8857d4e7c2e88ee71895570d9e00f5557b89490..0d6deba1b497022a6df3304305b8bb51bdc973b9 100644
--- a/doc/developer/examples/populate_spec/tests/example/oracle/populate.res.oracle
+++ b/doc/developer/examples/populate_spec/tests/example/oracle/populate.res.oracle
@@ -1,6 +1,6 @@
Registering a new spec generation mode
[kernel] Parsing populate.c (with preprocessing)
-[kernel:annot:missing-spec] populate.c:13: Warning:
+[kernel:annot:missing-spec] populate.c:11: Warning:
Neither code nor explicit exits, assigns, requires, allocates and terminates for function f,
generating default clauses (some from the specification). See -generated-spec-* options for more info
/* Generated by Frama-C */
diff --git a/doc/developer/examples/syntactic_check/syntactic_check.ml b/doc/developer/examples/syntactic_check/syntactic_check.ml
index 604d1885603bcdec9502f303603e75d2be66b608..7d84275fba2ef2f6bb137ee5f8177f79066be563 100644
--- a/doc/developer/examples/syntactic_check/syntactic_check.ml
+++ b/doc/developer/examples/syntactic_check/syntactic_check.ml
@@ -64,4 +64,4 @@ let create_syntactic_check_project () =
ignore
(File.create_project_from_visitor "syntactic check" (new non_zero_divisor))
-let () = Db.Main.extend create_syntactic_check_project
+let () = Boot.Main.extend create_syntactic_check_project
diff --git a/doc/developer/tutorial.tex b/doc/developer/tutorial.tex
index 0f68c6a8e95789c32b2ebd7c7bb7048e51388b67..675985f348f4627d3d8f330c5876eff09c24834d 100644
--- a/doc/developer/tutorial.tex
+++ b/doc/developer/tutorial.tex
@@ -122,7 +122,7 @@ platform. This tutorial focuses on specific parts of this figure.
{on chain,draw,fill=Orange,minimum height=\designheight,txt,
minimum width=\kernelwidth}]
{kernel}
- \node (db-main) {Db.Main};
+ \node (db-main) {Boot.Main};
\node (dynamic) {Dynamic};
\node (plugin) {Plugin};
\node (type) {Type};
@@ -148,7 +148,7 @@ platform. This tutorial focuses on specific parts of this figure.
\end{tikzpicture}
\end{center}
-\scodeidx{Db}{Main}\codeidx{Dynamic}\codeidx{Plugin}
+\scodeidx{Boot}{Main}\codeidx{Dynamic}\codeidx{Plugin}
\codeidx{Project}\codeidx{Type}
\codeidx{Design}
\index{GUI}\index{Plug-in!GUI}
@@ -163,7 +163,7 @@ a function or a functor). For instance,
the next section shows how to:
\begin{itemize}
\item extend the \framac entry point\index{Entry point} thanks to the function
- \texttt{Db.Main.extend}\sscodeidx{Db}{Main}{extend} if you want to run
+ \texttt{Boot.Main.extend}\sscodeidx{Boot}{Main}{extend} if you want to run
plug-in specific code whenever \framac is executed;
\item use specific plug-in services provided by the module
\texttt{Plugin}\codeidx{Plugin}, such as adding a new \framac option.
@@ -247,7 +247,7 @@ Let us add a simple file to our plug-in:
\listingname{./hello\_world.ml}
\ocamlinput{./tutorial/hello/v1-simple/hello_world.ml}
-\sscodeidx{Db}{Main}{extend}
+\sscodeidx{Boot}{Main}{extend}
This file defines a simple function that writes a message to an output file,
then registers the function \texttt{run} as an entry point. \framac will call
@@ -281,7 +281,7 @@ Registering a plug-in is achieved through the use of the
\listingname{./hello\_world.ml}
\ocamlinput{./tutorial/hello/v2-register/hello_world.ml}
-\sscodeidx{Db}{Main}{extend}
+\sscodeidx{Boot}{Main}{extend}
\scodeidx{Plugin}{Register}
The argument to the \texttt{Plugin.Register} functor is a module with three
@@ -318,7 +318,7 @@ general services instead\footnote{However, writing to a new file using standard
\listingname{./hello\_world.ml}
\ocamlinput{./tutorial/hello/v3-log/hello_world.ml}
-\sscodeidx{Db}{Main}{extend}
+\sscodeidx{Boot}{Main}{extend}
\scodeidx{Plugin}{Register}
Running this script yields the following output:
@@ -440,7 +440,7 @@ You can uninstall it by running \verb|dune uninstall|.
Here is a slightly more complex example where the plug-in has been split into
several files. Usually, plug-in registration through \texttt{Plugin.Register}
should be done at the bottom of the module hierarchy, while registration of the
-\texttt{run} function through \texttt{Db.Main.extend} should be at the top.
+\texttt{run} function through \texttt{Boot.Main.extend} should be at the top.
The three following files completely replace the \texttt{./hello\_world.ml}
from the previous section. Modules are directly called by their name in the
classical \ocaml way.
@@ -454,7 +454,7 @@ classical \ocaml way.
\listingname{./hello\_run.ml}
\ocamlinput{./tutorial/hello/v5-multiple/hello_run.ml}
-\sscodeidx{Db}{Main}{extend}
+\sscodeidx{Boot}{Main}{extend}
The plug-in can be tested again by running:
@@ -656,7 +656,7 @@ Now, let's introduce an error. Assume the plug-in has been modified as follows:
\listingname{./hello\_run.ml}
\ocamlinput{./tutorial/hello/v6-test-with-bug/hello_run.ml}
-\sscodeidx{Db}{Main}{extend}
+\sscodeidx{Boot}{Main}{extend}
We assume that ``\texttt{Hello, world!}'' has been unintentionally changed to
``\texttt{Hello world!}''.
@@ -750,7 +750,7 @@ Then, we add some documentation tags to our modules:
\listingname{./hello\_run.ml}
\ocamlinput{./tutorial/hello/v7-doc//hello_run.ml}
-\sscodeidx{Db}{Main}{extend}
+\sscodeidx{Boot}{Main}{extend}
Running \verb|dune build @doc| will generate documentation files in
\texttt{./\_build/default/\_doc/\_html}. Open \texttt{index.html} in your
@@ -1042,7 +1042,7 @@ Now our plug-in can call all functions and access all types declared in
For historical reasons, several kernel-integrated plug-ins, such as
\textsf{From}, \textsf{InOut} and \textsf{Slicing}, had their API exposed
-via the \texttt{Db} module of the \framac kernel. This has been deprecated
+via the \texttt{Boot} module of the \framac kernel. This has been deprecated
for \textsf{Eva}, and newer plug-ins expose their public interface directly.
In our example, we will use \textsf{Eva}'s new API to obtain reachability
@@ -1112,7 +1112,7 @@ We will create the following files:
command-line options (\verb|Enabled| and \verb|OutputFile|);
\item[visit.ml]: will contain the \verb|print_stmt| function and the visitor;
\item[run.ml]: will contain the definition of function \verb|run| and the
- call to \verb|Db.Main.extend|.
+ call to \verb|Boot.Main.extend|.
\end{description}
Note that a few changes are needed to the code: functions from other files
diff --git a/doc/developer/tutorial/hello/src/extend_run.ml b/doc/developer/tutorial/hello/src/extend_run.ml
index e256faa8a32f45946288a775ea6dbcc6e25253d0..4ee00dad2e55f438854ed90ba1329ad26ceba80a 100644
--- a/doc/developer/tutorial/hello/src/extend_run.ml
+++ b/doc/developer/tutorial/hello/src/extend_run.ml
@@ -1 +1 @@
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/hello/v1-simple/hello_world.ml b/doc/developer/tutorial/hello/v1-simple/hello_world.ml
index 4cc340bc30d2c07a6417f012e124d30c0d533825..e4bd3f11a35681cd93890902c785e4568dfe897d 100644
--- a/doc/developer/tutorial/hello/v1-simple/hello_world.ml
+++ b/doc/developer/tutorial/hello/v1-simple/hello_world.ml
@@ -8,4 +8,4 @@ let run () =
let msg = Printexc.to_string exc in
Printf.eprintf "There was an error: %s\n" msg
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/hello/v2-register/hello_world.ml b/doc/developer/tutorial/hello/v2-register/hello_world.ml
index e5c74452edddbeadc9391e782b657e1b4b963dcf..5f3817778ebd052192b21669882fa288893007fb 100644
--- a/doc/developer/tutorial/hello/v2-register/hello_world.ml
+++ b/doc/developer/tutorial/hello/v2-register/hello_world.ml
@@ -17,4 +17,4 @@ let run () =
let msg = Printexc.to_string exc in
Printf.eprintf "There was an error: %s\n" msg
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/hello/v3-log/hello_world.ml b/doc/developer/tutorial/hello/v3-log/hello_world.ml
index 3d9a51c9c604652a63f21c9a4074b6f38ff0fe5a..988275d9d341ffa6fa8695e2c56ad40c29808341 100644
--- a/doc/developer/tutorial/hello/v3-log/hello_world.ml
+++ b/doc/developer/tutorial/hello/v3-log/hello_world.ml
@@ -15,4 +15,4 @@ let run () =
in
Self.result "11 * 5 = %d" product
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/hello/v4-options/hello_world.ml b/doc/developer/tutorial/hello/v4-options/hello_world.ml
index 382621862ec580be5c3723396d727593b07e4161..cc433a923fd2668f12619f4b68c42b7459de7511 100644
--- a/doc/developer/tutorial/hello/v4-options/hello_world.ml
+++ b/doc/developer/tutorial/hello/v4-options/hello_world.ml
@@ -40,4 +40,4 @@ let run () =
let msg = Printexc.to_string exc in
Printf.eprintf "There was an error: %s\n" msg
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/hello/v5-multiple/hello_run.ml b/doc/developer/tutorial/hello/v5-multiple/hello_run.ml
index e688748981644b66e97171f44f68a7506821fcd4..3a289ed851cb41b7a0f6945b7218e110b0581db7 100644
--- a/doc/developer/tutorial/hello/v5-multiple/hello_run.ml
+++ b/doc/developer/tutorial/hello/v5-multiple/hello_run.ml
@@ -2,4 +2,4 @@ let run () =
if Hello_options.Enabled.get() then
Hello_print.output "Hello, world!"
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/hello/v6-test-with-bug/hello_run.ml b/doc/developer/tutorial/hello/v6-test-with-bug/hello_run.ml
index e01bf492151dd13574dc8b7abde0e992a417769d..23af83d0008e0a7aa763ffa46d3a70d674fb80b6 100644
--- a/doc/developer/tutorial/hello/v6-test-with-bug/hello_run.ml
+++ b/doc/developer/tutorial/hello/v6-test-with-bug/hello_run.ml
@@ -2,4 +2,4 @@ let run () =
if Hello_options.Enabled.get() then
Hello_print.output "Hello world!" (* removed comma *)
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/hello/v7-doc/hello_run.ml b/doc/developer/tutorial/hello/v7-doc/hello_run.ml
index e46b2fe6fc2f72585dccc7fbe40618eb4ab1be43..6c15467ee648a43199b14bd1413d632392b46446 100644
--- a/doc/developer/tutorial/hello/v7-doc/hello_run.ml
+++ b/doc/developer/tutorial/hello/v7-doc/hello_run.ml
@@ -13,4 +13,4 @@ let run () =
Hello_print.output "Hello, world!"
(** Definition of the entry point of the hello plug-in. *)
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/viewcfg/src/extend_with_run_with_options.ml b/doc/developer/tutorial/viewcfg/src/extend_with_run_with_options.ml
index b498fdb3da4511bc0a74c731c6e0c88046886d00..eb80f881da9479b14529a5810dbdfe7d2f30f102 100644
--- a/doc/developer/tutorial/viewcfg/src/extend_with_run_with_options.ml
+++ b/doc/developer/tutorial/viewcfg/src/extend_with_run_with_options.ml
@@ -6,4 +6,4 @@ let run () =
Visitor.visitFramacFileSameGlobals (new print_cfg fmt) (Ast.get ());
close_out chan
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/viewcfg/src/extend_with_simple_run.ml b/doc/developer/tutorial/viewcfg/src/extend_with_simple_run.ml
index 122d1ffdc531791aca5aa71de75a6db779882fa9..f6cfe1692742bcca7a98251eb68a66d5059ac017 100644
--- a/doc/developer/tutorial/viewcfg/src/extend_with_simple_run.ml
+++ b/doc/developer/tutorial/viewcfg/src/extend_with_simple_run.ml
@@ -4,4 +4,4 @@ let run () =
Visitor.visitFramacFileSameGlobals (new print_cfg fmt) (Ast.get ());
close_out chan
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/viewcfg/v1-simple/view_cfg.ml b/doc/developer/tutorial/viewcfg/v1-simple/view_cfg.ml
index 0841af991e943fae2d37d9daf1498dc608d73ed7..7a695885327a51392c578d3d85a694179090ef98 100644
--- a/doc/developer/tutorial/viewcfg/v1-simple/view_cfg.ml
+++ b/doc/developer/tutorial/viewcfg/v1-simple/view_cfg.ml
@@ -50,4 +50,4 @@ let run () =
Visitor.visitFramacFileSameGlobals (new print_cfg fmt) (Ast.get ());
close_out chan
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/viewcfg/v2-options/view_cfg.ml b/doc/developer/tutorial/viewcfg/v2-options/view_cfg.ml
index 8fa8244e8d460ef4f3f26ec30b6d7918b47ca0ca..fdf6111c94e02ceca8fe8e9d939a90c5919f82b7 100644
--- a/doc/developer/tutorial/viewcfg/v2-options/view_cfg.ml
+++ b/doc/developer/tutorial/viewcfg/v2-options/view_cfg.ml
@@ -71,4 +71,4 @@ let run () =
Visitor.visitFramacFileSameGlobals (new print_cfg fmt) (Ast.get ());
close_out chan
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/viewcfg/v3-eva/view_cfg.ml b/doc/developer/tutorial/viewcfg/v3-eva/view_cfg.ml
index 1eefd2a6aafa696dbdfc11045a2169bb73eef85b..d4efc8e180a17821395a7476d9ae56fbbd7d656f 100644
--- a/doc/developer/tutorial/viewcfg/v3-eva/view_cfg.ml
+++ b/doc/developer/tutorial/viewcfg/v3-eva/view_cfg.ml
@@ -79,4 +79,4 @@ let run () =
Visitor.visitFramacFileSameGlobals (new print_cfg fmt) (Ast.get ());
close_out chan
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/viewcfg/v4-bogue/run.ml b/doc/developer/tutorial/viewcfg/v4-bogue/run.ml
index adc46ac9afe5f9e8de4429f4f89fef630fb99f85..77310af6265b1dc720b369cb676a8b9ae56a7736 100644
--- a/doc/developer/tutorial/viewcfg/v4-bogue/run.ml
+++ b/doc/developer/tutorial/viewcfg/v4-bogue/run.ml
@@ -2,4 +2,4 @@ let run () =
if Options.Gui.get() then
Gui.show ()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/viewcfg/v5-state/run.ml b/doc/developer/tutorial/viewcfg/v5-state/run.ml
index adc46ac9afe5f9e8de4429f4f89fef630fb99f85..77310af6265b1dc720b369cb676a8b9ae56a7736 100644
--- a/doc/developer/tutorial/viewcfg/v5-state/run.ml
+++ b/doc/developer/tutorial/viewcfg/v5-state/run.ml
@@ -2,4 +2,4 @@ let run () =
if Options.Gui.get() then
Gui.show ()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/viewcfg/v6-state-clear/run.ml b/doc/developer/tutorial/viewcfg/v6-state-clear/run.ml
index adc46ac9afe5f9e8de4429f4f89fef630fb99f85..77310af6265b1dc720b369cb676a8b9ae56a7736 100644
--- a/doc/developer/tutorial/viewcfg/v6-state-clear/run.ml
+++ b/doc/developer/tutorial/viewcfg/v6-state-clear/run.ml
@@ -2,4 +2,4 @@ let run () =
if Options.Gui.get() then
Gui.show ()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/slicing/design-fr/intro.tex b/doc/slicing/design-fr/intro.tex
index 7f312529bebf333dfa3e2427babd70bc15d6a658..db722a6cb3fc366e3fda7df0593e32faa891c450 100644
--- a/doc/slicing/design-fr/intro.tex
+++ b/doc/slicing/design-fr/intro.tex
@@ -348,7 +348,7 @@ Pour plus de détail sur l'implémentation ou les commandes disponibles,
le lecteur est invité à consulter la documentation du code
car elle sera toujours plus détaillée et à jour que ce rapport.
Comme la boîte à outil de \slicing est un greffon de \ppc,
-son interface est définie dans le module \verbtt{Db.Slicing}.
+son interface est définie dans le module \verbtt{Slicing}.
Par ailleurs, l'introduction de la documentation interne du module
donne une idée de l'architecture, et donne des points d'entrée.\\
diff --git a/share/analysis-scripts/list_functions.ml b/share/analysis-scripts/list_functions.ml
index 2f5e58acc1635df6a8b03b80d2d92bc6607f00f7..843e8bfd9d228db5e290a16d877b5eb6a2ae0b3c 100644
--- a/share/analysis-scripts/list_functions.ml
+++ b/share/analysis-scripts/list_functions.ml
@@ -300,4 +300,4 @@ let run () =
in
print_json outfp funinfos_json
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/src/kernel_internals/runtime/boot.ml b/src/kernel_internals/runtime/boot.ml
index 9f9d354823e420ca49bc6b66786a5b92d37423ab..e93f37b85bd6d346e81e0bf14eaf2c7460b8b218 100644
--- a/src/kernel_internals/runtime/boot.ml
+++ b/src/kernel_internals/runtime/boot.ml
@@ -20,37 +20,40 @@
(* *)
(**************************************************************************)
-let boot () =
- let play_analysis () =
- if Kernel.TypeCheck.get () then begin
- if Kernel.Files.get () <> [] || Kernel.TypeCheck.is_set () then begin
- Ast.compute ();
- (* Printing files before anything else (in debug mode only) *)
- if Kernel.debug_atleast 1 && Kernel.is_debug_key_enabled Kernel.dkey_ast
- then File.pretty_ast ()
- end
- end;
- try
- Db.Main.apply ();
- Log.treat_deferred_error ();
- (* Printing code, if required, have to be done at end. *)
- if Kernel.PrintCode.get () then File.pretty_ast ();
- (* Easier to handle option -set-project-as-default at the last moment:
- no need to worry about nested [Project.on] *)
- Project.set_keep_current (Kernel.Set_project_as_default.get ());
- (* unset Kernel.Set_project_as_default, but only if it set.
- This avoids disturbing the "set by user" flag. *)
- if Kernel.Set_project_as_default.get () then
- Kernel.Set_project_as_default.off ()
- with Globals.No_such_entry_point msg ->
- Kernel.abort "%s" msg
- in
- let on_from_name name f =
- try Project.on (Project.from_unique_name name) f ()
- with Project.Unknown_project -> Kernel.abort "no project `%s'." name
- in
- Db.Main.play := play_analysis;
+module Main = Hook.Make ()
+
+let toplevel = ref (fun f -> f ())
+let set_toplevel run = toplevel := run
+let play_analysis () =
+ if Kernel.TypeCheck.get () then begin
+ if Kernel.Files.get () <> [] || Kernel.TypeCheck.is_set () then begin
+ Ast.compute ();
+ (* Printing files before anything else (in debug mode only) *)
+ if Kernel.debug_atleast 1 && Kernel.is_debug_key_enabled Kernel.dkey_ast
+ then File.pretty_ast ()
+ end
+ end;
+ try
+ Main.apply ();
+ Log.treat_deferred_error ();
+ (* Printing code, if required, have to be done at end. *)
+ if Kernel.PrintCode.get () then File.pretty_ast ();
+ (* Easier to handle option -set-project-as-default at the last moment:
+ no need to worry about nested [Project.on] *)
+ Project.set_keep_current (Kernel.Set_project_as_default.get ());
+ (* unset Kernel.Set_project_as_default, but only if it set.
+ This avoids disturbing the "set by user" flag. *)
+ if Kernel.Set_project_as_default.get () then
+ Kernel.Set_project_as_default.off ()
+ with Globals.No_such_entry_point msg ->
+ Kernel.abort "%s" msg
+
+let on_from_name name f =
+ try Project.on (Project.from_unique_name name) f ()
+ with Project.Unknown_project -> Kernel.abort "no project `%s'." name
+
+let boot () =
(* Main: let's go! *)
Sys.catch_break true;
let f () =
@@ -58,7 +61,7 @@ let boot () =
let on_from_name = { Cmdline.on_from_name } in
Cmdline.parse_and_boot
~on_from_name
- ~get_toplevel:(fun () -> !Db.Toplevel.run)
+ ~get_toplevel:(fun () -> !toplevel)
~play_analysis
in
Cmdline.catch_toplevel_run
diff --git a/src/kernel_internals/runtime/boot.mli b/src/kernel_internals/runtime/boot.mli
index e6825efd8a10f4e51b702b8534323601858e0573..7655842fb51e08f109189576b6d52596385ff1fe 100644
--- a/src/kernel_internals/runtime/boot.mli
+++ b/src/kernel_internals/runtime/boot.mli
@@ -20,6 +20,27 @@
(* *)
(**************************************************************************)
+(** Frama-C main interface.
+ @since Lithium-20081201
+ @before Frama-C+dev it was in a module named Db
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
+module Main : sig
+ val extend : (unit -> unit) -> unit
+ (** Register a function to be called by the Frama-C main entry point.
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
+end
+
+val play_analysis : unit -> unit
+(** Run all the Frama-C analyses. This function should be called only by
+ toplevels.
+ @since Frama-C+dev
+*)
+
val boot : unit -> unit
-(** Start and define the Frama-C kernel main loop. Run by the last linked
- module. *)
+(** Start and define the Frama-C kernel main loop. *)
+
+val set_toplevel: ((unit -> unit) -> unit) -> unit
+(** Changes the toplevel function to run on boot
+ @since Frama-C+dev
+ @before Frama-C+dev it was provided in a different way in Db.Toplevel
+*)
diff --git a/src/kernel_services/plugin_entry_points/async.ml b/src/kernel_services/plugin_entry_points/async.ml
new file mode 100644
index 0000000000000000000000000000000000000000..62b272ad7100315bd248f10ec47249546c5ed7b4
--- /dev/null
+++ b/src/kernel_services/plugin_entry_points/async.ml
@@ -0,0 +1,157 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+type daemon = {
+ trigger : unit -> unit ;
+ on_delayed : (int -> unit) option ;
+ on_finished : (unit -> unit) option ;
+ debounced : float ; (* in ms *)
+ mutable next_at : float ; (* next trigger time *)
+ mutable last_yield_at : float ; (* last yield time *)
+}
+
+(* ---- Registry ---- *)
+
+let daemons = ref []
+
+let on_progress ?(debounced=0) ?on_delayed ?on_finished trigger =
+ let d = {
+ trigger ;
+ debounced = float debounced *. 0.001 ;
+ on_delayed ;
+ on_finished ;
+ last_yield_at = 0.0 ;
+ next_at = 0.0 ;
+ } in
+ daemons := List.append !daemons [d] ; d
+
+let off_progress d =
+ daemons := List.filter (fun d0 -> d != d0) !daemons ;
+ match d.on_finished with
+ | None -> ()
+ | Some f -> f ()
+
+let while_progress ?debounced ?on_delayed ?on_finished progress =
+ let d : daemon option ref = ref None in
+ let trigger () =
+ if not @@ progress () then
+ Option.iter off_progress !d
+ in
+ d := Some (on_progress ?debounced ?on_delayed ?on_finished trigger)
+
+let with_progress ?debounced ?on_delayed ?on_finished trigger job data =
+ let d = on_progress ?debounced ?on_delayed ?on_finished trigger in
+ let result =
+ try job data
+ with exn ->
+ off_progress d ;
+ raise exn
+ in
+ off_progress d ; result
+
+(* ---- Canceling ---- *)
+
+exception Cancel
+
+(* ---- Triggering ---- *)
+
+let canceled = ref false
+let cancel () = canceled := true
+
+let warn_error exn =
+ Kernel.failure
+ "Unexpected Async.daemon exception:@\n%s"
+ (Printexc.to_string exn)
+
+let fire ~warn_on_delayed ~forced ~time d =
+ if forced || time > d.next_at then
+ begin
+ try
+ d.next_at <- time +. d.debounced ;
+ d.trigger () ;
+ with
+ | Cancel -> canceled := true
+ | exn -> warn_error exn ; raise exn
+ end ;
+ match d.on_delayed with
+ | None -> ()
+ | Some warn ->
+ if warn_on_delayed && 0.0 < d.last_yield_at then
+ begin
+ let time_since_last_yield = time -. d.last_yield_at in
+ let delay = if d.debounced > 0.0 then d.debounced else 0.1 in
+ if time_since_last_yield > delay then
+ warn (int_of_float (time_since_last_yield *. 1000.0)) ;
+ end ;
+ d.last_yield_at <- time
+
+let raise_if_canceled () =
+ if !canceled then ( canceled := false ; raise Cancel )
+
+(* ---- Yielding ---- *)
+
+let do_yield ~warn_on_delayed ~forced () =
+ match !daemons with
+ | [] -> ()
+ | ds ->
+ begin
+ let time = Unix.gettimeofday () in
+ List.iter (fire ~warn_on_delayed ~forced ~time) ds ;
+ raise_if_canceled () ;
+ end
+
+let yield = do_yield ~warn_on_delayed:true ~forced:false
+let flush = do_yield ~warn_on_delayed:false ~forced:true
+
+(* ---- Sleeping ---- *)
+
+let rec gcd a b = if b = 0 then a else gcd b (a mod b)
+
+(* n=0 means no periodic daemons (yet) *)
+let merge_period n { debounced = p } =
+ if p > 0.0 then gcd (int_of_float (p *. 1000.0)) n else n
+
+let sleep ms =
+ if ms > 0 then
+ let delta = float ms *. 0.001 in
+ let period = List.fold_left merge_period 0 !daemons in
+ if period = 0 then
+ begin
+ Unix.sleepf delta ;
+ do_yield ~warn_on_delayed:false ~forced:false ()
+ end
+ else
+ let delay = float period *. 0.001 in
+ let finished_at = Unix.gettimeofday () +. delta in
+ let rec wait_and_trigger () =
+ Unix.sleepf delay ;
+ let time = Unix.gettimeofday () in
+ List.iter
+ (fire ~warn_on_delayed:false ~forced:false ~time)
+ !daemons ;
+ raise_if_canceled () ;
+ if time < finished_at then
+ if time +. delay > finished_at then
+ Unix.sleepf (finished_at -. time)
+ else wait_and_trigger ()
+ in
+ wait_and_trigger ()
diff --git a/src/kernel_services/plugin_entry_points/async.mli b/src/kernel_services/plugin_entry_points/async.mli
new file mode 100644
index 0000000000000000000000000000000000000000..0775c22c8be984380185674ded31a12a209058e3
--- /dev/null
+++ b/src/kernel_services/plugin_entry_points/async.mli
@@ -0,0 +1,83 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** Module dedicated to asynchronous actions.
+ @since Frama-C+dev
+ @before Frama-C+dev these features were in a module named Db
+*)
+
+(** Registered daemon on progress. *)
+type daemon
+
+(** [on_progress ?debounced ?on_delayed trigger] registers [trigger] as new
+ daemon to be executed on each {!yield}.
+ @param debounced the least amount of time between two successive calls to
+ the daemon, in milliseconds (default is 0ms).
+ @param on_delayed callback is invoked as soon as the time since the last
+ {!yield} is greater than [debounced] milliseconds (or 100ms at least).
+ @param on_finished callback is invoked when the callback is unregistered.
+*)
+val on_progress :
+ ?debounced:int -> ?on_delayed:(int -> unit) -> ?on_finished:(unit -> unit) ->
+ (unit -> unit) -> daemon
+
+(** Unregister the [daemon]. *)
+val off_progress : daemon -> unit
+
+(** [while_progress ?debounced ?on_delayed ?on_finished trigger] is similar to
+ [on_progress] but the daemon is automatically unregistered
+ as soon as [trigger] returns [false].
+ Same optional parameters than [on_progress].
+*)
+val while_progress :
+ ?debounced:int -> ?on_delayed:(int -> unit) -> ?on_finished:(unit -> unit) ->
+ (unit -> bool) -> unit
+
+(** [with_progress ?debounced ?on_delayed trigger job data] executes the given
+ [job] on [data] while registering [trigger] as temporary (debounced) daemon.
+ The daemon is finally unregistered at the end of the computation.
+ Same optional parameters than [on_progress].
+*)
+val with_progress :
+ ?debounced:int -> ?on_delayed:(int -> unit) -> ?on_finished:(unit -> unit) ->
+ (unit -> unit) -> ('a -> 'b) -> 'a -> 'b
+
+(** Trigger all daemons immediately. *)
+val flush : unit -> unit
+
+(** Trigger all registered daemons (debounced).
+ This function should be called from time to time by all analysers taking
+ time. In GUI or Server mode, this will make the clients responsive. *)
+val yield : unit -> unit
+
+(** Interrupt the currently running job: the next call to {!yield}
+ will raise a [Cancel] exception. *)
+val cancel : unit -> unit
+
+(** Pauses the currently running process for the specified time, in milliseconds.
+ Registered daemons, if any, will be regularly triggered during this waiting
+ time at a reasonable period with respect to their debouncing constraints.
+*)
+val sleep : int -> unit
+
+(** This exception may be raised by {!yield} to interrupt computations. *)
+exception Cancel
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 365cbf36d5e5dfec6b09b31ed1089312760095f4..e1d0d1816d585b87c87ca8047d9e5d02890cafd2 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -20,163 +20,6 @@
(* *)
(**************************************************************************)
-open Extlib
-
module Main = struct
- include Hook.Make()
- let play = mk_fun "Main.play"
-end
-
-module Toplevel = struct
-
- let run = ref (fun f -> f ())
-
+ let extend = Boot.Main.extend
end
-
-(* ************************************************************************* *)
-(** {2 GUI} *)
-(* ************************************************************************* *)
-
-type daemon = {
- trigger : unit -> unit ;
- on_delayed : (int -> unit) option ;
- on_finished : (unit -> unit) option ;
- debounced : float ; (* in ms *)
- mutable next_at : float ; (* next trigger time *)
- mutable last_yield_at : float ; (* last yield time *)
-}
-
-(* ---- Registry ---- *)
-
-let daemons = ref []
-
-let on_progress ?(debounced=0) ?on_delayed ?on_finished trigger =
- let d = {
- trigger ;
- debounced = float debounced *. 0.001 ;
- on_delayed ;
- on_finished ;
- last_yield_at = 0.0 ;
- next_at = 0.0 ;
- } in
- daemons := List.append !daemons [d] ; d
-
-let off_progress d =
- daemons := List.filter (fun d0 -> d != d0) !daemons ;
- match d.on_finished with
- | None -> ()
- | Some f -> f ()
-
-let while_progress ?debounced ?on_delayed ?on_finished progress =
- let d : daemon option ref = ref None in
- let trigger () =
- if not @@ progress () then
- Option.iter off_progress !d
- in
- d := Some (on_progress ?debounced ?on_delayed ?on_finished trigger)
-
-let with_progress ?debounced ?on_delayed ?on_finished trigger job data =
- let d = on_progress ?debounced ?on_delayed ?on_finished trigger in
- let result =
- try job data
- with exn ->
- off_progress d ;
- raise exn
- in
- off_progress d ; result
-
-(* ---- Canceling ---- *)
-
-exception Cancel
-
-(* ---- Triggering ---- *)
-
-let canceled = ref false
-let cancel () = canceled := true
-
-let warn_error exn =
- Kernel.failure
- "Unexpected Db.daemon exception:@\n%s"
- (Printexc.to_string exn)
-
-let fire ~warn_on_delayed ~forced ~time d =
- if forced || time > d.next_at then
- begin
- try
- d.next_at <- time +. d.debounced ;
- d.trigger () ;
- with
- | Cancel -> canceled := true
- | exn -> warn_error exn ; raise exn
- end ;
- match d.on_delayed with
- | None -> ()
- | Some warn ->
- if warn_on_delayed && 0.0 < d.last_yield_at then
- begin
- let time_since_last_yield = time -. d.last_yield_at in
- let delay = if d.debounced > 0.0 then d.debounced else 0.1 in
- if time_since_last_yield > delay then
- warn (int_of_float (time_since_last_yield *. 1000.0)) ;
- end ;
- d.last_yield_at <- time
-
-let raise_if_canceled () =
- if !canceled then ( canceled := false ; raise Cancel )
-
-(* ---- Yielding ---- *)
-
-let do_yield ~warn_on_delayed ~forced () =
- match !daemons with
- | [] -> ()
- | ds ->
- begin
- let time = Unix.gettimeofday () in
- List.iter (fire ~warn_on_delayed ~forced ~time) ds ;
- raise_if_canceled () ;
- end
-
-let yield = do_yield ~warn_on_delayed:true ~forced:false
-let flush = do_yield ~warn_on_delayed:false ~forced:true
-
-(* ---- Sleeping ---- *)
-
-let rec gcd a b = if b = 0 then a else gcd b (a mod b)
-
-(* n=0 means no periodic daemons (yet) *)
-let merge_period n { debounced = p } =
- if p > 0.0 then gcd (int_of_float (p *. 1000.0)) n else n
-
-let sleep ms =
- if ms > 0 then
- let delta = float ms *. 0.001 in
- let period = List.fold_left merge_period 0 !daemons in
- if period = 0 then
- begin
- Unix.sleepf delta ;
- do_yield ~warn_on_delayed:false ~forced:false ()
- end
- else
- let delay = float period *. 0.001 in
- let finished_at = Unix.gettimeofday () +. delta in
- let rec wait_and_trigger () =
- Unix.sleepf delay ;
- let time = Unix.gettimeofday () in
- List.iter
- (fire ~warn_on_delayed:false ~forced:false ~time)
- !daemons ;
- raise_if_canceled () ;
- if time < finished_at then
- if time +. delay > finished_at then
- Unix.sleepf (finished_at -. time)
- else wait_and_trigger ()
- in
- wait_and_trigger ()
-
-(* ************************************************************************* *)
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index e7d04befcc2991a6b84725468d1f43cd09b83286..f30706002fe4c71b1eaab8ec6695fd2026268a38 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -20,125 +20,12 @@
(* *)
(**************************************************************************)
-(** Database in which static plugins are registered.
- @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
-
-(**
- Modules providing general services:
- - {!Dynamic}: API for plug-ins linked dynamically
- - {!Log}: message outputs and printers
- - {!Plugin}: general services for plug-ins
- - {!Project} and associated files: {!Datatype} and {!State_builder}.
-
- Other main kernel modules:
- - {!Ast}: the cil AST
- - {!Ast_info}: syntactic value directly computed from the Cil Ast
- - {!File}: Cil file initialization
- - {!Globals}: global variables, functions and annotations
- - {!Annotations}: annotations associated with a statement
- - {!Property_status}: status of annotations
- - {!Kernel_function}: C functions as seen by Frama-C
- - {!Stmts_graph}: the statement graph
- - {!Loop}: (natural) loops
- - {!Visitor}: frama-c visitors
- - {!Kernel}: general parameters of Frama-C (mostly set from the command
- line)
-*)
-
-(** Frama-C main interface.
+(** DEPRECATED Frama-C main interface.
@since Lithium-20081201
- @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
+ @deprecated Frama-C+dev Use module {!Boot.Main} *)
module Main: sig
-
val extend : (unit -> unit) -> unit
+ [@@ deprecated "Use module Boot.Main"]
(** Register a function to be called by the Frama-C main entry point.
- @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
-
- val play: (unit -> unit) ref
- (** Run all the Frama-C analyses. This function should be called only by
- toplevels.
- @since Beryllium-20090901 *)
-
- (**/**)
- val apply: unit -> unit
- (** Not for casual user. *)
- (**/**)
-
-end
-
-module Toplevel: sig
-
- val run: ((unit -> unit) -> unit) ref
- (** Run a Frama-C toplevel playing the game given in argument (in
- particular, applying the argument runs the analyses).
- @since Beryllium-20090901 *)
-
+ @deprecated Frama-C+dev Use module {!Boot.Main} *)
end
-
-(** {3 GUI} *)
-
-(** Registered daemon on progress. *)
-type daemon
-
-(**
- [on_progress ?debounced ?on_delayed trigger] registers [trigger] as new
- daemon to be executed on each {!yield}.
- @param debounced the least amount of time between two successive calls to the
- daemon, in milliseconds (default is 0ms).
- @param on_delayed callback is invoked as soon as the time since the last
- {!yield} is greater than [debounced] milliseconds (or 100ms at least).
- @param on_finished callback is invoked when the callback is unregistered.
-*)
-val on_progress :
- ?debounced:int -> ?on_delayed:(int -> unit) -> ?on_finished:(unit -> unit) ->
- (unit -> unit) -> daemon
-
-(** Unregister the [daemon]. *)
-val off_progress : daemon -> unit
-
-(** [while_progress ?debounced ?on_delayed ?on_finished trigger] is similar to
- [on_progress] but the daemon is automatically unregistered
- as soon as [trigger] returns [false].
- Same optional parameters than [on_progress].
-*)
-val while_progress :
- ?debounced:int -> ?on_delayed:(int -> unit) -> ?on_finished:(unit -> unit) ->
- (unit -> bool) -> unit
-
-(**
- [with_progress ?debounced ?on_delayed trigger job data] executes the given
- [job] on [data] while registering [trigger] as temporary (debounced) daemon.
- The daemon is finally unregistered at the end of the computation.
- Same optional parameters than [on_progress].
-*)
-val with_progress :
- ?debounced:int -> ?on_delayed:(int -> unit) -> ?on_finished:(unit -> unit) ->
- (unit -> unit) -> ('a -> 'b) -> 'a -> 'b
-
-(** Trigger all daemons immediately. *)
-val flush : unit -> unit
-
-(** Trigger all registered daemons (debounced).
- This function should be called from time to time by all analysers taking
- time. In GUI or Server mode, this will make the clients responsive. *)
-val yield : unit -> unit
-
-(** Interrupt the currently running job: the next call to {!yield}
- will raise a [Cancel] exception. *)
-val cancel : unit -> unit
-
-(**
- Pauses the currently running process for the specified time, in milliseconds.
- Registered daemons, if any, will be regularly triggered during this waiting
- time at a reasonable period with respect to their debouncing constraints.
-*)
-val sleep : int -> unit
-
-(** This exception may be raised by {!yield} to interrupt computations. *)
-exception Cancel
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/visitors/visitor.mli b/src/kernel_services/visitors/visitor.mli
index 1414b29a14ab2e24a733bf8be800c2b02743b27f..c3923794a177dbd5ad1d06f446cd814d9d5ff322 100644
--- a/src/kernel_services/visitors/visitor.mli
+++ b/src/kernel_services/visitors/visitor.mli
@@ -24,7 +24,7 @@
open Cil_types
-(** Class type for a Db-aware visitor.
+(** Class type for a database-aware visitor.
This is done by defining auxiliary methods that can be
redefined in inherited classes, while the corresponding ones from
{!Cil.cilVisitor} {b must} retain their values as defined here. Otherwise,
diff --git a/src/libraries/utils/command.ml b/src/libraries/utils/command.ml
index c0ef15d620221e39da672e65f639088f25cd86ee..f2211d8a389b0a6f35b2bdff706b145089ea98c8 100644
--- a/src/libraries/utils/command.ml
+++ b/src/libraries/utils/command.ml
@@ -43,7 +43,7 @@ let pp_from_file fmt (file: Filepath.Normalized.t) =
let cin = open_in (file :> string) in
try
while true do
- Db.yield () ;
+ Async.yield () ;
let line = input_line cin in
Format.pp_print_string fmt line ;
Format.pp_print_newline fmt () ;
@@ -248,11 +248,11 @@ let command ?(timeout=0) ?stdout ?stderr cmd args =
| Not_ready terminate ->
begin
try
- Db.yield () ;
+ Async.yield () ;
if timeout > 0 && Unix.gettimeofday () -. !start > ftimeout then
- raise Db.Cancel ;
+ raise Async.Cancel ;
true
- with Db.Cancel as e ->
+ with Async.Cancel as e ->
terminate ();
raise e
end
diff --git a/src/libraries/utils/command.mli b/src/libraries/utils/command.mli
index bdf1f030c4052488fc2c43b3f3e6846932f09b95..b6ce12d959bd1b1fe13f54b8e77d182244c525b0 100644
--- a/src/libraries/utils/command.mli
+++ b/src/libraries/utils/command.mli
@@ -125,7 +125,9 @@ val command :
When this function returns, the stdout and stderr of the child
process will be filled into the arguments buffer.
@raise Sys_error when a system error occurs
- @raise Db.Cancel when the computation is interrupted or on timeout *)
+ @raise Async.Cancel when the computation is interrupted or on timeout
+ @before Frama-C+dev Async.Cancel was Db.Cancel
+*)
(*
Local Variables:
diff --git a/src/libraries/utils/task.ml b/src/libraries/utils/task.ml
index 557953250f45cd4473a3b7229cc64e2764cef2e3..86beb2188dcd814d62676ebcda0e2a1686fa7d17 100644
--- a/src/libraries/utils/task.ml
+++ b/src/libraries/utils/task.ml
@@ -108,9 +108,9 @@ struct
let rec wait = function
| UNIT a -> a
- | YIELD f -> Db.yield() ; wait (f Coin)
+ | YIELD f -> Async.yield() ; wait (f Coin)
| WAIT(ms,f) ->
- Db.yield() ; Unix.sleepf (float_of_int ms /. 1_000_000.); wait (f Coin)
+ Async.yield() ; Unix.sleepf (float_of_int ms /. 1_000_000.); wait (f Coin)
let finished = function UNIT a -> Some a | YIELD _ | WAIT _ -> None
@@ -342,7 +342,7 @@ let share sh = todo
let on_idle = ref
(fun f -> try
while f () do Unix.sleepf 0.05 (* wait for 50ms *) done
- with Db.Cancel -> ())
+ with Async.Cancel -> ())
(* -------------------------------------------------------------------------- *)
(* --- Task thread --- *)
@@ -484,8 +484,8 @@ let server_progress server () =
) server.running ;
Array.iter (schedule server) server.queue ;
let () =
- try Db.yield ()
- with Db.Cancel -> cancel_all server
+ try Async.yield ()
+ with Async.Cancel -> cancel_all server
in
fire server.activity ;
if server.running <> [] then
diff --git a/src/plugins/alias/Alias.ml b/src/plugins/alias/Alias.ml
index fe144bb2b96ff10ef8b8f29240892e52c4dd1390..fa71e931f156b8dad9bd99cae34fab8fe65e6df2 100644
--- a/src/plugins/alias/Alias.ml
+++ b/src/plugins/alias/Alias.ml
@@ -33,4 +33,4 @@ let main () =
end
let () =
- Db.Main.extend main
+ Boot.Main.extend main
diff --git a/src/plugins/aorai/aorai_register.ml b/src/plugins/aorai/aorai_register.ml
index 67739a849f82ed036730165d3406b0b8cb91ec0d..cc589bf59371c62ef0ca4131cf413a582d155060 100644
--- a/src/plugins/aorai/aorai_register.ml
+++ b/src/plugins/aorai/aorai_register.ml
@@ -200,7 +200,7 @@ let run, _ =
run
let main () = if Aorai_option.is_on () then run ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(*
Local Variables:
diff --git a/src/plugins/aorai/tests/Aorai_test.ml b/src/plugins/aorai/tests/Aorai_test.ml
index 5cd54943e86d5589f36fa80cd8d86f13d30b4266..47e9071fd8a164094251eef06787abeb159842ca 100644
--- a/src/plugins/aorai/tests/Aorai_test.ml
+++ b/src/plugins/aorai/tests/Aorai_test.ml
@@ -50,7 +50,6 @@ let is_suffix suf str =
let extend () =
let myrun =
- let run = !Db.Toplevel.run in
fun f ->
let my_project = Project.create "Reparsing" in
let wp_compute_kf kf =
@@ -71,7 +70,7 @@ let extend () =
then
wp_compute_kf kf
in
- run f;
+ f ();
let tmpdir = Filename.get_temp_dir_name () in
let tmpdir =
match Filename.chop_suffix_opt ~suffix:"/" tmpdir with
@@ -133,6 +132,6 @@ let extend () =
end;
ok:=true (* no error, we can erase the file *)
in
- Db.Toplevel.run := myrun
+ Boot.set_toplevel myrun
let () = extend ()
diff --git a/src/plugins/api-generator/api_generator.ml b/src/plugins/api-generator/api_generator.ml
index 95ce1b8feb867bdd15cc0a9c7ee44ab341c5a3b0..8a58db24333455c0a4985a0cbac47e8c4e732db9 100644
--- a/src/plugins/api-generator/api_generator.ml
+++ b/src/plugins/api-generator/api_generator.ml
@@ -581,6 +581,6 @@ let generate () =
end
let () =
- Db.Main.extend generate
+ Boot.Main.extend generate
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/callgraph/register.ml b/src/plugins/callgraph/register.ml
index 67792829ccc13bd7c1f32ba40da461af3555459a..d1a29f66bc4f1898ff14f15fafdd80781a075526 100644
--- a/src/plugins/callgraph/register.ml
+++ b/src/plugins/callgraph/register.ml
@@ -27,7 +27,7 @@ let main () =
end else
if not (Cg.is_computed ()) then Cg.dump ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(*
Local Variables:
diff --git a/src/plugins/constant_propagation/api.ml b/src/plugins/constant_propagation/api.ml
index 13c1a758514b42aedfc5e71c3cd884654cbfd8b7..b81b894199c01d393eda516848b3e0532d9f43b7 100644
--- a/src/plugins/constant_propagation/api.ml
+++ b/src/plugins/constant_propagation/api.ml
@@ -398,7 +398,7 @@ let main () =
if force_semantic_folding then compute ()
let () =
- Db.Main.extend main
+ Boot.Main.extend main
(*
Local Variables:
diff --git a/src/plugins/dive/main.ml b/src/plugins/dive/main.ml
index 6c81b013f84c8a11d4aea07b9852af7cc1ca04f4..33f036663ac343318c2ca7e2e208eaa1a39f63eb 100644
--- a/src/plugins/dive/main.ml
+++ b/src/plugins/dive/main.ml
@@ -66,4 +66,4 @@ let main () =
end
let () =
- Db.Main.extend main
+ Boot.Main.extend main
diff --git a/src/plugins/e-acsl/examples/demo/script.ml b/src/plugins/e-acsl/examples/demo/script.ml
index 5c61595d99b3af283f52eeb3bdbad942a2f28334..bca0d3708ad9c754898d14f3b2c44edfc8bc5ef7 100644
--- a/src/plugins/e-acsl/examples/demo/script.ml
+++ b/src/plugins/e-acsl/examples/demo/script.ml
@@ -113,4 +113,4 @@ let main () =
let ppt, line = search kf in
emit ppt line
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/src/plugins/e-acsl/src/main.ml b/src/plugins/e-acsl/src/main.ml
index 850ebb7fe74df3a1ce5164f9f724cd5d0d8e16f8..a4e5e85d31f4fcf406c56278beb2757a7f0e9eb1 100644
--- a/src/plugins/e-acsl/src/main.ml
+++ b/src/plugins/e-acsl/src/main.ml
@@ -162,7 +162,7 @@ let main () =
ignore (generate_code (Options.Project_name.get ()));
end
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(*
Local Variables:
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 69d7664b7b6ef74637f9965bf5978458291749d8..7ee21c551d305b60cadca7ec6460b7d37f67b24b 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -181,14 +181,7 @@ end
module Results: sig
(** Eva's result API is a new interface to access the results of an analysis,
- once it is completed. It may slightly change in the future. It aims at
- replacing most uses of [Db.Value], and has some advantages over Db's :
-
- - evaluations uses every available domains and not only Cvalue;
- - the caller may distinguish failure cases when a request is unsucessful;
- - working with callstacks is easy;
- - some common shortcuts are provided (e.g. for extracting ival directly);
- - overall, individual functions are simpler.
+ once it is completed. It may slightly change in the future.
The idea behind this API is that requests must be decomposed in several
steps. For instance, to evaluate an expression :
diff --git a/src/plugins/eva/engine/analysis.ml b/src/plugins/eva/engine/analysis.ml
index aee5de68bf0f43530d7fad97ae8be115ad7c227a..de72e68303aecbedcf173f33f8fa3c3dcc470063 100644
--- a/src/plugins/eva/engine/analysis.ml
+++ b/src/plugins/eva/engine/analysis.ml
@@ -236,4 +236,4 @@ let main () =
if Parameters.ForceValues.get () then compute ();
if is_computed () then Red_statuses.report ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/src/plugins/eva/engine/iterator.ml b/src/plugins/eva/engine/iterator.ml
index f17c7e4f86e72193b7c2f989cd578e98f6aa784e..de1a942094da8c318b35f1c24c9e6e110106842b 100644
--- a/src/plugins/eva/engine/iterator.ml
+++ b/src/plugins/eva/engine/iterator.ml
@@ -438,7 +438,7 @@ module Make_Dataflow
let {edge_transition=transition; edge_kinstr=kinstr} = e in
let tank = get_edge_data e in
let flow = Partitioning.drain tank in
- Db.yield ();
+ Async.yield ();
check_signals ();
current_ki := kinstr;
Cil.CurrentLoc.set e.edge_loc;
diff --git a/src/plugins/eva/utils/results.mli b/src/plugins/eva/utils/results.mli
index 122dfe95a676937703d5ddf4261f7a88147923c1..b091f95830f1e2c6846970a94b84bbafc81e4072 100644
--- a/src/plugins/eva/utils/results.mli
+++ b/src/plugins/eva/utils/results.mli
@@ -23,14 +23,7 @@
[@@@ api_start]
(** Eva's result API is a new interface to access the results of an analysis,
- once it is completed. It may slightly change in the future. It aims at
- replacing most uses of [Db.Value], and has some advantages over Db's :
-
- - evaluations uses every available domains and not only Cvalue;
- - the caller may distinguish failure cases when a request is unsucessful;
- - working with callstacks is easy;
- - some common shortcuts are provided (e.g. for extracting ival directly);
- - overall, individual functions are simpler.
+ once it is completed. It may slightly change in the future.
The idea behind this API is that requests must be decomposed in several
steps. For instance, to evaluate an expression :
diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index af8c23cbca592da73d5a42f76f7275a57d30082f..4060d0d518378c27d35ebfd9724579e3e3f6354a 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -323,7 +323,7 @@ struct
~exact access state.deps_table loc deps }
let transfer_call stmt dest f args _loc state =
- Db.yield ();
+ Async.yield ();
let request = To_Use.stmt_request stmt in
let called_vinfos = Eva.Results.(eval_callee f request |> default []) in
let f_deps = Eva.Results.expr_deps f request in
@@ -424,7 +424,7 @@ struct
result
let transfer_instr stmt (i: instr) (state: t) =
- Db.yield ();
+ Async.yield ();
match i with
| Set (lv, exp, _) ->
let comp_vars = find stmt state.deps_table exp in
@@ -643,7 +643,7 @@ struct
s := !s^" <-"^(Format.asprintf "%a" Kernel_function.pretty kf))
call_stack;
!s);
- Db.yield ();
+ Async.yield ();
let result =
if Eva.Analysis.use_spec_instead_of_definition kf
then compute_using_prototype kf
@@ -652,7 +652,7 @@ struct
let result = To_Use.cleanup_and_save kf result in
From_parameters.feedback
"Done for function %a" Kernel_function.pretty kf;
- Db.yield ();
+ Async.yield ();
CurrentLoc.set call_site_loc;
result
diff --git a/src/plugins/from/from_register.ml b/src/plugins/from/from_register.ml
index 003c0d78fcf236517599ece74cf28a5978abb668..df9beea20f8bd31766c25136d413db7fb06a2b9f 100644
--- a/src/plugins/from/from_register.ml
+++ b/src/plugins/from/from_register.ml
@@ -158,7 +158,7 @@ let main () =
if not_quiet then print_calldeps ();
)
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(*
Local Variables:
diff --git a/src/plugins/gui/analyses_manager.ml b/src/plugins/gui/analyses_manager.ml
index 2c315fb4090b271d29b39ade604ffe4a40a6cbd1..6bfc77e2fc3dc06b7bda3a78bbf8437495f1998e 100644
--- a/src/plugins/gui/analyses_manager.ml
+++ b/src/plugins/gui/analyses_manager.ml
@@ -43,7 +43,7 @@ let run title filter_name extension loader
| `EXECUTE ->
let run f =
loader f;
- !Db.Main.play ();
+ Boot.play_analysis ();
host_window#reset ()
in
Option.iter run dialog#filename;
@@ -68,7 +68,7 @@ let insert (main_ui: Design.main_window_extension_points) =
(Menu_manager.Unit_callback (fun () -> run_module main_ui));
Menu_manager.toolbar ~sensitive:(fun () -> !stop_sensitive) ~icon:`STOP
~label:"Stop" ~tooltip:"Stop currently running analyses"
- (Menu_manager.Unit_callback Db.cancel)
+ (Menu_manager.Unit_callback Async.cancel)
]
in
default_analyses_items.(0)#add_accelerator `CONTROL 'r';
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index 2442eb86f7141a0e31f1af8e7d7047843abaa5d5..a86b95b86cee8f229072c1a88fc6493f94910330 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -1885,7 +1885,7 @@ let make_splash () =
let toplevel play =
Gtk_helper.Configuration.load ();
- ignore (Db.on_progress Gtk_helper.refresh_gui) ;
+ ignore (Async.on_progress Gtk_helper.refresh_gui) ;
let in_idle () =
let tid, splash_out, splash_w, reparent_console, force_s= make_splash () in
let error_manager =
@@ -1937,7 +1937,7 @@ let toplevel play =
ignore (Glib.Idle.add (fun () -> in_idle (); false));
GMain.Main.main ()
-let () = Db.Toplevel.run := toplevel
+let () = Boot.set_toplevel toplevel
(*
Local Variables:
diff --git a/src/plugins/gui/file_manager.ml b/src/plugins/gui/file_manager.ml
index 655eaff92af82a369c9e2d8c48a4b042c307f1ef..3feaf60108f06f9b067ea54e0e8336325c0c3973 100644
--- a/src/plugins/gui/file_manager.ml
+++ b/src/plugins/gui/file_manager.ml
@@ -49,7 +49,7 @@ let reparse (host_window: Design.main_window_extension_points) =
Kernel.Files.set [];
Kernel.Files.set files;
Ast.compute ();
- !Db.Main.play ();
+ Boot.play_analysis ();
Source_manager.clear host_window#original_source_viewer)
in
begin match old_helt, succeeded with
diff --git a/src/plugins/gui/gtk_helper.ml b/src/plugins/gui/gtk_helper.ml
index 20df4ae960110acfb74801ce47b078f327453203..fac1f1725dcd2e809613eec7688d33e937bf4b2c 100644
--- a/src/plugins/gui/gtk_helper.ml
+++ b/src/plugins/gui/gtk_helper.ml
@@ -788,7 +788,7 @@ class error_manager ?reset (o_parent:GWindow.window_skel) : host =
| Cmdline.Exit ->
if cancelable then Project.Undo.clear_breakpoint ();
None
- | Sys.Break | Db.Cancel ->
+ | Sys.Break | Async.Cancel ->
if cancelable then Project.Undo.restore ();
self#error ?parent ~reset:true
"Stopping current computation on user request.";
diff --git a/src/plugins/gui/launcher.ml b/src/plugins/gui/launcher.ml
index e6d9dbf1fb4883606dc28c0c1faea373ba7978c9..00b716d11b7fbe22d41970655c82f6aae69c8192 100644
--- a/src/plugins/gui/launcher.ml
+++ b/src/plugins/gui/launcher.ml
@@ -35,7 +35,7 @@ let run (host:basic_main) dialog () =
(fun () ->
dialog#destroy ();
Kernel_hook.apply ();
- !Db.Main.play ()));
+ Boot.play_analysis ()));
(* Even if the above operation failed, we try to reset the gui, as the
plugins might have done something before crashing *)
ignore (host#protect ~cancelable:false ~parent:(dialog :> GWindow.window_skel)
diff --git a/src/plugins/gui/menu_manager.ml b/src/plugins/gui/menu_manager.ml
index 26fc68df230d6d2aaac763921a1e6df2e4553232..56e64e53e6ade951ef9d5412d74de1c729815ca4 100644
--- a/src/plugins/gui/menu_manager.ml
+++ b/src/plugins/gui/menu_manager.ml
@@ -339,7 +339,7 @@ class menu_manager ?packing (_:Gtk_helper.host) =
else debug_item#misc#hide ()
in
reset ();
- Db.Main.extend reset
+ Boot.Main.extend reset
end
diff --git a/src/plugins/impact/compute_impact.ml b/src/plugins/impact/compute_impact.ml
index 6f78536af6a6deb3c7e433fab4d0ca57dc01c4f5..e92cbe6a932f02cab388b78e95db27681ecc3a46 100644
--- a/src/plugins/impact/compute_impact.ml
+++ b/src/plugins/impact/compute_impact.ml
@@ -581,7 +581,7 @@ let rec intraprocedural wl = match pick wl with
| Some (pnode, { kf; pdg; init; zone }) ->
let node = pnode, zone in
add_to_result wl node kf init;
- Db.yield ();
+ Async.yield ();
Options.debug ~level:2 "considering new node %a in %a:@ <%a>%t"
PdgTypes.Node.pretty pnode Kernel_function.pretty kf
Pdg_aux.pretty_node node
diff --git a/src/plugins/impact/register.ml b/src/plugins/impact/register.ml
index 3e5ff2aeb18c4aa3965443546fdeeb96014b4ec9..84f9e678d825fb51539fa4cd8e315d30d0b35049 100644
--- a/src/plugins/impact/register.ml
+++ b/src/plugins/impact/register.ml
@@ -161,7 +161,7 @@ let main () =
ignore (compute_pragmas ());
Options.feedback "analysis done"
end
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(*
Local Variables:
diff --git a/src/plugins/inout/register.ml b/src/plugins/inout/register.ml
index f93bf609e17efc98cf19d17c94995d7a188692d7..f7a1db558c624007a7d82ccc7b1cf2d61bfcb9ec 100644
--- a/src/plugins/inout/register.ml
+++ b/src/plugins/inout/register.ml
@@ -77,7 +77,7 @@ let main () =
end)
end
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(*
diff --git a/src/plugins/loop_analysis/register.ml b/src/plugins/loop_analysis/register.ml
index b643f5e21c331646a38be17b5c09630bcf0e6cd9..cc4d6ba366686a4f6dc473ffeb6f5c08b4028aeb 100644
--- a/src/plugins/loop_analysis/register.ml
+++ b/src/plugins/loop_analysis/register.ml
@@ -38,4 +38,4 @@ let main () =
end
;;
-Db.Main.extend main;;
+Boot.Main.extend main;;
diff --git a/src/plugins/markdown-report/mdr_register.ml b/src/plugins/markdown-report/mdr_register.ml
index c459ac2c91b4394d82c728606ca11450aaa67cfa..24e4880f4565fafdbceaf1ffb39362c6b785a4d7 100644
--- a/src/plugins/markdown-report/mdr_register.ml
+++ b/src/plugins/markdown-report/mdr_register.ml
@@ -31,4 +31,4 @@ let main () =
Mdr_params.Generate.option_name s
let () =
- Db.Main.extend main
+ Boot.Main.extend main
diff --git a/src/plugins/metrics/register.ml b/src/plugins/metrics/register.ml
index 618b539d408c879d9008f0538ce5f1ea24119c3a..a307a06e68aab06c7783b10303ddac970d8ee536 100644
--- a/src/plugins/metrics/register.ml
+++ b/src/plugins/metrics/register.ml
@@ -76,7 +76,7 @@ let main () =
;;
(* Register main entry points *)
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(*
diff --git a/src/plugins/nonterm/nonterm_run.ml b/src/plugins/nonterm/nonterm_run.ml
index 176678b5e498016794add8061f174db1042246fd..9f01ac05a016a02c824b9ff66af216f565138df6 100644
--- a/src/plugins/nonterm/nonterm_run.ml
+++ b/src/plugins/nonterm/nonterm_run.ml
@@ -348,4 +348,4 @@ let main () =
if Enabled.get () then run_once ()
let () =
- Db.Main.extend main
+ Boot.Main.extend main
diff --git a/src/plugins/obfuscator/obfuscator_register.ml b/src/plugins/obfuscator/obfuscator_register.ml
index 22b3e698f5ef07a053b2b626ec33fcebe58927d7..43e491e743369265dab22b83a593ca0db5be9728 100644
--- a/src/plugins/obfuscator/obfuscator_register.ml
+++ b/src/plugins/obfuscator/obfuscator_register.ml
@@ -71,7 +71,7 @@ let run () =
and by the discussion in Gitlab issue #491 *)
end
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
(*
Local Variables:
diff --git a/src/plugins/occurrence/register.ml b/src/plugins/occurrence/register.ml
index 84e2056534967d964bd941612b2a9f9c70add25c..de26bd8c7fab55bac5544a16cd096fd20dd5ddf0 100644
--- a/src/plugins/occurrence/register.ml
+++ b/src/plugins/occurrence/register.ml
@@ -132,7 +132,7 @@ class occurrence = object (self)
DoChildren
method! vstmt_aux s =
- Db.yield ();
+ Async.yield ();
super#vstmt_aux s
initializer Eva.Analysis.compute ()
@@ -249,7 +249,7 @@ let print_all = print_all
(* ************************************************************************** *)
let main _fmt = if Print.get () then print_all ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(*
Local Variables:
diff --git a/src/plugins/pdg/build.ml b/src/plugins/pdg/build.ml
index 51196e16434cfdbb459e8c6a825eb8249d8152dc..6db271d345e2405a1761dc0f0ea9be74ad26a0d8 100644
--- a/src/plugins/pdg/build.ml
+++ b/src/plugins/pdg/build.ml
@@ -875,7 +875,7 @@ module Computer
(** Compute the new state after 'instr' starting from state before 'state'.
*)
let doInstr stmt instr state =
- Db.yield ();
+ Async.yield ();
pdg_debug "doInstr sid:%d : %a" stmt.sid Printer.pp_instr instr;
match instr with
| _ when not (Eva.Results.is_reachable stmt) ->
@@ -884,12 +884,12 @@ module Computer
| Local_init (v, AssignInit i, _) ->
process_init current_pdg state stmt (Cil.var v) i
| Local_init (v, ConsInit (f, args, kind), loc) ->
- Db.yield ();
+ Async.yield ();
Cil.treat_constructor_as_func
(process_call current_pdg state stmt) v f args kind loc
| Set (lv, exp, _) -> process_asgn current_pdg state stmt lv exp
| Call (lvaloption,funcexp,argl,loc) ->
- Db.yield ();
+ Async.yield ();
process_call current_pdg state stmt lvaloption funcexp argl loc
| Code_annot _
| Skip _ -> process_skip current_pdg state stmt
diff --git a/src/plugins/pdg/pdg_tbl.ml b/src/plugins/pdg/pdg_tbl.ml
index 74245fe8a9bbe362d03bd067016a1ca55a3dce70..7fc187415b95d2b3abb07c0ee76718f7938370ef 100644
--- a/src/plugins/pdg/pdg_tbl.ml
+++ b/src/plugins/pdg/pdg_tbl.ml
@@ -33,8 +33,7 @@ module Tbl =
(PdgTypes.Pdg)
(struct
let name = "Pdg.State"
- let dependencies = [] (* postponed because !Db.From.self may
- not exist yet *)
+ let dependencies = [] (* postponed because From.self may not exist yet *)
let size = 17
end)
diff --git a/src/plugins/pdg/register.ml b/src/plugins/pdg/register.ml
index b065d1184b534cd5020fd3365a0d50030ca940ca..ad9c1cd40ad09cb28026fe7989fdd01b3332e20d 100644
--- a/src/plugins/pdg/register.ml
+++ b/src/plugins/pdg/register.ml
@@ -84,7 +84,7 @@ let main () =
(compute_once ();
Pdg_parameters.BuildAll.output output)
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(* {2 Overview}
diff --git a/src/plugins/postdominators/compute.ml b/src/plugins/postdominators/compute.ml
index c2e20b2ea2e19d21b45d4ad40ca709c1e53e13cc..ab96a7e74196a14d5b7c96a01b25e54a97cde8fd 100644
--- a/src/plugins/postdominators/compute.ml
+++ b/src/plugins/postdominators/compute.ml
@@ -120,7 +120,7 @@ struct
let combineSuccessors = DomSet.inter
let doStmt stmt =
- Db.yield ();
+ Async.yield ();
Postdominators_parameters.debug ~level:2 "doStmt: %d" stmt.sid;
match stmt.skind with
| Return _ -> Dataflow2.Done (DomSet.Value (Stmt.Hptset.singleton stmt))
diff --git a/src/plugins/postdominators/postdominators.ml b/src/plugins/postdominators/postdominators.ml
index d9273a0790d5e53a0f199245b637d219c8acdfc4..a182c3e78447f00fabd1964aaa995dc243975f53 100644
--- a/src/plugins/postdominators/postdominators.ml
+++ b/src/plugins/postdominators/postdominators.ml
@@ -39,4 +39,4 @@ let output () =
let output, _ = State_builder.apply_once "Postdominators.Compute.output"
[Compute.self] output
-let () = Db.Main.extend output
+let () = Boot.Main.extend output
diff --git a/src/plugins/reduc/register.ml b/src/plugins/reduc/register.ml
index 4595aacd8a2e12f73a352451095a39c1fc055818..8c2c574f6b5bfcaed5c8bbdfd8c1a8a402c93483 100644
--- a/src/plugins/reduc/register.ml
+++ b/src/plugins/reduc/register.ml
@@ -38,4 +38,4 @@ let main () =
()
end
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/src/plugins/report/classify.ml b/src/plugins/report/classify.ml
index 5e7ef8e3bc1159857218f3e3e3213d97a7ee9177..8a6cf8b9e4decffdd36e809510c3ebafe2969a29 100644
--- a/src/plugins/report/classify.ml
+++ b/src/plugins/report/classify.ml
@@ -574,7 +574,7 @@ let main () =
let () =
begin
Cmdline.run_after_configuring_stage register ;
- Db.Main.extend main ;
+ Boot.Main.extend main ;
end
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/report/csv.ml b/src/plugins/report/csv.ml
index df3464b57135b9a7a6327735639a4232b64949e2..6b0e644de4e98c55cd9d141c0cca34318b27fa5b 100644
--- a/src/plugins/report/csv.ml
+++ b/src/plugins/report/csv.ml
@@ -110,7 +110,7 @@ let print_csv, _ =
let main () =
if not (Report_parameters.CSVFile.is_empty ()) then print_csv ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(*
diff --git a/src/plugins/report/register.ml b/src/plugins/report/register.ml
index 7bb30f7433978bffd79585946e69db15bfcdbf6a..d19dc67fd9c8d531ddb7d2eb8ce2769472d273dc 100644
--- a/src/plugins/report/register.ml
+++ b/src/plugins/report/register.ml
@@ -47,7 +47,7 @@ let print, _ =
let main () = if Report_parameters.Print.get () then print ()
let () =
- Db.Main.extend main;
+ Boot.Main.extend main;
(*
Local Variables:
diff --git a/src/plugins/report/tests/report/multi_emitters.ml b/src/plugins/report/tests/report/multi_emitters.ml
index 9680545a9181782f63276fbecd1d738d3c498784..b8411106ae8e8b0a4a9b939b007b82940968129d 100644
--- a/src/plugins/report/tests/report/multi_emitters.ml
+++ b/src/plugins/report/tests/report/multi_emitters.ml
@@ -59,4 +59,4 @@ let main () =
set_status emitter1 Property_status.False_and_reachable;
print_status ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/src/plugins/report/tests/report/no_hyp.ml b/src/plugins/report/tests/report/no_hyp.ml
index ecc7d9b45051bd034248a154eec671e6dcf52fd7..8c5bd1a2951cfa3ef9782322e59f4715491b330a 100644
--- a/src/plugins/report/tests/report/no_hyp.ml
+++ b/src/plugins/report/tests/report/no_hyp.ml
@@ -52,4 +52,4 @@ let main () =
*)
end
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/src/plugins/report/tests/report/one_hyp.ml b/src/plugins/report/tests/report/one_hyp.ml
index 178682c5981788be687fbc5881856b6eda2fc160..48f2de3ef19731d8b3395f2397e273b2d5a953b1 100644
--- a/src/plugins/report/tests/report/one_hyp.ml
+++ b/src/plugins/report/tests/report/one_hyp.ml
@@ -223,4 +223,4 @@ let main () =
(* *********************************************************************** *)
()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/src/plugins/report/tests/report/projectified_status.ml b/src/plugins/report/tests/report/projectified_status.ml
index 643fbd6057e6cd512bce729b09b029f65113d122..8e361649e87b3e0bac19a96d240aca37b5af61ab 100644
--- a/src/plugins/report/tests/report/projectified_status.ml
+++ b/src/plugins/report/tests/report/projectified_status.ml
@@ -55,4 +55,4 @@ let main () =
set_status Property_status.Dont_know;
print_status ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/src/plugins/report/tests/report/several_hyps.ml b/src/plugins/report/tests/report/several_hyps.ml
index 929820d1c99edbf9534a97a8b7e3f64f622ceb9d..c1413df81d4ac7039fbfbbc26cac79db2dee2694 100644
--- a/src/plugins/report/tests/report/several_hyps.ml
+++ b/src/plugins/report/tests/report/several_hyps.ml
@@ -205,4 +205,4 @@ let main () =
(***************************************************************************)
test "INCONSISTENT + INCONSISTENT" (set inconsistent inconsistent)
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/src/plugins/rte/RteGen.mli b/src/plugins/rte/RteGen.mli
index dda18706daadcf48439956f31931d0ebd1b5a155..fc927c236f044cafed5879173e5e52dbbaf36457 100644
--- a/src/plugins/rte/RteGen.mli
+++ b/src/plugins/rte/RteGen.mli
@@ -58,5 +58,4 @@ module Visit : sig
code_annotation * bool
end
-(** Replaces old Db API *)
module Api : module type of Api
diff --git a/src/plugins/rte/register.ml b/src/plugins/rte/register.ml
index 27abdbadafe39fdb947327983cf2674cc6b21b2d..2019f62b4db49ceeccc28bb8f930d5def0d183b5 100644
--- a/src/plugins/rte/register.ml
+++ b/src/plugins/rte/register.ml
@@ -86,7 +86,7 @@ let main () =
"annotations computed"
end
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(*
Local Variables:
diff --git a/src/plugins/server/doc/server.md b/src/plugins/server/doc/server.md
index e0d6927a3dabf7620a4dd10892e73b4aa3c510f1..2f87f9754717c77403f6a6b87bc3b8ad43c720b1 100644
--- a/src/plugins/server/doc/server.md
+++ b/src/plugins/server/doc/server.md
@@ -38,7 +38,7 @@ asynchronous entry points, requests are classified into three kinds:
- `EXEC` to starts a resource intensive analysis in Frama-C
During an `EXEC` requests, the implementation of the all resource demanding
-computations shall repeatedly call the yielding routine `Db.yield()` of the
+computations shall repeatedly call the yielding routine `Async.yield()` of the
Frama-C kernel to ensures a smooth asynchronous behavior of the Server. During a
_yield_ call, the Server would be allowed to handle few `GET` pending requests,
since they shall be fast without any modification. When the server is idled, any
@@ -75,8 +75,8 @@ Signals will be notified in addition to responses or logical requests
or server polling.
During the execution of the Frama-C command line, the server behaves just like
-during an `EXEC` request: only `GET` requests are processed at `Db.yield()` calls
-until the (normal) termination of the command line.
+during an `EXEC` request: only `GET` requests are processed at `Async.yield()`
+calls until the (normal) termination of the command line.
## Transport Messages
@@ -144,7 +144,7 @@ provide an implementation of the non-blocking `fetch` function and create a serv
with `Server.create`. Then, you shall:
- Schedule `Server.start myServer` during the main plug-in extension phase _via_
- `Db.Main.extend`;
+ `Boot.Main.extend`;
- Schedule `Server.run myServer` at normal command line termination phase _via_
`Cmdline.at_normal_exit`;
diff --git a/src/plugins/server/main.ml b/src/plugins/server/main.ml
index 06d8471f772e6b7712291d9b7961f187290d5791..9363447b71ea9d618e8682575207ebef3f9af3f1 100644
--- a/src/plugins/server/main.ml
+++ b/src/plugins/server/main.ml
@@ -107,7 +107,7 @@ type 'a server = {
fetch : unit -> 'a message option ; (* fetch some client message *)
q_in : 'a pending Queue.t ; (* queue of pending `EXEC and `GET jobs *)
q_out : 'a response Queue.t ; (* queue of pending responses *)
- mutable daemon : Db.daemon option ; (* Db.yield daemon *)
+ mutable daemon : Async.daemon option ; (* Async.yield daemon *)
mutable s_listen : Signals.t ; (* signals the client is listening to *)
mutable s_emitted : Signals.t ; (* emitted signals enqueued *)
mutable s_pending : Signals.t ; (* emitted signals not enqueued yet *)
@@ -184,7 +184,7 @@ let execute_process server ?yield proc =
Senv.debug ~level:2 "%a" (pp_process server.pretty) proc ;
let resp = match yield with
| Some yield when proc.yield ->
- Db.with_progress
+ Async.with_progress
~debounced:server.polling
?on_delayed:(delayed proc.request)
yield run proc
@@ -231,7 +231,7 @@ let raise_if_killed = function
let kill_running ?id s =
match s.running with
| Idle -> ()
- | CmdLine -> if id = None then Db.cancel ()
+ | CmdLine -> if id = None then Async.cancel ()
| ExecRequest p ->
match id with
| None -> p.killed <- true
@@ -362,7 +362,7 @@ let rec process server =
execute_process server ~yield p
| Command cmd ->
server.running <- CmdLine ;
- Db.with_progress
+ Async.with_progress
~debounced:server.polling
?on_delayed:(delayed "<async>")
yield cmd ()
@@ -414,7 +414,7 @@ let schedule server job data =
let st =
try Task.Result (job data)
with
- | Db.Cancel -> Task.Canceled
+ | Async.Cancel -> Task.Canceled
| exn -> Task.Failed exn
in status := Task.Return st
in
@@ -455,7 +455,7 @@ let start server =
begin
Senv.feedback "Server enabled." ;
let daemon =
- Db.on_progress
+ Async.on_progress
~debounced:server.polling
?on_delayed:(delayed "command line")
(do_yield server)
@@ -480,7 +480,7 @@ let stop server =
server.daemon <- None ;
server.running <- Idle ;
server.cmdline <- None ;
- Db.off_progress daemon ;
+ Async.off_progress daemon ;
set_active false ;
end
end
@@ -493,14 +493,14 @@ let foreground server =
server.running <- Idle ;
server.cmdline <- Some false ;
emitter := do_signal server ;
- Task.on_idle := Db.while_progress ~debounced:50 ;
+ Task.on_idle := Async.while_progress ~debounced:50 ;
scheduler := Server server ;
match server.daemon with
| None -> ()
| Some daemon ->
begin
server.daemon <- None ;
- Db.off_progress daemon ;
+ Async.off_progress daemon ;
end
end
@@ -521,7 +521,7 @@ let run server =
try
while not server.shutdown do
let activity = process server in
- if not activity then Db.sleep server.polling
+ if not activity then Async.sleep server.polling
done ;
with Sys.Break -> () (* Ctr+C, just leave the loop normally *)
end;
diff --git a/src/plugins/server/main.mli b/src/plugins/server/main.mli
index 4868d732093c60bcc6317b463158c7542b55ec76..9215a456db54f9aa3020f2401f945b964f1e678e 100644
--- a/src/plugins/server/main.mli
+++ b/src/plugins/server/main.mli
@@ -94,10 +94,10 @@ val create :
(** Start the server in background.
The function returns immediately after installing a daemon that (only)
- accepts GET requests received by the server on calls to [Db.yield()].
+ accepts GET requests received by the server on calls to [Async.yield()].
Shall be scheduled at command line main stage {i via}
- [Db.Main.extend] extension point.
+ [Boot.Main.extend] extension point.
*)
val start : 'a server -> unit
@@ -114,7 +114,7 @@ val stop : 'a server -> unit
(** Run the server forever.
The server would now accept any kind of requests and start handling them.
While executing an [`EXEC] request, the server would
- continue to handle (only) [`GET] pending requests on [Db.yield()]
+ continue to handle (only) [`GET] pending requests on [Async.yield()]
at every [server.polling] time interval.
The function will {i not} return until the server is actually shutdown.
diff --git a/src/plugins/server/server_batch.ml b/src/plugins/server/server_batch.ml
index 5f1039342c9246c5c2243d0b8e70a32dc5cfa17b..855dbe38cfd397c89b10a1516bf7d3195d73100a 100644
--- a/src/plugins/server/server_batch.ml
+++ b/src/plugins/server/server_batch.ml
@@ -126,6 +126,6 @@ let execute () =
(* --- Run the Server from the Command line --- *)
(* -------------------------------------------------------------------------- *)
-let () = Db.Main.extend execute
+let () = Boot.Main.extend execute
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/server_doc.ml b/src/plugins/server/server_doc.ml
index 52eb8613929beaab64f7de7c011f12b6a546f873..7a6617155ee3f52357b04063a1a9992e344f6003 100644
--- a/src/plugins/server/server_doc.ml
+++ b/src/plugins/server/server_doc.ml
@@ -383,7 +383,7 @@ let dump ~root ?(meta=true) () =
end
let () =
- Db.Main.extend begin
+ Boot.Main.extend begin
fun () ->
if not (Senv.Doc.is_empty ()) then
let root = Senv.Doc.get () in
diff --git a/src/plugins/server/server_socket.ml b/src/plugins/server/server_socket.ml
index 2337dbdb92dda2b2c435be532a16d344557f0667..74394943bb2f274858574210d3d09ac18c8d42cc 100644
--- a/src/plugins/server/server_socket.ml
+++ b/src/plugins/server/server_socket.ml
@@ -336,6 +336,6 @@ let cmdline () =
(Printexc.to_string exn)
end
-let () = Db.Main.extend cmdline
+let () = Boot.Main.extend cmdline
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/server_zmq.ok.ml b/src/plugins/server/server_zmq.ok.ml
index 04bf6496e9f681b54439603ffddf3b5dc5088272..340aec48868f73b4dc44e0ab1c994676692d07f6 100644
--- a/src/plugins/server/server_zmq.ok.ml
+++ b/src/plugins/server/server_zmq.ok.ml
@@ -212,6 +212,6 @@ let cmdline () =
if cmd <> "" then launch_client cmd ;
end
-let () = Db.Main.extend cmdline
+let () = Boot.Main.extend cmdline
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/slicing/api.mli b/src/plugins/slicing/api.mli
index a09fa2b1cb965fd4d3136613d88a645fbe9b5564..9b36bbdb6b32e38f47fdaa55de167f0f70b37f02 100644
--- a/src/plugins/slicing/api.mli
+++ b/src/plugins/slicing/api.mli
@@ -50,7 +50,7 @@ module Project : sig
@raise SlicingTypes.WrongSlicingLevel if [n] is not valid. *)
val change_slicing_level : Cil_types.kernel_function -> int -> unit
- (** Build a new [Db.Project.t] from all [Slice.t] of a project.
+ (** Build a new [Project.t] from all [Slice.t] of a project.
Can optionally specify how to name the sliced functions
by defining [f_slice_names].
[f_slice_names kf src_visi num_slice] has to return the name
diff --git a/src/plugins/slicing/register.ml b/src/plugins/slicing/register.ml
index 42bcad35768e1b6f33a2f02a58d253fd36fb65f5..716d0e00e99ceaff9a1e4f7665ae73fd123c1d3d 100644
--- a/src/plugins/slicing/register.ml
+++ b/src/plugins/slicing/register.ml
@@ -60,7 +60,7 @@ let main () =
end
(** Register the function [main] as a main entry point. *)
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(* {2 Overview}
diff --git a/src/plugins/slicing/slicingCmds.mli b/src/plugins/slicing/slicingCmds.mli
index f7c09dd5d8d44cfae8d7f01aac1033d0b3ca71ec..1643eef87f1a9137962404ddaafb208ce1250e48 100644
--- a/src/plugins/slicing/slicingCmds.mli
+++ b/src/plugins/slicing/slicingCmds.mli
@@ -28,7 +28,7 @@ open Pdg_types
is too vast and must be simplified. For example, functions should not
receive variables as names (ie. strings) but directly as zones, possibly
with a hint to the function that does to conversion. Also, most functions
- are slightly modified in Register, then registered in Db. This module and
+ are slightly modified in Register. This module and
Register should be fused. *)
type set = SlicingTypes.Fct_user_crit.t Cil_datatype.Varinfo.Map.t
diff --git a/src/plugins/slicing/slicingInternals.mli b/src/plugins/slicing/slicingInternals.mli
index e95e7e115ba72039b783b304846da7539d898740..7019d516155668f1c031fb98eb18bcab5f8dd5fb 100644
--- a/src/plugins/slicing/slicingInternals.mli
+++ b/src/plugins/slicing/slicingInternals.mli
@@ -21,9 +21,8 @@
(**************************************************************************)
(** {2 Internals types}
- Internals type definitions should be hidden to the outside world,
- but it is not really possible to have abstract types since Slicing has to
- use Db.Slicing functions... *)
+ Internals type definitions should be hidden to the outside world.
+*)
open Cil_datatype
diff --git a/src/plugins/slicing/slicingState.mli b/src/plugins/slicing/slicingState.mli
index 4afe0727826260baa2ffbfdc48340a5430a55e96..2e5fbafc5bc5c1e89d56b3aafc8e378765905ac9 100644
--- a/src/plugins/slicing/slicingState.mli
+++ b/src/plugins/slicing/slicingState.mli
@@ -25,15 +25,16 @@
val get: unit -> SlicingTypes.sl_project
(** Get the state of the slicing project.
- Assume it has already been initialized through {!Db.Slicing.reset_slice}. *)
+ Assume it has already been initialized through {!Slicing.Api.reset_slicing}.
+*)
val may: (unit -> unit) -> unit
(** apply the given closure if the slicing project has been initialized through
- {!Db.Slicing.reset_slice}. *)
+ {!Slicing.Api.reset_slicing}. *)
val may_map: none:'a -> (unit -> 'a) -> 'a
(** apply the given closure if the slicing project has been initialized through
- {!Db.Slicing.reset_slice}, or else return the default value.*)
+ {!Slicing.Api.reset_slicing}, or else return the default value.*)
val self: State.t
(** Internal state of the slicing tool from project viewpoints.
diff --git a/src/plugins/slicing/slicingTypes.mli b/src/plugins/slicing/slicingTypes.mli
index ce42a918acf0f228645dd4b8ecca2ecaea755bf3..c8be622febe9d45e68dee7b40ad84117768d2a81 100644
--- a/src/plugins/slicing/slicingTypes.mli
+++ b/src/plugins/slicing/slicingTypes.mli
@@ -39,10 +39,7 @@ exception NoPdg
(** {2 Public types} *)
(** These types are the only one that should be used by the API functions.
- Public type definitions should be hidden to the outside world,
- but it is not really possible to have abstract types since Slicing has to
- use Db.Slicing functions... So, it is up to the user of this module to use
- only this public part.
+ Public type definitions should be hidden to the outside world.
*)
(** contains global things that has been computed so far
diff --git a/src/plugins/sparecode/register.ml b/src/plugins/sparecode/register.ml
index b413b26e45126b3d60f2e70442d5a8a019e99351..9cfc87fef111b9a9d01dec19534ffa4ed8eea314 100644
--- a/src/plugins/sparecode/register.ml
+++ b/src/plugins/sparecode/register.ml
@@ -98,7 +98,7 @@ let main () =
File.pretty_ast ~prj:new_proj ()
end
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(*
Local Variables:
diff --git a/src/plugins/users/users_register.ml b/src/plugins/users/users_register.ml
index 25fd111322f8f8abfc1fc2e866dc0fd388b8e707..9cb63d7e0d9696da87f1086abcbb54771e8e5313 100644
--- a/src/plugins/users/users_register.ml
+++ b/src/plugins/users/users_register.ml
@@ -110,7 +110,7 @@ let print () =
let print_once, _self_print =
State_builder.apply_once "Users_register.print" [ Users.self ] print
-let () = Db.Main.extend print_once
+let () = Boot.Main.extend print_once
(*
Local Variables:
diff --git a/src/plugins/variadic/tests/declared/called_in_ghost.ml b/src/plugins/variadic/tests/declared/called_in_ghost.ml
index 4aa4ac68015e0d5c4aa32f616f850e0f41f3456a..24b8ad9579f09e0fda4f78e2437bc99392102693 100644
--- a/src/plugins/variadic/tests/declared/called_in_ghost.ml
+++ b/src/plugins/variadic/tests/declared/called_in_ghost.ml
@@ -37,4 +37,4 @@ class print =
let run () = Visitor.visitFramacFileSameGlobals (new print) (Ast.get())
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index bb251b1e1789b5725c01c33d46a3261ee25cc7d3..461d4303122d3a9b69f716b5b366c9e53eb4afc8 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -1164,7 +1164,7 @@ end
let rec fixpoint limit solvers sigma s0 =
if limit > 0 then compute limit solvers sigma s0 else s0
and compute limit solvers sigma s0 =
- Db.yield ();
+ Async.yield ();
let s1 =
if Wp_parameters.Ground.get () then ground s0
else s0 in
@@ -1227,7 +1227,7 @@ let tc = ref 0
let rec test_cases (s : hsp) = function
| [] -> s
| (p,_) :: tail ->
- Db.yield () ;
+ Async.yield () ;
match test_case p s , test_case (p_not p) s with
| None , None -> incr tc ; [],F.p_true
| Some w , None -> incr tc ; test_cases w tail
diff --git a/src/plugins/wp/RegionAnalysis.ml b/src/plugins/wp/RegionAnalysis.ml
index d476d72a07963e1cdc3355c0c63857a238f92513..50bc432573eac4fecacf885f01ec8c541c11f3cd 100644
--- a/src/plugins/wp/RegionAnalysis.ml
+++ b/src/plugins/wp/RegionAnalysis.ml
@@ -111,6 +111,6 @@ let main () =
) ;
end
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(* ---------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index eca897451ea5a8d0498ad46dc1526b67ada578f2..1823763111f162e7261f4cba82782fac30b490f9 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -1031,6 +1031,6 @@ let main =
]
let () = Cmdline.at_normal_exit do_cache_cleanup
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(* ------------------------------------------------------------------------ *)
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test.ml b/src/plugins/wp/tests/wp/stmtcompiler_test.ml
index db4668d7326f8d28db6b399a1ffb5d17fda5c679..4ab9acd47ce62ac91057617cf0fe1578d02c0aa6 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test.ml
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test.ml
@@ -149,4 +149,4 @@ let turn_off_populate () =
let () = Cmdline.run_after_configuring_stage turn_off_populate
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
index 3e167f78bf94d7e2e68dfd7ce6c25f60653a1ed1..369d710cdd7fdf82a6d78fc37a061e96c2e195e5 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
@@ -162,4 +162,4 @@ let run () =
ordered_kf
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index aa558367890b812aec77a6c21dd81f4f8ec083f6..8eab81d849685d385cb46cb915e8370ae914f8b5 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -1300,7 +1300,7 @@ let print_generated ?header file =
let protect e =
if debug_atleast 1 then false else
match e with
- | Sys.Break | Db.Cancel | Log.AbortError _ | Log.AbortFatal _ -> false
+ | Sys.Break | Async.Cancel | Log.AbortError _ | Log.AbortFatal _ -> false
| _ -> true
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index 94995e8bb72c47a7ee64e08cdbac4866b01a4fce..7dc808882fd5efbe61ff6ccc72cef48d287013f5 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -150,7 +150,7 @@ struct
let apply option phi g =
try
- Db.yield () ;
+ Async.yield () ;
Wp_parameters.debug ~dkey "Apply %s" option ;
g.sequent <- phi g.sequent ;
with exn when Wp_parameters.protect exn ->
diff --git a/tests/builtins/big_local_array_script.ml b/tests/builtins/big_local_array_script.ml
index dd8183d8e506894079b751a435730d199ae22a04..3654187155ecb9e02f8d730dfc78bcaa4af9df44 100644
--- a/tests/builtins/big_local_array_script.ml
+++ b/tests/builtins/big_local_array_script.ml
@@ -6,4 +6,4 @@ let foo () =
File.init_from_c_files [File.from_filename f]
end
-let () = Db.Main.extend foo
+let () = Boot.Main.extend foo
diff --git a/tests/callgraph/function_pointer.ml b/tests/callgraph/function_pointer.ml
index c2b8ca966bd971e147c8f49ee8aeb94f7af9e0ff..168be205dbb456f3eeabff4c9990fed028d18424 100644
--- a/tests/callgraph/function_pointer.ml
+++ b/tests/callgraph/function_pointer.ml
@@ -1,4 +1,4 @@
let main () =
Format.printf "number of calls = %d@." (Callgraph.Uses.nb_calls ())
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/cil/Change_formals.ml b/tests/cil/Change_formals.ml
index f224e4bcfca28421dbd9967f5624a0e485d8cccb..fe51268692588c39cf096254d141c2672d8710fa 100644
--- a/tests/cil/Change_formals.ml
+++ b/tests/cil/Change_formals.ml
@@ -88,7 +88,7 @@ let main () =
if Project.get_name (Project.current()) <> "test" then
ignore (generate_code "test")
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(*
Local Variables:
diff --git a/tests/cil/change_to_instr.ml b/tests/cil/change_to_instr.ml
index 04d2679952d844a376299eb5e32449b829314e9a..85f19109e0f142708efddda38da2ef5813fffb8b 100644
--- a/tests/cil/change_to_instr.ml
+++ b/tests/cil/change_to_instr.ml
@@ -14,4 +14,4 @@ let run () =
Visitor.visitFramacFileSameGlobals (new add_skip) (Ast.get())
let () =
- Db.Main.extend run
+ Boot.Main.extend run
diff --git a/tests/cil/insert_formal.ml b/tests/cil/insert_formal.ml
index a4796d9b33bb2fdf068980b0230a25f860cba669..311f8c041013ab8b03207ae341bcaf946a947fac 100644
--- a/tests/cil/insert_formal.ml
+++ b/tests/cil/insert_formal.ml
@@ -57,4 +57,4 @@ let update_func f =
let run () =
Globals.Functions.iter_on_fundecs update_func
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/cil/mkBinOp.ml b/tests/cil/mkBinOp.ml
index 7ef013171d3ffcb3393faadca7654fcbb964c638..e07f3b60ab1e197091d8b5bce1575e49dc8d8bd7 100644
--- a/tests/cil/mkBinOp.ml
+++ b/tests/cil/mkBinOp.ml
@@ -40,4 +40,4 @@ let main () =
test cone ione;
test ione cone
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/cil/queue_ghost_instr.ml b/tests/cil/queue_ghost_instr.ml
index f8a486d3fe77663beff1fa0c8e18168a44c1bf7d..78dfc0eeb16cf32a9301bbb1cc595975da5b9c08 100644
--- a/tests/cil/queue_ghost_instr.ml
+++ b/tests/cil/queue_ghost_instr.ml
@@ -24,4 +24,4 @@ let run () =
Visitor.visitFramacFileSameGlobals (new add_skip) (Ast.get())
let () =
- Db.Main.extend run
+ Boot.Main.extend run
diff --git a/tests/constant_propagation/introduction_of_non_explicit_cast.ml b/tests/constant_propagation/introduction_of_non_explicit_cast.ml
index 2d20a43cb00819d2370fd19c4a2e2db7e2b4f880..425a359bd354165fc4e26b06d8e5050f6304d030 100644
--- a/tests/constant_propagation/introduction_of_non_explicit_cast.ml
+++ b/tests/constant_propagation/introduction_of_non_explicit_cast.ml
@@ -10,4 +10,4 @@ let main _ =
();
File.pretty_ast ~prj:new_proj ();;
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/crowbar/mutable_const_fail.ml b/tests/crowbar/mutable_const_fail.ml
index 453fa5f48395e14b1a3f3adcadca1228a9d2e434..1b8ed9cb196e9088339e739812e246b5d54226a8 100644
--- a/tests/crowbar/mutable_const_fail.ml
+++ b/tests/crowbar/mutable_const_fail.ml
@@ -15,4 +15,4 @@ let main () =
(Cil.typeHasAttribute "const" (Cil.typeOffset x.vtype offset))
| _ -> assert false
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/crowbar/mutable_mutable_fail.ml b/tests/crowbar/mutable_mutable_fail.ml
index a3c06d6424eeda5e5c4268f5af98c0af9fbc74ae..b72ff4783dac1d229a8a18577676f652427f6358 100644
--- a/tests/crowbar/mutable_mutable_fail.ml
+++ b/tests/crowbar/mutable_mutable_fail.ml
@@ -15,4 +15,4 @@ let main () =
(not (Cil.typeHasAttribute "const" (Cil.typeOffset x.vtype offset)))
| _ -> assert false
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/dynamic/abstract2.ml b/tests/dynamic/abstract2.ml
index 73293f6f62db4ff66140644d78c423ab6c181980..f3f0f72b3e4a76c0c8dd1369a12c864672381771 100644
--- a/tests/dynamic/abstract2.ml
+++ b/tests/dynamic/abstract2.ml
@@ -30,4 +30,4 @@ let main () =
()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/float/fval_test.ml b/tests/float/fval_test.ml
index 6ce0dc57be049a58c3884d46b551637628452564..edf9e20adaee3abddd7e38a5302f496695f26c2b 100644
--- a/tests/float/fval_test.ml
+++ b/tests/float/fval_test.ml
@@ -277,4 +277,4 @@ let main _ =
test_forward_comp ();
;;
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/jcdb/jcdb.ml b/tests/jcdb/jcdb.ml
index d9163defa210d991acf8362bd59ac34d9f9c57ac..b5eceabbdf7f201d47c6db5334cf566e3ef0675e 100644
--- a/tests/jcdb/jcdb.ml
+++ b/tests/jcdb/jcdb.ml
@@ -10,4 +10,4 @@ let run () =
let prj = Project.create_by_copy ~last:true "copy" in
Project.on prj print_json ()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/libc/check_compliance.ml b/tests/libc/check_compliance.ml
index 7a13be06edfa6eefa75872796092c46e78abe1f7..e75f6dac805235d5831fcb4fc83bc33c6aa3cad9 100644
--- a/tests/libc/check_compliance.ml
+++ b/tests/libc/check_compliance.ml
@@ -124,7 +124,7 @@ let check_ident c11 posix glibc nonstandard c11_headers id headers =
end
let () =
- Db.Main.extend (fun () ->
+ Boot.Main.extend (fun () ->
if not !run_once then begin
run_once := true;
let vis = new stdlib_visitor in
diff --git a/tests/libc/check_const.ml b/tests/libc/check_const.ml
index 9be7b2b2cf3ab2debf77a764ef0d4fe04f02eecc..6996d5ed0326d36527c4ac9f2521463a66dc03b6 100644
--- a/tests/libc/check_const.ml
+++ b/tests/libc/check_const.ml
@@ -68,4 +68,4 @@ let check () =
in
Globals.Functions.iter check_kf
-let () = Db.Main.extend check
+let () = Boot.Main.extend check
diff --git a/tests/libc/check_libc_anonymous_tags.ml b/tests/libc/check_libc_anonymous_tags.ml
index c57db98104c49e29b04fa97b48f459248f6b4fd9..8e59f646a944c1c3a4464672beced4ff5349350b 100644
--- a/tests/libc/check_libc_anonymous_tags.ml
+++ b/tests/libc/check_libc_anonymous_tags.ml
@@ -50,7 +50,7 @@ end
let run_once = ref false
let () =
- Db.Main.extend (fun () ->
+ Boot.Main.extend (fun () ->
if not !run_once then begin
run_once := true;
Visitor.visitFramacFile (new tags_visitor) (Ast.get ())
diff --git a/tests/libc/check_libc_naming_conventions.ml b/tests/libc/check_libc_naming_conventions.ml
index b4f0bdbd1988e9dee39c410f4e17810aab53f5d8..bb8b128d2960a1baded2d1a0b9fd84d5db0b14ce 100644
--- a/tests/libc/check_libc_naming_conventions.ml
+++ b/tests/libc/check_libc_naming_conventions.ml
@@ -46,7 +46,7 @@ let check_separated =
let run_once = ref false
let () =
- Db.Main.extend (fun () ->
+ Boot.Main.extend (fun () ->
if not !run_once then begin
run_once := true;
Globals.Functions.fold (fun kf () ->
diff --git a/tests/libc/check_parsing_individual_headers.ml b/tests/libc/check_parsing_individual_headers.ml
index 8c18407a7c3570bca2d96930ab0f6c28d5e85865..3f9c35918acef2fdf3f119c27689c2d6d7f5fd3d 100644
--- a/tests/libc/check_parsing_individual_headers.ml
+++ b/tests/libc/check_parsing_individual_headers.ml
@@ -45,4 +45,4 @@ let collect_headers () =
) all_headers
let () =
- Db.Main.extend collect_headers
+ Boot.Main.extend collect_headers
diff --git a/tests/misc/Debug_category.ml b/tests/misc/Debug_category.ml
index c3ab6699cdcf5d62e36ddf353bf4201f736b5f77..01515996ec887e0b04587bb5712cdf435c66b4d6 100644
--- a/tests/misc/Debug_category.ml
+++ b/tests/misc/Debug_category.ml
@@ -43,4 +43,4 @@ let run () =
feedback ~dkey "D is enabled";
warning ~wkey "Another Warning A"
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/misc/add_assigns.ml b/tests/misc/add_assigns.ml
index d129f05a877ac00f90d79bc0ba48f6a62591dfa1..fdcf2b0c5d8a47c3135d2f6f528f6acb034706b5 100644
--- a/tests/misc/add_assigns.ml
+++ b/tests/misc/add_assigns.ml
@@ -33,4 +33,4 @@ let main () =
Property_status.(emit emitter ~hyps:[] ip True)
end
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/misc/behavior_names.ml b/tests/misc/behavior_names.ml
index 079fb42f5e3a8c26cb4d5b0a231a582e08ba8e61..8c1b1578e44040204b9e91c008b6e1aeb694f346 100644
--- a/tests/misc/behavior_names.ml
+++ b/tests/misc/behavior_names.ml
@@ -10,4 +10,4 @@ let run () =
(Annotations.fresh_behavior_name kf "foo")
(Annotations.fresh_behavior_name kf "bla")
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/misc/bts0489.ml b/tests/misc/bts0489.ml
index 224c74f4289c413958bf7e141380d34e00949465..cb02f561c1223b0876d439044040e5db8240fc06 100644
--- a/tests/misc/bts0489.ml
+++ b/tests/misc/bts0489.ml
@@ -17,4 +17,4 @@ let run () =
let file = Ast.get () in
Visitor.visitFramacFile (new visitor) file
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/misc/bts1201.ml b/tests/misc/bts1201.ml
index 8cb421763f5dc9c46a3c61679a6413b458875578..9358eb15ac52523d94d9c705b142142f512702a2 100644
--- a/tests/misc/bts1201.ml
+++ b/tests/misc/bts1201.ml
@@ -4,4 +4,4 @@ let main () =
Eva.Analysis.compute ();
;;
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/misc/bts1347.ml b/tests/misc/bts1347.ml
index ea417ba7710a999aa54681cf88770f622473b46f..b89b9009d34d9dc3f4a9b9fbecf6593eb6a3aca6 100644
--- a/tests/misc/bts1347.ml
+++ b/tests/misc/bts1347.ml
@@ -25,4 +25,4 @@ let run () =
end)
let () =
- Db.Main.extend run
+ Boot.Main.extend run
diff --git a/tests/misc/bug_0209.ml b/tests/misc/bug_0209.ml
index b46478f7925e914d25506a3200d3d9e87b55885f..88601d0e0687b81c0e55a8ab30421c6cd01fae49 100644
--- a/tests/misc/bug_0209.ml
+++ b/tests/misc/bug_0209.ml
@@ -13,4 +13,4 @@ let main () =
Logic_env.Builtins is not projectified) *)
Project.on p Ast.compute ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/misc/callsite.ml b/tests/misc/callsite.ml
index c906a333c79cdbc7b004e95ccfe1496de65f0cf6..4e839e8c33766d6e92832de24c7380754ad9c3bc 100644
--- a/tests/misc/callsite.ml
+++ b/tests/misc/callsite.ml
@@ -16,4 +16,4 @@ let main () =
Ast.compute () ;
List.iter dump ["f";"g";"h";"k"]
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/misc/change_main.ml b/tests/misc/change_main.ml
index ac7fba803c66a0b3a6d79d93cdda3118cb3d19db..cfc236e625f9057be89c97065706c7f2096c55f3 100644
--- a/tests/misc/change_main.ml
+++ b/tests/misc/change_main.ml
@@ -11,4 +11,4 @@ let run () =
(File.create_project_from_visitor
"change_main" (fun prj -> new visitor prj))
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/misc/cil_builder.ml b/tests/misc/cil_builder.ml
index 571edd890e7d77048cac3fd1376645a59e2eab64..3f3bdb9afceb8a130ab76fd704f4d1057cf8d08c 100644
--- a/tests/misc/cil_builder.ml
+++ b/tests/misc/cil_builder.ml
@@ -18,4 +18,4 @@ let run () =
let () =
- Db.Main.extend run
+ Boot.Main.extend run
diff --git a/tests/misc/cli_string_multiple_map.ml b/tests/misc/cli_string_multiple_map.ml
index e8f5b806e8358fdc021fe1977576213b1b93f109..32771550a04aaa8a069987a52b8357872be20888 100644
--- a/tests/misc/cli_string_multiple_map.ml
+++ b/tests/misc/cli_string_multiple_map.ml
@@ -32,4 +32,4 @@ let main () =
in
Datatype.String.Map.iter print (M.get ())
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/misc/copy_kf.ml b/tests/misc/copy_kf.ml
index 84eef5538f096ec0107928b835f597a9c662520d..b06b24d64dbf3c3213af4927f553fe358a0f162f 100644
--- a/tests/misc/copy_kf.ml
+++ b/tests/misc/copy_kf.ml
@@ -53,4 +53,4 @@ let main () =
Kernel.feedback "After replacement:@\n%t"
(fun fmt -> File.pretty_ast ~fmt ())
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/misc/copy_machdep.ml b/tests/misc/copy_machdep.ml
index 9843d085b1e85bbb4cca3d1c49fdb0e15fcda88b..63d674cf07ba768f453d41eb778b371ff9ba7979 100644
--- a/tests/misc/copy_machdep.ml
+++ b/tests/misc/copy_machdep.ml
@@ -13,4 +13,4 @@ let run () =
(if Kernel.Unicode.get () = Project.on proj Kernel.Unicode.get () then
"" else "not ")
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/misc/ensures.ml b/tests/misc/ensures.ml
index 61dfa1768fa4a977aab7240a422d22f1d46e8314..ca6ed24e40feabcb1e89b30899a15e9f04f6cfc3 100644
--- a/tests/misc/ensures.ml
+++ b/tests/misc/ensures.ml
@@ -21,4 +21,4 @@ let run () =
function_name Property_status.pretty status)
ip)
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/misc/find_enclosing_loop.ml b/tests/misc/find_enclosing_loop.ml
index bf97a89df6479fba8dcfeb7cb317fba07fb3f6cc..fe869a1f1bef88f9d0cb0e3d89ac24c9a7282f85 100644
--- a/tests/misc/find_enclosing_loop.ml
+++ b/tests/misc/find_enclosing_loop.ml
@@ -30,4 +30,4 @@ let run () =
Visitor.visitFramacFileSameGlobals (new check) (Ast.get());
Kernel.result "Script done"
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/misc/global_decl_loc.ml b/tests/misc/global_decl_loc.ml
index afe0d309b5e8b570901a9fad9eaa53b264a969ee..6e51a976ceae8728fd025e6275f8bc3ffff9fdd3 100644
--- a/tests/misc/global_decl_loc.ml
+++ b/tests/misc/global_decl_loc.ml
@@ -8,4 +8,4 @@ let run () =
Printer.pp_location vi.vdecl
)
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/misc/init_from_cil.ml b/tests/misc/init_from_cil.ml
index b64d3776a9de481781db197742c069a77e68d120..8f1c10e8d02f20232e08f2e487b89ab56b5c4771 100644
--- a/tests/misc/init_from_cil.ml
+++ b/tests/misc/init_from_cil.ml
@@ -5,4 +5,4 @@ let run () =
Project.set_current prj;
Printer.pp_file Format.std_formatter (Ast.get())
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/misc/interpreted_automata_dataflow_backward.ml b/tests/misc/interpreted_automata_dataflow_backward.ml
index 43e96ba1a24aa9b14808047fb4b9f26b6b73f360..dce5e8cfc2b03a89b957de3e4c16fe25a09e3071 100644
--- a/tests/misc/interpreted_automata_dataflow_backward.ml
+++ b/tests/misc/interpreted_automata_dataflow_backward.ml
@@ -70,4 +70,4 @@ let run () =
Dataflow.Result.to_dot_file LivenessDomain.pretty results filepath
let () =
- Db.Main.extend run
+ Boot.Main.extend run
diff --git a/tests/misc/interpreted_automata_dataflow_forward.ml b/tests/misc/interpreted_automata_dataflow_forward.ml
index 6470ee925904435745bd9ead0d9d7a33cf929d00..97678ef9abb1e9e2e6c4d626c5600abf3ac13d53 100644
--- a/tests/misc/interpreted_automata_dataflow_forward.ml
+++ b/tests/misc/interpreted_automata_dataflow_forward.ml
@@ -120,4 +120,4 @@ let run () =
ConstantsDomain.pretty result
let () =
- Db.Main.extend run
+ Boot.Main.extend run
diff --git a/tests/misc/issue109.ml b/tests/misc/issue109.ml
index 290543f644af55ef65b3fca95563f627c4f17f59..cf379082ec0a407dca4e3670b79adc3348741148 100644
--- a/tests/misc/issue109.ml
+++ b/tests/misc/issue109.ml
@@ -5,4 +5,4 @@ let main () =
File.init_from_cmdline ();
Eva.Analysis.compute ()
-let main = Db.Main.extend main
+let main = Boot.Main.extend main
diff --git a/tests/misc/justcopy.ml b/tests/misc/justcopy.ml
index 297c7fed4a45df97b8970a4a78a31a0a6d8cf6f4..9597d33f3c7dde54c9eb2d3fdac7c14f53dbbab5 100644
--- a/tests/misc/justcopy.ml
+++ b/tests/misc/justcopy.ml
@@ -7,4 +7,4 @@ let main () =
in
ignore (File.create_project_from_visitor "justcopy" o)
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/misc/log_twice.ml b/tests/misc/log_twice.ml
index 73238757c077b193a9a5ea1cfd9be83778134585..67bb3b984883dad3a98ecfd1278272e9479da2c0 100644
--- a/tests/misc/log_twice.ml
+++ b/tests/misc/log_twice.ml
@@ -13,4 +13,4 @@ let run () =
Eva.Analysis.compute ();
()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/misc/my_visitor.ml b/tests/misc/my_visitor.ml
index 832c2104127e461c46e5e120a9e9868262897194..c2248a4ebc119d082c215d70662ce313ab5fe2d4 100644
--- a/tests/misc/my_visitor.ml
+++ b/tests/misc/my_visitor.ml
@@ -81,7 +81,7 @@ let main () =
print ()
end
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(* This other main is a simple test for deep copy. *)
@@ -95,4 +95,4 @@ let main () =
assert (Project.on p ~selection (fun () -> not (Kernel.LibEntry.get ())) ())
end
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/misc/orphan_emitter.ml b/tests/misc/orphan_emitter.ml
index 2fd3673ffa30e0005f7e38f8b3663104e5dce937..5c31565debc4da05f38968f730c72ef8e835f9ad 100644
--- a/tests/misc/orphan_emitter.ml
+++ b/tests/misc/orphan_emitter.ml
@@ -18,4 +18,4 @@ let main () =
let stmt = Kernel_function.find_first_stmt kf in
Annotations.add_assert emitter1 stmt Logic_const.ptrue
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/misc/plugin_log.ml b/tests/misc/plugin_log.ml
index 81908f382636d5494b21425fc938182ab0d00d38..ac6d9836317842aba5b37ac9087a2ae546aa5d5d 100644
--- a/tests/misc/plugin_log.ml
+++ b/tests/misc/plugin_log.ml
@@ -17,4 +17,4 @@ let main () =
failure "failure";*)
()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/misc/remove_status_hyps.ml b/tests/misc/remove_status_hyps.ml
index c382ddaaabc0f7b7ba73f904d9ef5b7dbbbcea1a..be52ee29bff92683bab71ee573da183e602739be 100644
--- a/tests/misc/remove_status_hyps.ml
+++ b/tests/misc/remove_status_hyps.ml
@@ -58,4 +58,4 @@ let main () =
report "removing P1" l'
| _ -> assert false
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/misc/save_comments.ml b/tests/misc/save_comments.ml
index 0c9dea658b023a88f7be802b18c95c7de552edab..cfd3e993581eef73247ed9ff74fd7172f8e33df8 100644
--- a/tests/misc/save_comments.ml
+++ b/tests/misc/save_comments.ml
@@ -40,4 +40,4 @@ let run () =
Format.printf "Printing saved project:@.";
File.pretty_ast ~prj ~fmt ()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/misc/static.ml b/tests/misc/static.ml
index 7b6f77aa5f8f1d7d362de123ec827c53e052bd70..36c84526fddb1f700c1b64111bdd721dc93055e5 100644
--- a/tests/misc/static.ml
+++ b/tests/misc/static.ml
@@ -23,4 +23,4 @@ let run () =
Kernel.fatal "mixing local variables from f and g";
File.pretty_ast ()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/misc/test_datatype.ml b/tests/misc/test_datatype.ml
index 4787ec1dbbb58ed4ef196814ab780ea26df0b2d8..04a8eeca0ea3fe4b7cfe4b80107f238026c6e1f4 100644
--- a/tests/misc/test_datatype.ml
+++ b/tests/misc/test_datatype.ml
@@ -26,4 +26,4 @@ let main () =
(* no equality in Hashtbls. *)
Test.Hashtbl.iter (fun _ _ -> assert false) (H.copy h)
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/misc/version.ml b/tests/misc/version.ml
index c51486acaecd1ccf588f1180f59d1728c5a81768..cddd787c76c38aff5d5b9bb450744645c79045fd 100644
--- a/tests/misc/version.ml
+++ b/tests/misc/version.ml
@@ -17,4 +17,4 @@ let run () =
Kernel.abort
"could not parse Fc_config.version"
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/misc/vis_queueInstr.ml b/tests/misc/vis_queueInstr.ml
index eef216849e864ac5b972d0b401683ffecbd5e7f1..6b4473fae3dfb11f25f6a96b1034d3b4f12510df 100644
--- a/tests/misc/vis_queueInstr.ml
+++ b/tests/misc/vis_queueInstr.ml
@@ -4,5 +4,5 @@ class vis prj = object(this)
end
let () =
- Db.Main.extend (fun () ->
+ Boot.Main.extend (fun () ->
ignore (File.create_project_from_visitor "A" (new vis)))
diff --git a/tests/misc/vis_spec.ml b/tests/misc/vis_spec.ml
index d8d0b2b0373de8cdb41233441db0c85f0099395b..b1f013cf8a5df9af901e113ddb89e93501582aab 100644
--- a/tests/misc/vis_spec.ml
+++ b/tests/misc/vis_spec.ml
@@ -48,4 +48,4 @@ let startup () =
Project.set_current prj;
;;
-let () = Db.Main.extend startup
+let () = Boot.Main.extend startup
diff --git a/tests/misc/visitor_creates_func_bts_1349.ml b/tests/misc/visitor_creates_func_bts_1349.ml
index 44d7b7cae636a1d6aa880f2ff6c65c01bd1914a0..ad70dd8cd73f3a148b9de2fadff5578d38f1a1de 100644
--- a/tests/misc/visitor_creates_func_bts_1349.ml
+++ b/tests/misc/visitor_creates_func_bts_1349.ml
@@ -44,4 +44,4 @@ let run () =
let vis prj = new test prj in
ignore (File.create_project_from_visitor "test" vis)
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/misc/well_typed_alarm.ml b/tests/misc/well_typed_alarm.ml
index 6c792a3d3ee8155beb6f9ba3c44e698f5d196a33..e9a1d1ba3467bbc39ac705f514d0133f71afa9b6 100644
--- a/tests/misc/well_typed_alarm.ml
+++ b/tests/misc/well_typed_alarm.ml
@@ -3,4 +3,4 @@ let main () =
Filecheck.check_ast "Check alarm";
File.pretty_ast ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/misc/with space/module.ml b/tests/misc/with space/module.ml
index b9c45d54b4c46abc1b0e634ec17b6879414a0c78..47e5c94e5b2cddf1e473683678f87c99bdc50ee5 100644
--- a/tests/misc/with space/module.ml
+++ b/tests/misc/with space/module.ml
@@ -1,3 +1,3 @@
-let () = Db.Main.extend (fun () ->
+let () = Boot.Main.extend (fun () ->
Kernel.feedback "module successfully loaded"
)
diff --git a/tests/misc/wstring_phase6.ml b/tests/misc/wstring_phase6.ml
index a7a36476e7bd7baf11e9e893971bb13722ca783b..f1e33d6a26ec54a33718c5da4afabbd862fd2f2e 100644
--- a/tests/misc/wstring_phase6.ml
+++ b/tests/misc/wstring_phase6.ml
@@ -19,4 +19,4 @@ class vis =
let do_it () = Visitor.visitFramacFileSameGlobals (new vis) (Ast.get())
-let () = Db.Main.extend do_it
+let () = Boot.Main.extend do_it
diff --git a/tests/pdg/dyn_dpds.ml b/tests/pdg/dyn_dpds.ml
index 5bf2774757d4402519d82ae1590fef2b179ca7ea..70498a8b9d7df4c2567f3f99134c210ae884c16d 100644
--- a/tests/pdg/dyn_dpds.ml
+++ b/tests/pdg/dyn_dpds.ml
@@ -42,4 +42,4 @@ let main _ =
Format.printf "%a@." (Pdg.Api.pretty ~bw:false) pdg;
Pdg.Api.extract pdg "dyn_dpds_1.dot"
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/pdg/sets.ml b/tests/pdg/sets.ml
index 23c627b3a5bb207fb6a40a3d1ec5fcd793dfbe3e..c19687a8e02f102cf506b5c9e39b3cbbadfdf10d 100644
--- a/tests/pdg/sets.ml
+++ b/tests/pdg/sets.ml
@@ -54,4 +54,4 @@ let main _ =
pp_nodes "Test [all_related_nodes] y@11" nodes
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/rte/compute_annot.ml b/tests/rte/compute_annot.ml
index 7ef362bb5864a62627fc589a2ee7e243e68b9e62..213681f5ea014d82deed4ebab5efbd95489efbab 100644
--- a/tests/rte/compute_annot.ml
+++ b/tests/rte/compute_annot.ml
@@ -38,4 +38,4 @@ let main () =
print ();
print_status ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/rte/my_annot_proxy.ml b/tests/rte/my_annot_proxy.ml
index cd22de24d55aeb20304ac0c9c47cac5a00854a52..544cedc524d73d676d906c3b45a7d20ff9296209 100644
--- a/tests/rte/my_annot_proxy.ml
+++ b/tests/rte/my_annot_proxy.ml
@@ -36,4 +36,4 @@ let main () =
print ();
print_status ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/rte/my_annotation.ml b/tests/rte/my_annotation.ml
index c1549b692964c6eb2732665b2848d4cb38f28a61..7a845bfc81448f019c3ee2c703902fee2aa8e709 100644
--- a/tests/rte/my_annotation.ml
+++ b/tests/rte/my_annotation.ml
@@ -49,4 +49,4 @@ let main () =
print () ;
print_status ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/rte/rte_get_annot.ml b/tests/rte/rte_get_annot.ml
index c360664de0dccaa55c8c903489869ccae5dba7d7..0ffabb44622aeb623304cfb67b9fe370d316a99b 100644
--- a/tests/rte/rte_get_annot.ml
+++ b/tests/rte/rte_get_annot.ml
@@ -53,4 +53,4 @@ let main () =
print () ;
Globals.Functions.iter show_rte_of_kf
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/saveload/deps_E.ml b/tests/saveload/deps_E.ml
index 1e5347ab012160175d918845265e2438e3ea3532..a0a766521b2afba0e386ed2f7e13da7d93e82f9f 100644
--- a/tests/saveload/deps_E.ml
+++ b/tests/saveload/deps_E.ml
@@ -37,4 +37,4 @@ let main () =
assert (StateB.get_option () = None); (* reset to default *)
assert (StateC.get_option () = None) (* reset because of dependency of B *)
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/saveload/load_one.ml b/tests/saveload/load_one.ml
index 12d0bb16cd9ea6f58270a01a2cb71ed3d5042f34..02186193baa7df0b46834af0aeb7af26164b4939 100644
--- a/tests/saveload/load_one.ml
+++ b/tests/saveload/load_one.ml
@@ -13,7 +13,7 @@ let main () =
let p = Project.load fp in
Project.on p (fun () -> Eva.Analysis.compute (); ignore (sparecode ())) ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(* testing Project.create_by_copy *)
let main2 () =
@@ -24,4 +24,4 @@ let main2 () =
Format.printf "COPY AST@.";
File.pretty_ast ~prj ()
-let () = Db.Main.extend main2
+let () = Boot.Main.extend main2
diff --git a/tests/saveload/multi_project.ml b/tests/saveload/multi_project.ml
index 4a7bd87831f8f3dff90580f39dff13bb9b039ad3..ba7f105b8e6435c1be4f6215f0a8b918caf8a2bd 100644
--- a/tests/saveload/multi_project.ml
+++ b/tests/saveload/multi_project.ml
@@ -23,4 +23,4 @@ let main () =
check "default" (<>);
check "bar" (<>)
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/saveload/status.ml b/tests/saveload/status.ml
index 5337381c38f61d7ebd21bfe3dd76abd77f937f0b..1203f653da673aa02b8e30ade126e5ed44a2a880 100644
--- a/tests/saveload/status.ml
+++ b/tests/saveload/status.ml
@@ -39,4 +39,4 @@ let main () =
end in
Visitor.visitFramacFileSameGlobals o (Ast.get ())
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/scope/bts971.ml b/tests/scope/bts971.ml
index 308f4e84faac142bf859f27f65f499b5d4aa70fc..2f42807031bdccf95eeb08e69fc0774381810d31 100644
--- a/tests/scope/bts971.ml
+++ b/tests/scope/bts971.ml
@@ -63,4 +63,4 @@ let main _ =
tests ()
;;
-let _ = Db.Main.extend main
+let _ = Boot.Main.extend main
diff --git a/tests/scope/zones.ml b/tests/scope/zones.ml
index 44c8841ce20ff11081d17df4ce27678a661ef8a5..2cdc9f2b99108fa1448c43793ada568d86a66a2f 100644
--- a/tests/scope/zones.ml
+++ b/tests/scope/zones.ml
@@ -64,4 +64,4 @@ let main _ =
let pp = find_ret "caller" in
compute_and_print pp "Yf"
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/slicing/adpcm.ml b/tests/slicing/adpcm.ml
index ff6515dce26737dc4355e611a7eaeca836bd31d8..bea1c788a8db4d25ed8d4337915b2a808a6289a3 100644
--- a/tests/slicing/adpcm.ml
+++ b/tests/slicing/adpcm.ml
@@ -12,5 +12,5 @@ let resname = "tests/slicing/adpcm.sliced" in
ignore (test "uppol2" ~do_prop_to_callers:true ~resname (select_retres));;
*)
let () =
- Db.Main.extend
+ Boot.Main.extend
(fun _ -> ignore (test "uppol2" ~do_prop_to_callers:true (select_retres)))
diff --git a/tests/slicing/anim.ml b/tests/slicing/anim.ml
index 50e23891052592eb8f602c19bb18a5990e8c8740..d80f6eaded10b3c578372359d019b0219dc4f72c 100644
--- a/tests/slicing/anim.ml
+++ b/tests/slicing/anim.ml
@@ -47,4 +47,4 @@ let main _ =
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/slicing/combine.ml b/tests/slicing/combine.ml
index 55fef497d923a4e9cba21e14e64d1b0174829bc4..363a52744674203eb654ba925d0ddcd543241187 100644
--- a/tests/slicing/combine.ml
+++ b/tests/slicing/combine.ml
@@ -66,4 +66,4 @@ let main _ =
Format.printf "After Sparecode :@.";
File.pretty_ast ~prj:proj4 ();;
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/slicing/ex_spec_interproc.ml b/tests/slicing/ex_spec_interproc.ml
index f378201635ea019df2276d1c0ec0c8bea7ed1952..749bf33a9cd6b05cbd4389a7c1f10fb8cfa64fb0 100644
--- a/tests/slicing/ex_spec_interproc.ml
+++ b/tests/slicing/ex_spec_interproc.ml
@@ -107,4 +107,4 @@ let main _ =
print_project ();;
(*=========================================================================*)
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/slicing/horwitz.ml b/tests/slicing/horwitz.ml
index f8034d2bb8bfe58794f7aee9d97fa09214159c64..59d8909fec7affa744ce0427e937dbcd6bf08266 100644
--- a/tests/slicing/horwitz.ml
+++ b/tests/slicing/horwitz.ml
@@ -8,6 +8,6 @@ tests/slicing/horwitz.byte -deps tests/slicing/horwitz.c
include LibSelect;;
let () =
- Db.Main.extend
+ Boot.Main.extend
(fun _ ->
ignore (test_select_data ~do_prop_to_callers:true "incr" "*pi"));;
diff --git a/tests/slicing/mark_all_slices.ml b/tests/slicing/mark_all_slices.ml
index 368ca32111e0e6c146a934c0a1ad3c7f3bf02b98..eecfabb85f5754b981b19e5b9a74d37fecbfb142 100644
--- a/tests/slicing/mark_all_slices.ml
+++ b/tests/slicing/mark_all_slices.ml
@@ -70,4 +70,4 @@ let main _ =
Slicing.Api.Request.apply_all_internal ();
extract_and_print ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/slicing/merge.ml b/tests/slicing/merge.ml
index 779736380bbeacedb289bdd76ba997d4da072c04..59c3c7850452178fea83a2e65f9d7878a12b75ec 100644
--- a/tests/slicing/merge.ml
+++ b/tests/slicing/merge.ml
@@ -95,4 +95,4 @@ let main _ =
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/slicing/min_call.ml b/tests/slicing/min_call.ml
index 80fbe7ad12575a7cf978e0441508b3fec992676d..20d9cf894b4313e8de955b113d1856183320df45 100644
--- a/tests/slicing/min_call.ml
+++ b/tests/slicing/min_call.ml
@@ -129,4 +129,4 @@ extract_and_print project;;
*)
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/slicing/select_by_annot.ml b/tests/slicing/select_by_annot.ml
index 39e3e6d67a0bbda7190384523b629ca7b7ba20b9..f6c24675639034770580bd80540ddadde8624ba1 100644
--- a/tests/slicing/select_by_annot.ml
+++ b/tests/slicing/select_by_annot.ml
@@ -45,4 +45,4 @@ let main _ =
Slicing.Api.Project.pretty Format.std_formatter;
extract_and_print ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/slicing/select_simple.ml b/tests/slicing/select_simple.ml
index 3f4f91a882baf5854948d5ae40233726b28d64ec..620101c3c7112425f8722af6cb47975778dcc1a3 100644
--- a/tests/slicing/select_simple.ml
+++ b/tests/slicing/select_simple.ml
@@ -21,4 +21,4 @@ let main _ =
ignore (test_select_data "f8" "ps->c");
ignore (test_select_data "f8" "*ps")
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/slicing/simple_intra_slice.ml b/tests/slicing/simple_intra_slice.ml
index e60a1638a7c80ed04c83d6de012bcb1146ace84e..44324761620faf36c046e3895eb3710b00e0b2dc 100644
--- a/tests/slicing/simple_intra_slice.ml
+++ b/tests/slicing/simple_intra_slice.ml
@@ -108,4 +108,4 @@ let main _ =
Slicing.Api.Project.pretty Format.std_formatter
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/slicing/slice_no_body.ml b/tests/slicing/slice_no_body.ml
index 3987c2dbb5549f1e1cb5a3f78a8f52bbbf2f909c..1ac5530d7cf37a47366539cc2bca97124630a18b 100644
--- a/tests/slicing/slice_no_body.ml
+++ b/tests/slicing/slice_no_body.ml
@@ -58,4 +58,4 @@ let main _ =
print_project ();
extract_and_print ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/slicing/switch.ml b/tests/slicing/switch.ml
index 3ca361344c91d376826f603ced718685d0c257ac..34757642a6d327507f33b708517a67ae9b8dbb33 100644
--- a/tests/slicing/switch.ml
+++ b/tests/slicing/switch.ml
@@ -7,4 +7,4 @@ let main _ =
test_select_data "main" "x";
test_select_data "main" "y";
test_select_data "main" "z"
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/spec/Extend.ml b/tests/spec/Extend.ml
index db2b0600fb056e3493e2567ff559ebaf3b460813..86330eb14674168bdf7439fa582fbdd6d7b0353d 100644
--- a/tests/spec/Extend.ml
+++ b/tests/spec/Extend.ml
@@ -136,4 +136,4 @@ let run () =
Project.on prj Ast.compute ();
File.pretty_ast ~prj ()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/spec/Extend_recursive_preprocess.ml b/tests/spec/Extend_recursive_preprocess.ml
index 49ebe8a4369d0367afcecc959f034e61381861d1..e2e583cb32bc19ed1e21ae061cc3983296b2c2b1 100644
--- a/tests/spec/Extend_recursive_preprocess.ml
+++ b/tests/spec/Extend_recursive_preprocess.ml
@@ -80,4 +80,4 @@ let run () =
Filecheck.check_ast "Test";
Project.set_current old
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/spec/Extend_short_print.ml b/tests/spec/Extend_short_print.ml
index 3bc2da1b356c7916b579cc72d42623b0409a4f5b..00856164ca3523766c133b6b89918d6ad4055323 100644
--- a/tests/spec/Extend_short_print.ml
+++ b/tests/spec/Extend_short_print.ml
@@ -11,4 +11,4 @@ let process_global _ = function
| Dextended(e, _, _) -> Kernel.feedback "%a" Cil_printer.pp_short_extended e
| _ -> ()
-let () = Db.Main.extend (fun () -> Annotations.iter_global process_global)
+let () = Boot.Main.extend (fun () -> Annotations.iter_global process_global)
diff --git a/tests/spec/Type_of_term.ml b/tests/spec/Type_of_term.ml
index 30350f7bc83682ce293385dccfec0cbbb1015729..2ea168c2e08b9f3f21fb2a041d1d69bf10cc60cb 100644
--- a/tests/spec/Type_of_term.ml
+++ b/tests/spec/Type_of_term.ml
@@ -33,4 +33,4 @@ let run () =
Visitor.visitFramacFileSameGlobals (new visitor) ast
;;
-Db.Main.extend run
+Boot.Main.extend run
diff --git a/tests/spec/add_global.ml b/tests/spec/add_global.ml
index 20497076ec3e57581978dddbee179f5355356a45..1bef94312b3bc740c7a8912c2ac415329b49fef6 100644
--- a/tests/spec/add_global.ml
+++ b/tests/spec/add_global.ml
@@ -33,4 +33,4 @@ let transform () =
Project.on prj Filecheck.check_ast "prj";
File.pretty_ast ~prj ()
-let () = Db.Main.extend transform
+let () = Boot.Main.extend transform
diff --git a/tests/spec/assigns_from_kf.ml b/tests/spec/assigns_from_kf.ml
index 0b2db1c2597924a3f4fd195103ad2ad8c2927047..67e0a71a3574101028de48cc2540f7b24aaaec63 100644
--- a/tests/spec/assigns_from_kf.ml
+++ b/tests/spec/assigns_from_kf.ml
@@ -4,4 +4,4 @@ let run () =
ignore (Annotations.funspec kf)
)
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/spec/boolean_conversion.ml b/tests/spec/boolean_conversion.ml
index a2071303368c92bef6b1bcec891ca5ca807a365e..1f592aa1cdc112703551aa5da04e17868a0eaf4b 100644
--- a/tests/spec/boolean_conversion.ml
+++ b/tests/spec/boolean_conversion.ml
@@ -19,4 +19,4 @@ let run () =
Visitor.visitFramacFileSameGlobals vis (Ast.get());
Filecheck.check_ast "Test"
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/spec/bts0578.ml b/tests/spec/bts0578.ml
index 594d3b71e4b03b506173990f569c70b3ae21ddcf..00edf14ec350c23d5eea437c613119917a2df405 100644
--- a/tests/spec/bts0578.ml
+++ b/tests/spec/bts0578.ml
@@ -42,4 +42,4 @@ let main () =
Annotations.add_ensures Emitter.end_user kf ~stmt:!s3 post_cond;
Filecheck.check_ast "after merging code_annot and ensures"
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/spec/bts0655.ml b/tests/spec/bts0655.ml
index 6137de01c4f3443ed4e811608d4a18ca94de7a6f..515c000abbb03468a37d8053daf74328951a6dd1 100644
--- a/tests/spec/bts0655.ml
+++ b/tests/spec/bts0655.ml
@@ -20,4 +20,4 @@ let run () =
let f = Ast.get () in
Visitor.visitFramacFileSameGlobals (new check_float) f
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/spec/comparison.ml b/tests/spec/comparison.ml
index b04cbf629387bf88dfc337863dfbed17b492e2bb..c0983cdcb65cb77e13f02aee58e6add4245c564c 100644
--- a/tests/spec/comparison.ml
+++ b/tests/spec/comparison.ml
@@ -28,4 +28,4 @@ let run () =
Visitor.visitFramacFileSameGlobals vis (Ast.get())
;;
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/spec/default_spec_combine.ml b/tests/spec/default_spec_combine.ml
index 5c2cd6c0ccbc488e12917a4b33ba866d09b1d65a..df156a1b321f7feedff45c526870173b42af5b6c 100644
--- a/tests/spec/default_spec_combine.ml
+++ b/tests/spec/default_spec_combine.ml
@@ -28,4 +28,4 @@ let populate () =
let () = Cmdline.run_after_configuring_stage populate
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/spec/default_spec_custom.ml b/tests/spec/default_spec_custom.ml
index 964e4bd7e1546e51f9b1d0424ecc7e2fdec5d000..e804e3f5c1573dd4803d79cafbee2b0f16952fc6 100644
--- a/tests/spec/default_spec_custom.ml
+++ b/tests/spec/default_spec_custom.ml
@@ -48,4 +48,4 @@ let populate () =
let () = Cmdline.run_after_configuring_stage populate
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/spec/default_spec_mode.ml b/tests/spec/default_spec_mode.ml
index 1ebbd226e9059736d7af1124fb3f44f65f4925b2..c72a69092d8540bddd292d152a0a05669fbe2737 100644
--- a/tests/spec/default_spec_mode.ml
+++ b/tests/spec/default_spec_mode.ml
@@ -16,4 +16,4 @@ let run () =
Globals.Functions.iter generate_spec
[@@ warning "-3"]
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/spec/expr_to_term.ml b/tests/spec/expr_to_term.ml
index ab45132edef74fda692787fbfbbb8eb75acf6832..981677af4b9157cbaf129644343cbec9bc1386a9 100644
--- a/tests/spec/expr_to_term.ml
+++ b/tests/spec/expr_to_term.ml
@@ -92,4 +92,4 @@ let compute () =
treat_fct_pred i;
end
-let () = Db.Main.extend compute
+let () = Boot.Main.extend compute
diff --git a/tests/spec/extend_extern.ml b/tests/spec/extend_extern.ml
index e5c2f208daa0da69b050079e2917b19e417fc40d..4bc0b994098b02e948cb1d2a4e3d9e19f6d23bfd 100644
--- a/tests/spec/extend_extern.ml
+++ b/tests/spec/extend_extern.ml
@@ -33,4 +33,4 @@ let () = Kernel.TypeCheck.set false
let () = Kernel.Debug.set 1
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/spec/location_char.ml b/tests/spec/location_char.ml
index 59768fd96d6e2f7a79f844c3eb7514e5b84a7b57..49357073c1e86bb4f2a7e09de2bc0e6d52f912ac 100644
--- a/tests/spec/location_char.ml
+++ b/tests/spec/location_char.ml
@@ -37,4 +37,4 @@ end
let main () =
Visitor.visitFramacFileSameGlobals (new print_term) (Ast.get())
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/spec/logic_functions_sets.ml b/tests/spec/logic_functions_sets.ml
index f4b2847fec3e10ff5d3b6fd673406b363e403ffd..567806c7f75335fa50180b7624b8e1cc0d195021 100644
--- a/tests/spec/logic_functions_sets.ml
+++ b/tests/spec/logic_functions_sets.ml
@@ -13,4 +13,4 @@ let check = function
| _ -> ()
let () =
- Db.Main.extend (fun () -> Annotations.iter_global (fun _ g -> check g))
+ Boot.Main.extend (fun () -> Annotations.iter_global (fun _ g -> check g))
diff --git a/tests/spec/loop_assigns_generated.ml b/tests/spec/loop_assigns_generated.ml
index 00739577e3d845c29c86de1d3c6658fa34b6365f..c009bfc5e6ac4bf85dff53210803700de65c5375 100644
--- a/tests/spec/loop_assigns_generated.ml
+++ b/tests/spec/loop_assigns_generated.ml
@@ -92,4 +92,4 @@ let main () =
(Property.ip_of_code_annot_single kf s (List.hd lalloc)));
File.pretty_ast ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/spec/model.ml b/tests/spec/model.ml
index 0199a1377741054724df687749950ae71605b6dd..7ece88634f085734c53e16ef24f9843a72f2c333 100644
--- a/tests/spec/model.ml
+++ b/tests/spec/model.ml
@@ -46,4 +46,4 @@ let main () =
print_models typ;
Format.print_flush ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/spec/pp_empty_spec.ml b/tests/spec/pp_empty_spec.ml
index 220c1774a2c1ca3265ff87578f56edb13604456f..699515474771c8e719f14761632ef752c05cdccb 100644
--- a/tests/spec/pp_empty_spec.ml
+++ b/tests/spec/pp_empty_spec.ml
@@ -32,4 +32,4 @@ let run () =
(List.hd (Annotations.behaviors ~emitter main));
File.pretty_ast()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/spec/property_test.ml b/tests/spec/property_test.ml
index 9088cf306802455e82893b4042ccd39921790e5c..e7e19684b7d1b7b4e3bb696186b2d92aea2a34ac 100644
--- a/tests/spec/property_test.ml
+++ b/tests/spec/property_test.ml
@@ -74,4 +74,4 @@ let run () =
show_properties ();
Project.on prj show_properties ()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/spec/status_by_call_issue_890.ml b/tests/spec/status_by_call_issue_890.ml
index 374e927700b937885f27c029f3d1744110d9ea39..78684161af938b737b54fd6b718cc7eb2cfb86bb 100644
--- a/tests/spec/status_by_call_issue_890.ml
+++ b/tests/spec/status_by_call_issue_890.ml
@@ -1,3 +1,3 @@
let () =
- Db.Main.extend
+ Boot.Main.extend
(fun () -> Globals.Functions.iter Statuses_by_call.setup_all_preconditions_proxies)
diff --git a/tests/spec/type_constructors_in_env.ml b/tests/spec/type_constructors_in_env.ml
index 91848fca46bde9e68c9fa474f0419c94aa6d9ddf..ff32f386106f7cd0cd33a7ffc18ea3906bd533b2 100644
--- a/tests/spec/type_constructors_in_env.ml
+++ b/tests/spec/type_constructors_in_env.ml
@@ -8,4 +8,4 @@ let run () =
with Not_found -> Kernel.fatal "A should be in the environment");
File.pretty_ast ()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/syntax/Enum_repr.ml b/tests/syntax/Enum_repr.ml
index 3346cb44b0cf42d98bf275a8489e244f30513bf6..d94c9bb1f232e49dcf6c57f807b83c1f19646711 100644
--- a/tests/syntax/Enum_repr.ml
+++ b/tests/syntax/Enum_repr.ml
@@ -18,4 +18,4 @@ let run () =
| _ -> ()
in
List.iter output f.globals
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/syntax/Refresh_visitor.ml b/tests/syntax/Refresh_visitor.ml
index b5473e4babc253445b1cdc78594f3b683f93830d..1b56638f8397f1b0f0a0e00166a077318899bc8c 100644
--- a/tests/syntax/Refresh_visitor.ml
+++ b/tests/syntax/Refresh_visitor.ml
@@ -76,4 +76,4 @@ let main () =
) ();
File.pretty_ast ~prj:p ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/syntax/add_allocates.ml b/tests/syntax/add_allocates.ml
index b570e86889e229bf1528d4ef585196420363f2fd..1880115f52bfa921012297675a888f31d9c08b6f 100644
--- a/tests/syntax/add_allocates.ml
+++ b/tests/syntax/add_allocates.ml
@@ -1,2 +1,2 @@
let () =
- Db.Main.extend Allocates.add_allocates_nothing
+ Boot.Main.extend Allocates.add_allocates_nothing
diff --git a/tests/syntax/ast_diff_1.ml b/tests/syntax/ast_diff_1.ml
index 9cf6b01c5d5a3c04b1e180846e05ad48883ebc5b..1a85f02e29488f26c4e06a1b0359cbc4a2307f6c 100644
--- a/tests/syntax/ast_diff_1.ml
+++ b/tests/syntax/ast_diff_1.ml
@@ -24,4 +24,4 @@ let show_correspondances () =
Ast_diff.Kernel_function.iter show_fun;
end
-let () = Db.Main.extend show_correspondances
+let () = Boot.Main.extend show_correspondances
diff --git a/tests/syntax/ast_init.ml b/tests/syntax/ast_init.ml
index f0e57935a236f696af9949647edb7ec78d06fb81..5d8f7ebcf6bde4c0fe0a7d1547807ee631af983a 100644
--- a/tests/syntax/ast_init.ml
+++ b/tests/syntax/ast_init.ml
@@ -17,4 +17,4 @@ let run () =
Ast.compute ();
File.pretty_ast ()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/syntax/clone_test.ml b/tests/syntax/clone_test.ml
index f1d044e360ca5c10d475483b4dbee281e77758cf..f89efcb734e8e2c7a140bffe411ab5c2492be129 100644
--- a/tests/syntax/clone_test.ml
+++ b/tests/syntax/clone_test.ml
@@ -5,4 +5,4 @@ let run () =
File.pretty_ast();
Filecheck.check_ast "clone"
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/syntax/copy_visitor_bts_1073.ml b/tests/syntax/copy_visitor_bts_1073.ml
index 65cfeb144d9e11ed0dff43387c254d8ff4088af3..7a1bfb7d7bb59e2bcac99a3d28155ca89f05c12e 100644
--- a/tests/syntax/copy_visitor_bts_1073.ml
+++ b/tests/syntax/copy_visitor_bts_1073.ml
@@ -30,4 +30,4 @@ let run () =
in
File.pretty_ast ~prj ()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/syntax/copy_visitor_bts_1073_bis.ml b/tests/syntax/copy_visitor_bts_1073_bis.ml
index 7f6abc845200d0eceff40365c3c812cd702b3632..bf6940f3d0c048aaf94c70102fad611d99921108 100644
--- a/tests/syntax/copy_visitor_bts_1073_bis.ml
+++ b/tests/syntax/copy_visitor_bts_1073_bis.ml
@@ -51,5 +51,5 @@ let main () =
P.feedback "exported in new project : %s" new_proj_name
end
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(*============================================================================*)
diff --git a/tests/syntax/formals_decl_leak.ml b/tests/syntax/formals_decl_leak.ml
index ad61b6e9d03a365784d31010f6c2f3aae5a09eec..346158605bf084d856b40e9a985df3d5d141fd96 100644
--- a/tests/syntax/formals_decl_leak.ml
+++ b/tests/syntax/formals_decl_leak.ml
@@ -11,4 +11,4 @@ let check_vi_exists vi _ =
let run () =
let _ = Ast.get () in Cil.iterFormalsDecl check_vi_exists
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/syntax/func_locs.ml b/tests/syntax/func_locs.ml
index e28f0429b68ca220b12e37f15c4417edc32179c6..3c0d0a77a1bd9f39dfe5df3ef39a6cc3acd7236e 100644
--- a/tests/syntax/func_locs.ml
+++ b/tests/syntax/func_locs.ml
@@ -6,4 +6,4 @@ let run () =
fname
) (Cabs2cil.func_locs ())
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/syntax/get_astinfo_bts1136.ml b/tests/syntax/get_astinfo_bts1136.ml
index e842f7e046d687f023eca1e6c8563c03d6d33ccf..405d52240d1ae4ed4f237f8bb9d5f0c095cde338 100644
--- a/tests/syntax/get_astinfo_bts1136.ml
+++ b/tests/syntax/get_astinfo_bts1136.ml
@@ -36,4 +36,4 @@ let main () =
Cil_datatype.Syntactic_scope.pretty kind
in List.iter do_v vars; List.iter do_v vars'
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/syntax/ghost_cv_var_decl.ml b/tests/syntax/ghost_cv_var_decl.ml
index a4715ea3d0a87386c4ab6add6fb877e37c9bf7fe..c278d32a902345b7364575590f67e3b9fcdd3c9f 100644
--- a/tests/syntax/ghost_cv_var_decl.ml
+++ b/tests/syntax/ghost_cv_var_decl.ml
@@ -45,4 +45,4 @@ class visitor = object(_)
end
let () =
- Db.Main.extend (fun () -> Visitor.visitFramacFileSameGlobals (new visitor) (Ast.get ()))
+ Boot.Main.extend (fun () -> Visitor.visitFramacFileSameGlobals (new visitor) (Ast.get ()))
diff --git a/tests/syntax/ghost_parameters_formals_status.ml b/tests/syntax/ghost_parameters_formals_status.ml
index 792d21a8f44538b02c681ebff028fc22208362c8..8ed3ae99011d09628bbcc9fc3412c3312970f26d 100644
--- a/tests/syntax/ghost_parameters_formals_status.ml
+++ b/tests/syntax/ghost_parameters_formals_status.ml
@@ -25,4 +25,4 @@ let run () =
in
Globals.Functions.iter print_info
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/syntax/logic_env_script.ml b/tests/syntax/logic_env_script.ml
index 6598804b5dabf33d46bd35e748643f5f99661364..7d171a9b2a4f9e9001615ed475f36b72c7a8fac8 100644
--- a/tests/syntax/logic_env_script.ml
+++ b/tests/syntax/logic_env_script.ml
@@ -28,4 +28,4 @@ let run () =
in
Project.on prj check ()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/syntax/mutable_test.ml b/tests/syntax/mutable_test.ml
index a3c06d6424eeda5e5c4268f5af98c0af9fbc74ae..b72ff4783dac1d229a8a18577676f652427f6358 100644
--- a/tests/syntax/mutable_test.ml
+++ b/tests/syntax/mutable_test.ml
@@ -15,4 +15,4 @@ let main () =
(not (Cil.typeHasAttribute "const" (Cil.typeOffset x.vtype offset)))
| _ -> assert false
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/syntax/reorder.ml b/tests/syntax/reorder.ml
index 9a527c7a9a2d98e168b6a14ec29b3d449ff65dcc..6848afacc1c2a89a43e0aa9069a217f0d6d5aeaa 100644
--- a/tests/syntax/reorder.ml
+++ b/tests/syntax/reorder.ml
@@ -54,4 +54,4 @@ let run () =
File.pretty_ast ();
Filecheck.check_ast "reordered"
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/syntax/temporary_location.ml b/tests/syntax/temporary_location.ml
index 0f09f3308a6ece20e90940de47f88beb9e0c89a0..66bc8a7fe8e4b3b30b89ebb6cb8506f82d04e902 100644
--- a/tests/syntax/temporary_location.ml
+++ b/tests/syntax/temporary_location.ml
@@ -14,4 +14,4 @@ let main () =
Cil.visitCilFile (new vis :> Cil.cilVisitor) (Ast.get ())
let () =
- Db.Main.extend main
+ Boot.Main.extend main
diff --git a/tests/syntax/transient_block.ml b/tests/syntax/transient_block.ml
index 79a9fc9d24574aa3c8154e3e0e57aeda1f7360d4..6cde00d6b77403522c495807ceff448292603451 100644
--- a/tests/syntax/transient_block.ml
+++ b/tests/syntax/transient_block.ml
@@ -50,4 +50,4 @@ let main () =
let prj = File.create_project_from_visitor "test" (fun prj -> new vis prj) in
File.pretty_ast ~prj ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/syntax/typedef_multi.ml b/tests/syntax/typedef_multi.ml
index 2401972bb518c95055702f302615bf86e0814697..02d7c09feb1a5838b0a4a873c699b25efd257e77 100644
--- a/tests/syntax/typedef_multi.ml
+++ b/tests/syntax/typedef_multi.ml
@@ -2,4 +2,4 @@ let run () =
File.reorder_ast ();
File.pretty_ast ()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/syntax/vdescr_bts1387.ml b/tests/syntax/vdescr_bts1387.ml
index 8d9bfb9491f63f97f6b8d852dc4f8e6e6f46b072..42d12a82dc52596779d95c5794c5708da7caed8f 100644
--- a/tests/syntax/vdescr_bts1387.ml
+++ b/tests/syntax/vdescr_bts1387.ml
@@ -12,4 +12,4 @@ class print_vdescr =
let run () = Visitor.visitFramacFileSameGlobals (new print_vdescr) (Ast.get())
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/syntax/visit_create_local.ml b/tests/syntax/visit_create_local.ml
index 8a82d9d421339f8c89731d786fd60bc2d32dd017..43d34b1446e424d49725c174d632129fe6e03a3b 100644
--- a/tests/syntax/visit_create_local.ml
+++ b/tests/syntax/visit_create_local.ml
@@ -34,4 +34,4 @@ let main () =
Project.on prj run ();
end
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/value/unit_tests.ml b/tests/value/unit_tests.ml
index 48e3b3405bcb13af995b3a50f15aebaa64b09b54..16b578adda73105011b362ed629cff2ffbb6a9c2 100644
--- a/tests/value/unit_tests.ml
+++ b/tests/value/unit_tests.ml
@@ -1,3 +1,3 @@
(* Programmatic tests of Eva, run by unit_tests.i. *)
-let () = Db.Main.extend Eva.Unit_tests.run
+let () = Boot.Main.extend Eva.Unit_tests.run