diff --git a/Makefile b/Makefile
index 8c50dcd33285417a0de749dd2cf8105a5d0229fd..422f3709cbabf495152eeb0e5d56ae39d225388e 100644
--- a/Makefile
+++ b/Makefile
@@ -483,8 +483,7 @@ FIRST_CMO= src/kernel_internals/runtime/fc_config \
src/kernel_services/plugin_entry_points/log \
src/kernel_services/cmdline_parameters/cmdline \
src/libraries/project/project_skeleton \
- src/libraries/datatype/datatype \
- src/kernel_services/plugin_entry_points/journal
+ src/libraries/datatype/datatype
# project_skeleton requires log
# datatype requires project_skeleton
@@ -794,7 +793,7 @@ PLUGIN_ENABLE:=$(ENABLE_CALLGRAPH)
PLUGIN_NAME:=Callgraph
PLUGIN_DISTRIBUTED:=yes
PLUGIN_DIR:=src/plugins/callgraph
-PLUGIN_CMO:= options journalize subgraph cg services uses register
+PLUGIN_CMO:= options subgraph cg services uses register
ifeq ($(HAS_DGRAPH),yes)
PLUGIN_GUI_CMO:=cg_viewer
PLUGIN_GENERATED:=$(PLUGIN_DIR)/cg_viewer.ml
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 73cc5d5d77990e09a6e63e77a6b78ace38cdbd80..9204bb9d459298dcf9cd7461bca7afa7e7b695a3 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -1769,7 +1769,7 @@ contains the type itself, the type value corresponding to this type, its name,
functions \texttt{equal}, \texttt{compare}, \texttt{hash} and \texttt{pretty}
which may respectively be used to check equality, to compare, to hash and to
pretty print values of this type. It also contains some other values (for
-instance required when marshaling or journalizing). Whenever possible, a
+instance required when marshaling). Whenever possible, a
datatype implements an extensible version of \texttt{Datatype.S}, namely
\texttt{Datatype.S\_with\_collections}\scodeidx{Datatype}{S\_with\_collections}.
For a type $\tau$, this extended signature additionally provides modules
@@ -1830,7 +1830,6 @@ simple sum type.
\sscodeidx{Structural\_descr}{t}{Structure}
\sscodeidx{Structural\_descr}{structure}{Sum}
\scodeidx{Structural\_descr}{p\_int}
-\index{Journalisation}
\index{Marshaling}
\index{Project}
\begin{ocamlcode}
@@ -1867,31 +1866,11 @@ module AB =
let pretty fmt x =
Format.pp_print_string fmt
(match x with A -> "a" | B n -> "b" ^ string_of_int n)
- (* printer which must produce a valid OCaml value in a given
- context. It is used when journalising. *)
- let internal_pretty_code prec_caller fmt = function
- | A ->
- Type.par
- prec_caller
- Type.Basic
- fmt
- (fun fmt -> Format.pp_print_string fmt "A")
- | B n ->
- Type.par
- prec_caller
- Type.Call
- fmt
- (fun fmt -> Format.fprintf fmt "B %d" n)
- (* A good prefix name to use for an OCaml variable of this type. *)
- let varname v = "ab" ^ (match v with A -> "_a_" | B -> "_b_")
end)
\end{ocamlcode}
\end{example}
Only providing an effective implementation for the values \texttt{name} and
-\texttt{reprs} is mandatory. For instance, if you know that you never journalize
-a value of a type \texttt{t}, you can define the function
-\texttt{internal\_pretty\_code} equal to the predefined function
-\texttt{Datatype.pp\_fail}\scodeidx{Datatype}{pp\_fail}. Similarly, if you never
+\texttt{reprs} is mandatory. For instance, if you know that you never
use values of type \texttt{t} as keys of hashtable, you can define the function
hash equal to the function
\texttt{Datatype.undefined}\scodeidx{Datatype}{undefined} , and so on. To ease
@@ -2224,7 +2203,7 @@ previously registered with \texttt{Dynamic.register}.
The signature of \texttt{Dynamic.register}\scodeidx{Dynamic}{register} is as
follows.\scodeidx{Type}{t}
\begin{ocamlcode}
-val register: plugin:string -> string -> 'a Type.t -> journalize:bool -> 'a ->
+val register: plugin:string -> string -> 'a Type.t -> 'a ->
unit
\end{ocamlcode}
The first argument is the name of the plug-in registering the value and the
@@ -2234,11 +2213,8 @@ name, binding name) must not be used for value registration anywhere else in
(see next paragraph). The third argument is the \emph{type value}%
\index{Type!Value} of the registered value (see
Section~\ref{type:type-value}). It is required for safety reasons when accessing
-to the registered value (see the next paragraph). The labeled fourth argument
-\texttt{journalize} indicates whether a total call to this function must be
-written in the journal\index{Journalization} (see also
-Section~\ref{adv:journalization}). The usual value for this argument is
-\texttt{true}. The fifth argument is the value to register.
+to the registered value (see the next paragraph). The fourth argument is the
+value to register.
\begin{example}
Here is how the function \texttt{run} of the plug-in
@@ -2252,7 +2228,6 @@ let () =
~plugin:"Hello"
"run"
(Datatype.func Datatype.unit Datatype.unit)
- ~journalize:true
run
\end{ocamlcode}
If the string \texttt{"Hello.run"} is already used to register a
@@ -2332,10 +2307,6 @@ dynamically registered functions).
\ocamlinput{./examples/generated/use_callstack.ml}
\end{example}
-\section{Journalization}\label{adv:journalization}
-
-\todo
-
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Project Management System}\label{adv:project}
@@ -3165,9 +3136,8 @@ tightly coupled with handling the command line parameters.
The parsing of the command line parameters is performed in several
\emph{phases} and \emph{stages}
\index{Command Line!Parsing},
-each one dedicated to specific operations. For instance,
-journal replays should be performed after loading dynamic plug-ins, and so
-on. Following the general rule stated at the beginning of this section, even
+each one dedicated to specific operations.
+Following the general rule stated at the beginning of this section, even
the kernel services of \framac are internally registered as hooks routines to
be executed at a specific stage of the initialization process, among plug-ins
ones.
@@ -3201,25 +3171,21 @@ their execution order.
Plug-in developers cannot customize this stage. In particular, the module
\texttt{Cmdline}\codeidx{Cmdline} (one of the first linked modules, see
Figure~\ref{fig:architecture}) performs a very early configuration stage,
- such as checking if journalization has to be activated
- (cf.~Section~\ref{adv:journalization}\index{Journalization}), or setting the
- global verbosity and debugging levels.
-
+ such as setting the global verbosity and debugging levels.
+
\item \label{stage:early} \textbf{The Early Stage:} this stage initializes the
kernel services. More precisely:
\begin{enumerate}[(a)]
- \item first, the journal name is set to its right value (according to the
- option \texttt{-journal-name}) and the default project is created;
- \item then, the parsing of command line options registered for the
+ \item first, the parsing of command line options registered for the
\texttt{Cmdline.Early}\sscodeidxdef{Cmdline}{stage}{Early} stage;
- \item finally, all functions registered through
+ \item then, all functions registered through
\texttt{Cmdline.run\_after\_early\_stage}%
\scodeidxdef{Cmdline}{run\_after\_early\_stage} are executed in an
unspecified order.
\end{enumerate}
\item \label{stage:extending} \textbf{The Extending Stage:}\index{Linking} the searching and
- loading of dynamically linked plug-ins, of journal, scripts and
+ loading of dynamically linked plug-ins, scripts and
modules is performed at this stage. More precisely:
\begin{enumerate}[(a)]
@@ -3232,7 +3198,7 @@ their execution order.
\texttt{Cmdline.run\_during\_extending\_stage}
\scodeidxdef{Cmdline}{run\_during\_extending\_stage} are executed. Such
hooks include kernel function calls for searching, loading and linking the
- various plug-ins, journal and scripts compilation units, with respect to
+ various plug-ins and scripts compilation units, with respect to
the command line options parsed during stages~\ref{stage:early}
and~\ref{stage:extending}.
\end{enumerate}
@@ -3289,8 +3255,7 @@ their execution order.
\item \textbf{The Loading Stage:} this is where the initial state of \framac
can be replaced by another one. Typically, it would be loaded from disk
- through the \texttt{-load} option\index{Loading} or computed by running a
- journal (see Section~\ref{adv:journalization})\index{Journalization}. As
+ through the \texttt{-load} option\index{Loading}. As
for the other stages:
\begin{enumerate}[(a)]
diff --git a/doc/developer/changes.tex b/doc/developer/changes.tex
index 3f385775d1636b5f4ccba779ca8d0bde3119fbeb..28243898984e95fb7e2eddd4779693ec13c04e8f 100644
--- a/doc/developer/changes.tex
+++ b/doc/developer/changes.tex
@@ -5,6 +5,11 @@
This chapter summarizes the major changes in this documentation between each
\framac release, from newest to oldest.
+\section*{dev}
+\begin{itemize}
+\item \textbf{Journalisation}: Journalisation has been removed.
+\end{itemize}
+
\section*{25.0 Manganese}
\begin{itemize}
\item \textbf{Testing}: Document new directives (\texttt{PLUGIN}, \texttt{SCRIPT} and \texttt{LIBS}) and new predefined macros for \texttt{ptests}.
@@ -142,10 +147,10 @@ introduced loop extensions.
\item \textbf{Makefile} \texttt{WARN\_ERROR\_ALL} variable.
\item \textbf{Log}: Debug category (\texttt{\~{}dkey} argument).
\item \textbf{Visitor}: \texttt{DoChildrenPost} action.
-\item \textbf{Testing}: document the need for directories
+\item \textbf{Testing}: document the need for directories
to store result and oracles.
\item \textbf{Project Management System}: Fine tuning of AST dependencies.
-\item \textbf{Testing}: added \texttt{PTESTS\_OPTS} and
+\item \textbf{Testing}: added \texttt{PTESTS\_OPTS} and
\texttt{PLUGIN\_PTESTS\_OPTS} Makefile's variables.
\item \textbf{Type}: document the \texttt{type} library.
\item \textbf{Logical Annotations}: fully updated.
@@ -154,7 +159,7 @@ introduced loop extensions.
in \emph{Reference Manual}.
\item \textbf{Website}: refer to CEA internal documentation.
\item \textbf{Command Line Options}: explain how to modify the default behavior
- of an option.
+ of an option.
\item \textbf{Command Line Options}: fully updated.
\item \textbf{Project Management System}: fully updated.
\item \textbf{Plug-in Registration and Access}: \texttt{Type} replaced by
@@ -168,7 +173,7 @@ introduced loop extensions.
\section*{Nitrogen-20111001}
\begin{itemize}
-\item \textbf{Tutorial of the Future}: new chapter for preparing a future
+\item \textbf{Tutorial of the Future}: new chapter for preparing a future
tutorial.
\item \textbf{Types as first class values}: links to articles.
\item \textbf{Tutorial}: kernel-integrated plug-ins are now deprecated.
diff --git a/doc/developer/examples/callstack.ml b/doc/developer/examples/callstack.ml
index c08cff551558f36f7cf49ad7982fb0b8dd4f7a49..e5b5380a728743447d19e0a4a823b685b52712f8 100644
--- a/doc/developer/examples/callstack.ml
+++ b/doc/developer/examples/callstack.ml
@@ -11,7 +11,7 @@
(* *)
(**************************************************************************)
-module P =
+module P =
Plugin.Register
(struct
let name = "Callstack"
@@ -28,10 +28,10 @@ type callstack = (Kernel_function.t * Cil_datatype.Stmt.t) list
let empty = []
let push kf stmt stack = (kf, stmt) :: stack
let pop = function [] -> [] | _ :: stack -> stack
-let rec print = function
- | [] -> P.feedback ""
- | (kf, stmt) :: stack ->
- P.feedback "function %a called at stmt %a"
+let rec print = function
+ | [] -> P.feedback ""
+ | (kf, stmt) :: stack ->
+ P.feedback "function %a called at stmt %a"
Kernel_function.pretty kf
Cil_datatype.Stmt.pretty stmt;
print stack
@@ -51,7 +51,7 @@ module D =
(* Dynamic API registration *)
let register name ty =
- Dynamic.register ~plugin:"Callstack" ~journalize:false name ty
+ Dynamic.register ~plugin:"Callstack" name ty
let empty = register "empty" D.ty empty
let push = register "push" (Datatype.func3 kf_ty stmt_ty D.ty D.ty) push
diff --git a/doc/developer/hello_world/hello_world.ml b/doc/developer/hello_world/hello_world.ml
index 0c87e8eaacc363d3cc1ac984a75269a9c91bdf69..8fb440417ed1112b2367dfb47252b70e249cbf8f 100644
--- a/doc/developer/hello_world/hello_world.ml
+++ b/doc/developer/hello_world/hello_world.ml
@@ -39,17 +39,15 @@ let print () = Self.result "Hello world!"
(** The function [print] below is not mandatory: you can ignore it in a first
reading. It provides an API for the plug-in, so that the function [run] is
- callable by another plug-in and journalized: first, each plug-in can call
+ callable by another plug-in: each plug-in can call
[Dynamic.get "Hello.run" (Datatype.func Datatype.unit Datatype.unit)] in
- order to call [print] and second, each call to [print] is written in the
- Frama-C journal. *)
+ order to call [print]. *)
let print =
Dynamic.register
~comment:"[Dynamic.get \"Hello.run\" (Datatype.func Datatype.unit \
Datatype.unit)] calls [run] and pretty prints \"Hello world!\""
~plugin:"Hello"
"run"
- ~journalize:true
(Datatype.func Datatype.unit Datatype.unit)
print
diff --git a/doc/developer/refman.tex b/doc/developer/refman.tex
index 5194764b5854c12159d772fffd483b5cf8eca37d..e8b4e3bcad586027f605d4bca45c8695a93ff9c8 100644
--- a/doc/developer/refman.tex
+++ b/doc/developer/refman.tex
@@ -876,7 +876,7 @@ one for regular tests (if more than one \verb|OPT|).\\
\hline
\verb|PTEST_SCRIPT| & current list of plugins defined by the \verb|SCRIPT| directive\\
\hline
-\verb|PTEST_DEFAULT_OPTIONS| & the default option list: \verb|-journal-disable| \verb|-check| \verb|-no-autoload-plugins|\\
+\verb|PTEST_DEFAULT_OPTIONS| & the default option list: \verb|-check| \verb|-no-autoload-plugins|\\
\hline
\verb|PTEST_LOAD_MODULE| & the \verb|-load-module| option related to the \verb|MODULE| directive\\
\hline
diff --git a/doc/developer/tutorial.tex b/doc/developer/tutorial.tex
index 832fee3fcc70f60857c2526e8fe0df54c365887e..2d4de400ff47375e3eac228c48c5d777aae64816 100644
--- a/doc/developer/tutorial.tex
+++ b/doc/developer/tutorial.tex
@@ -183,7 +183,6 @@ platform. This tutorial focuses on specific parts of this figure.
\node (dynamic) {Dynamic};
\node (plugin) {Plugin};
\node (type) {Type};
- \node (journal) {Journal};
\node (project) {Project};
\end{tikz-vbox}
};
@@ -202,14 +201,13 @@ platform. This tutorial focuses on specific parts of this figure.
($(options.west -| main-pt)+(-0.4\bigpadding,-\padding)$);
\draw (implem-pt -| implem.west) -- (implem-pt);
\draw[-Latex] (implem-pt) |- (type.east);
- \draw[-Latex] (implem-pt) |- (journal.east);
\draw[-Latex] ($(plugin-dir.west |- implem-pt)+(0,-\padding)$)
-- ($(implem-pt)+(0.2\bigpadding,-\padding)$) |- (project.east);
\end{tikzpicture}
\end{center}
\scodeidx{Db}{Main}\codeidx{Dynamic}\codeidx{Plugin}
-\codeidx{Project}\codeidx{Type}\codeidx{Journal}
+\codeidx{Project}\codeidx{Type}
\codeidx{Makefile.dynamic}\codeidx{Design}
\index{GUI}\index{Plug-in!GUI}
\caption{Plug-in Integration Overview.}\label{fig:overview}
@@ -704,7 +702,7 @@ implementation, we explain some of \framac APIs such as how to visit
an AST\footnote{Abstract Syntax Tree}, to hook a plug-in, to interface
a plug-in with other plug-ins, to extend the
GUI\footnote{Graphical User Interface}, to make a plug-in usable by
-others, to make write a plug-in into the journal, to configure a script,
+others, to configure a script,
and to make a plug-in usable in a multi-projects setting.
This section assumes the reader is already familiar with the basics of plug-ins
@@ -1104,27 +1102,6 @@ Here is the listing for the different modules:
% TODO: A script that uses "dump_function" of the CFG plug-in
-\subsection{Writing your Plug-in into the Journal}\label{tut2:journal}
-\index{Journalization}
-\todo
-
-% TODO: Journalize dump_function.
-
-% La journalisation, c'est le fait d'avoir la GUI rajouter des entrees
-% dans le journal, pour pouvoir les rejouer. Ca permet, quand on
-% paufine des analyses, de refaire ce qu'on a fait dans la gui
-% automatiquement; apres on peut utiliser load-script pour rejouer le
-% journal.
-
-% Pour journaliser, il faut enregister la fonction pour qu'elle soit
-% accessible de l'exterieur. Apres il y a un argument journalize qui
-% permet de journaliser. Si je fais ca pour ma fonction dump_function,
-% je vais recuperer une fonction dump_function_journalized; et c'est
-% celle ci-qu'il faudrait que j'utilise dans la GUI; comme ca a chaque
-% fois que je fais un "show-cfg", ce serait enregistre. La ce n'est
-% pas tres interessant parce que je ne fais pas de modification de
-% l'AST, mais dans le cas general ca l'est.
-
\subsection{Writing a Configure Script}\label{tut2:configure}
\index{Plug-in!Configure}
\todo
diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index 9a37650c699bfc7fbc81aa44272d09940a92b29a..60d058461dc268df9b646252cfbd1e0525314e8e 100644
--- a/doc/userman/user-changes.tex
+++ b/doc/userman/user-changes.tex
@@ -3,6 +3,11 @@
This chapter summarizes the changes in this documentation between each \FramaC
release. First we list changes of the last release.
+\section*{Frama-C+dev}
+\begin{itemize}
+\item Removed Journalisation
+\end{itemize}
+
\section*{24.0 (Chromium)}
\begin{itemize}
\item \textbf{Standard library (libc):} Section added
@@ -132,9 +137,9 @@ in using the Frama-C OPAM package.
active by default.
\item \textbf{Normalizing the Source Code:} added section about macros
predefined by \FramaC (Section~\ref{sec:predefined-macros}).
-\item \textbf{Normalizing the Source Code:} document new option
+\item \textbf{Normalizing the Source Code:} document new option
\texttt{-custom-annot-char} (Section~\ref{sec:normalize})
-\item \textbf{Normalizing the Source Code:} document handling of
+\item \textbf{Normalizing the Source Code:} document handling of
new file suffix \texttt{.ci} (Section~\ref{sec:preprocessing})
\item \textbf{Preparing the Sources:} option \texttt{-warn-undefined-callee}
changed to \\ \texttt{-implicit-function-declaration warn}.
@@ -158,14 +163,14 @@ predefined by \FramaC (Section~\ref{sec:predefined-macros}).
\section*{Neon-20140*01}
\begin{itemize}
-\item \textbf{Getting Started:} fixes list of requirements
+\item \textbf{Getting Started:} fixes list of requirements
for compiling \FramaC.
\item \textbf{Preparing the Sources:} new option \texttt{-aggressive-merging}
\item \textbf{General Kernel Services:} change the default name of the journal.
-\item \textbf{Getting Started:}
+\item \textbf{Getting Started:}
new options \texttt{-config} and \texttt{-<plug-in shortname>-config}, as
well as new environment variable \texttt{FRAMAC\_CONFIG}.
-\item \textbf{Getting Started:}
+\item \textbf{Getting Started:}
new options \texttt{-session} and \texttt{-<plug-in shortname>-session}, as
well as new environment variable \texttt{FRAMAC\_SESSION}.
\item \textbf{Getting Started:} document option \texttt{-unicode}.
@@ -188,7 +193,7 @@ predefined by \FramaC (Section~\ref{sec:predefined-macros}).
\section*{Oxygen-20120901}
\begin{itemize}
-\item \textbf{Analysis Option:} better documentation of
+\item \textbf{Analysis Option:} better documentation of
\texttt{-unspecified-access}
\item \textbf{Preparing the Sources:} better documentation of \texttt{-pp-annot}
\item \textbf{Preparing the Sources:} pragma \texttt{UNROLL\_LOOP} is
diff --git a/doc/userman/user-services.tex b/doc/userman/user-services.tex
index 24aca42be20f94c4c5714a43cd1ca11ecbb66cc6..838b5974d334a8ad6200e619d374bbea35f2273c 100644
--- a/doc/userman/user-services.tex
+++ b/doc/userman/user-services.tex
@@ -5,7 +5,7 @@ This chapter presents some important services offered by the \FramaC platform.
\section{Projects}\label{sec:project}\index{Project|bfit}
A \FramaC project groups together one source code with the states (parameters,
-results, \etc) of the \FramaC kernel and analyzers.
+results, \etc) of the \FramaC kernel and analyzers.
In one \FramaC session, several projects may exist at the same time, while
there is always one and only one so-called \emph{current} project in which
@@ -87,8 +87,8 @@ loading another project file.
\paragraph{Special Cases}
Options \optionuse{-}{help}, \optionuse{-}{verbose},
-\optionuse{-}{debug}\xspace(and
-their corresponding plugin-specific counterpart)
+\optionuse{-}{debug}\xspace(and
+their corresponding plugin-specific counterpart)
as well as \optionuse{-}{explain}, \optionuse{-}{quiet}\xspace and
\optionuse{-}{unicode}\xspace are not saved on disk.
@@ -137,53 +137,3 @@ analysis $A_2$. Whenever the results from $A_2$ change, \FramaC automatically di
results from $A_1$. For instance, slicing results depend on value analysis
results; thus the slicing results are discarded whenever the value analysis
ones are.
-
-\section{Journalisation}\label{sec:journal}
-
-Journalisation logs each operation that modifies some parameters or results
-into a file called a \emph{journal}\index{Journal|bfit}. Observational
-operations like viewing the set of possibles values of a variable in the GUI
-are not logged.
-
-By default, the name of the journal is
-\texttt{SESSION\_DIR/frama\_c\_journal.ml} where \texttt{SESSION\_DIR} is the
-\FramaC session directory (see Section~\ref{sec:var-session}). It can be
-modified by using the option \optiondef{-}{journal-name}.
-
-A journal is a valid \FramaC dynamic plug-in. Thus it can be loaded by using
-the option \optionuse{-}{load-script} (see Section~\ref{sec:use-plugins}). The
-journal replays the very same results as the ones computed in the original
-session.
-
-Journals are commonly used for the three different purposes described
-thereafter.
-\begin{itemize}
-\item Easily replaying a given set of analysis operations in order to reach a
- certain state. Once the final state is reached, further analyses can be
- performed normally. Beware that journals may be source dependent and thus may
- not necessarily be reused on different source codes to perform the same
- analyses.
-%
-\item Acting as a macro language for plug-in developers. They can perform
- actions on the GUI to generate a journal and then adapt it to perform
- a more general but similar task.
-%
-\item Debugging. In the GUI, a journal is always generated, even when an error
- occurs. The output journal usually contains information about this
- error. Thus it provides an easy way to reproduce the very same
- error. Consequently, it is advised to attach the journal when reporting an
- error in the \FramaC BTS (see Chapter~\ref{user-errors}).
-\end{itemize}
-
-By default, a journal is generated upon exit of the session only whenever
-\FramaC crashes in graphical mode. In all other cases, no journal is
-generated. This behavior may be customized by using the option
-\optiondef{-}{journal-enable} (resp. \optiondef{-}{journal-disable}) that
-generates (resp. does not generate) a journal upon exiting the session.
-
-\paragraph{Special Cases}
-
-Modifications of options \optionuse{-}{help}, \optionuse{-}{verbose},
-\optionuse{-}{debug}\xspace (and their corresponding counterpart) as well as
-\optionuse{-}{explain}, \optionuse{-}{quiet}\xspace and
-\optionuse{-}{unicode}\xspace are not written in the journal.
diff --git a/doc/userman/user-start.tex b/doc/userman/user-start.tex
index 96c072ccf509912b50cb84e58663248213775d2f..0810f44626e3c42cd861c0b98f0c68eaa91c6cd3 100644
--- a/doc/userman/user-start.tex
+++ b/doc/userman/user-start.tex
@@ -189,11 +189,8 @@ for using the Unicode character set in messages has an opposite option
with
a name of the form \texttt{-<plug-in name>-<option name>} have their opposite
option named \texttt{-<plug-in name>-no-<option name>}. For instance, the
-opposite of option \optionuse{-}{wp-print} is \optionuse{-}{wp-no-print}. When
-prefixing
-an option name by \texttt{-no} is meaningless, the opposite option is usually
-renamed. For instance, the opposite option of \optionuse{-}{journal-enable} is
-\optionuse{-}{journal-disable}. Use the options \texttt{-kernel-help} and
+opposite of option \optionuse{-}{wp-print} is \optionuse{-}{wp-no-print}.
+Use the options \texttt{-kernel-help} and
\texttt{-<plug-in name>-help} to get the opposite option name of each
parameterless option.
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index e34347acdd061e025cfff74a0507b0f5dfac4d46..e635e42c3a12a14c3fd985f486d40ecff5b48673 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -657,8 +657,6 @@ src/kernel_services/plugin_entry_points/dynamic.ml: CEA_LGPL
src/kernel_services/plugin_entry_points/dynamic.mli: CEA_LGPL
src/kernel_services/plugin_entry_points/emitter.ml: CEA_LGPL
src/kernel_services/plugin_entry_points/emitter.mli: CEA_LGPL
-src/kernel_services/plugin_entry_points/journal.ml: CEA_LGPL
-src/kernel_services/plugin_entry_points/journal.mli: CEA_LGPL
src/kernel_services/plugin_entry_points/kernel.ml: CEA_LGPL
src/kernel_services/plugin_entry_points/kernel.mli: CEA_LGPL
src/kernel_services/plugin_entry_points/log.ml: CEA_LGPL
@@ -826,8 +824,6 @@ src/plugins/callgraph/cg.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/callgraph/cg.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/callgraph/cg_viewer.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/callgraph/cg_viewer.yes.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/callgraph/journalize.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/callgraph/journalize.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/callgraph/options.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/callgraph/options.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/callgraph/register.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/man/frama-c.1 b/man/frama-c.1
index 969afd9eac24f67f59b967eef0e51b17082bed4c..cab04ada2a14a815fa490e0f537193f47d4ca80f 100644
--- a/man/frama-c.1
+++ b/man/frama-c.1
@@ -3,13 +3,13 @@
.TH "FRAMA-C" "1" "" "2021-06-18" ""
.hy
.\"------------------------------------------------------------------------
-.\"
-.\" This file is part of Frama-C documentation
-.\"
-.\" Copyright (C) 2007-2021
-.\" CEA (Commissariat à l'énergie atomique et aux énergies
-.\" alternatives)
-.\"
+.\"
+.\" This file is part of Frama-C documentation
+.\"
+.\" Copyright (C) 2007-2021
+.\" CEA (Commissariat à l'énergie atomique et aux énergies
+.\" alternatives)
+.\"
.\" you can redistribute it and/or modify it under the terms of the
.\" CC-BY-SA 4.0 license
@@ -293,21 +293,6 @@ Use \f[B]\[at]inline\f[R] to select all functions with attribute
Recursive functions are inlined only at the first level.
Calls via function pointers are not inlined.
.TP
--journal-disable
-do not output a journal of the current session.
-See \f[B]-journal-enable\f[R].
-.TP
--journal-enable
-on by default, dumps a journal of all the actions performed during the
-current Frama-C session in the form of an OCaml script that can be
-replayed with \f[B]-load-script\f[R].
-The name of the script can be set with the \f[B]-journal-name\f[R]
-option.
-.TP
--journal-name \f[I]name\f[R]
-sets the name of the journal file (without the \f[I].ml\f[R] extension).
-Defaults to \f[B]frama_c_journal\f[R].
-.TP
-json-compilation-database \f[I]path\f[R]
use \f[I]path\f[R] as a JSON compilation database (see
<https://clang.llvm.org/docs/JSONCompilationDatabase.html> for more
diff --git a/man/frama-c.1.md b/man/frama-c.1.md
index 3d7aabda6cd921a3a8a6801f53049016bdd1671f..fb1a43b2009baed522145559583248f0b2dbe6a8 100644
--- a/man/frama-c.1.md
+++ b/man/frama-c.1.md
@@ -4,13 +4,13 @@ header-includes:
- |
```{=man}
.\"------------------------------------------------------------------------
- .\"
- .\" This file is part of Frama-C documentation
- .\"
- .\" Copyright (C) 2007-2021
- .\" CEA (Commissariat à l'énergie atomique et aux énergies
- .\" alternatives)
- .\"
+ .\"
+ .\" This file is part of Frama-C documentation
+ .\"
+ .\" Copyright (C) 2007-2021
+ .\" CEA (Commissariat à l'énergie atomique et aux énergies
+ .\" alternatives)
+ .\"
.\" you can redistribute it and/or modify it under the terms of the
.\" CC-BY-SA 4.0 license
@@ -248,19 +248,6 @@ Use **@inline** to select all functions with attribute *inline*.
Recursive functions are inlined only at the first level.
Calls via function pointers are not inlined.
--journal-disable
-: do not output a journal of the current session. See **-journal-enable**.
-
--journal-enable
-: on by default, dumps a journal of all the actions performed during the
-current Frama-C session in the form of an OCaml script that can be replayed
-with **-load-script**. The name of the script can be set with the
-**-journal-name** option.
-
--journal-name *name*
-: sets the name of the journal file (without the *.ml* extension).
-Defaults to **frama_c_journal**.
-
-json-compilation-database *path*
: use *path* as a JSON compilation database
(see <https://clang.llvm.org/docs/JSONCompilationDatabase.html>
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index cbd6875ae3dfa21c5c8fb22eafd9e53097703f1e..d797d5076b8c73de467757745cc1896a91b2452c 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -355,7 +355,7 @@ let exclude s = exclude_suites := s :: !exclude_suites
let macro_post_options = ref "" (* value set to @PTEST_POST_OPTIONS@ macro *)
let macro_pre_options = ref "" (* value set to @PTEST_PRE_OPTIONS@ macro *)
let macro_options = ref "@PTEST_PRE_OPTIONS@ @PTEST_OPT@ @PTEST_POST_OPTIONS@"
-let macro_default_options = ref "-journal-disable -check -no-autoload-plugins"
+let macro_default_options = ref "-check -no-autoload-plugins"
let macro_frama_c_cmd = ref "@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@"
let macro_frama_c = ref "@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@ @PTEST_LOAD_OPTIONS@"
diff --git a/share/Makefile.config.in b/share/Makefile.config.in
index c6d808f04e906cb195778fae19e2a20e7a9070a1..cab716c2a9744582c940695436017801e308f71c 100644
--- a/share/Makefile.config.in
+++ b/share/Makefile.config.in
@@ -163,7 +163,7 @@ HAVE_BUILTIN_VA_LIST ?=@HAVE_BUILTIN_VA_LIST@
# test directories for ptests configuration
# Non-plugin test directories containing some ML files to compile
TEST_DIRS_AS_PLUGIN:=\
- dynamic journal saveload spec misc syntax cil \
+ dynamic saveload spec misc syntax cil \
pretty_printing builtins libc value
ifeq ($(HAS_PYTHON36),yes)
diff --git a/src/kernel_internals/typing/rmtmps.ml b/src/kernel_internals/typing/rmtmps.ml
index 3b3eaadd34889a78bfab20890733789dd0e0e407..160f27ea9dc56848e41658d3ba06084c20865827 100644
--- a/src/kernel_internals/typing/rmtmps.ml
+++ b/src/kernel_internals/typing/rmtmps.ml
@@ -861,7 +861,7 @@ let removeUnmarked isRoot ast reachable_tbl =
begin
try
let kf = Globals.Functions.get vi in
- Kernel.debug ~dkey "GFunDecl: %a@." Kernel_function.pretty_code kf
+ Kernel.debug ~dkey "GFunDecl: %a@." Kernel_function.pretty kf
with Not_found ->
Kernel.debug ~dkey
"GFunDecl: %a (no associated kernel function)@."
diff --git a/src/kernel_services/abstract_interp/abstract_interp.ml b/src/kernel_services/abstract_interp/abstract_interp.ml
index 31de26b07b835d03c23d07fc916ecd04baf279a0..64798a80127fd5ffecae59774b474a6e3f3a4cf8 100644
--- a/src/kernel_services/abstract_interp/abstract_interp.ml
+++ b/src/kernel_services/abstract_interp/abstract_interp.ml
@@ -222,9 +222,7 @@ module Make_Generic_Lattice_Set
let hash = hash
let rehash = Datatype.identity
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty = pretty
- let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
end) :
Datatype.S with type t := t)
@@ -364,9 +362,7 @@ module Make_Lattice_Base (V:Lattice_Value):(Lattice_Base with type l = V.t) = st
let hash = hash
let rehash = Datatype.identity
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty = pretty
- let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
end) :
Datatype.S with type t := t)
@@ -517,8 +513,6 @@ module Bool = struct
let rehash = Datatype.identity
let copy = Datatype.identity
let pretty = pretty
- let internal_pretty_code = Datatype.undefined
- let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
end) :
Datatype.S with type t := t)
@@ -677,9 +671,7 @@ struct
let hash = hash
let rehash = Datatype.identity
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty = pretty
- let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
end) :
Datatype.S with type t := t)
@@ -777,9 +769,7 @@ struct
let hash = hash
let rehash = Datatype.identity
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty = pretty
- let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
end):
Datatype.S with type t := t)
@@ -947,9 +937,7 @@ struct
let hash = hash
let rehash = Datatype.undefined
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty = pretty
- let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
end)
let () = Type.set_ml_name ty None
diff --git a/src/kernel_services/abstract_interp/base.ml b/src/kernel_services/abstract_interp/base.ml
index 2ebe0f3efa129c9d60576ec84dd1b4d5d105eb40..e0b94048054efd2e308450022bdc9a7c79de202d 100644
--- a/src/kernel_services/abstract_interp/base.ml
+++ b/src/kernel_services/abstract_interp/base.ml
@@ -99,10 +99,8 @@ module Validity = Datatype.Make
let pretty = pretty_validity
let mem_project = Datatype.never_any_project
- let internal_pretty_code = Datatype.pp_fail
let rehash = Datatype.identity
let copy (x:t) = x
- let varname _ = "v"
end)
type cstring = CSString of string | CSWstring of Escape.wstring
@@ -450,10 +448,8 @@ module Base = struct
let pretty = pretty
let hash = hash
let mem_project = Datatype.never_any_project
- let internal_pretty_code = Datatype.pp_fail
let rehash = Datatype.identity
let copy = Datatype.undefined
- let varname = Datatype.undefined
end)
let id = id
let pretty_debug = pretty
diff --git a/src/kernel_services/abstract_interp/int_Base.ml b/src/kernel_services/abstract_interp/int_Base.ml
index 2aab074ee278371a381fbfc68e825606eef557bc..be9b6f846f68956a664b31fe84728c64323092c2 100644
--- a/src/kernel_services/abstract_interp/int_Base.ml
+++ b/src/kernel_services/abstract_interp/int_Base.ml
@@ -55,9 +55,7 @@ include Datatype.Make
let hash = hash
let rehash = Datatype.identity
let copy = Extlib.id
- let internal_pretty_code = Datatype.undefined
let pretty = pretty
- let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
end)
diff --git a/src/kernel_services/abstract_interp/int_interval.ml b/src/kernel_services/abstract_interp/int_interval.ml
index f1eb54dada1209a83225a2b0b5017fb34e7be71b..1b1979547e273dc830d327270dd7f025520da255 100644
--- a/src/kernel_services/abstract_interp/int_interval.ml
+++ b/src/kernel_services/abstract_interp/int_interval.ml
@@ -94,10 +94,8 @@ include Datatype.Make_with_collections
let hash = hash
let pretty = pretty
let rehash = Datatype.identity
- let internal_pretty_code = Datatype.pp_fail
let mem_project = Datatype.never_any_project
let copy = Datatype.undefined
- let varname = Datatype.undefined
end)
(* ------------------------------ Building ---------------------------------- *)
diff --git a/src/kernel_services/abstract_interp/int_set.ml b/src/kernel_services/abstract_interp/int_set.ml
index 1d5a7fad690e76287ed21e296371fcd9b25df308..69bf59a6a0284764997b8876a959acdfb4f02a99 100644
--- a/src/kernel_services/abstract_interp/int_set.ml
+++ b/src/kernel_services/abstract_interp/int_set.ml
@@ -130,10 +130,8 @@ include Datatype.Make_with_collections
let hash = hash
let pretty = pretty
let rehash x = x
- let internal_pretty_code = Datatype.pp_fail
let mem_project = Datatype.never_any_project
let copy = Datatype.undefined
- let varname = Datatype.undefined
end)
(* ---------------------------------- Utils --------------------------------- *)
diff --git a/src/kernel_services/abstract_interp/int_val.ml b/src/kernel_services/abstract_interp/int_val.ml
index 8fb7cf1b226f052663ef9f58979897e86792d1da..b8e450700314d6eeff3276db67085973a11765cd 100644
--- a/src/kernel_services/abstract_interp/int_val.ml
+++ b/src/kernel_services/abstract_interp/int_val.ml
@@ -75,10 +75,8 @@ include Datatype.Make_with_collections
let hash = hash
let pretty = pretty
let rehash x = x
- let internal_pretty_code = Datatype.pp_fail
let mem_project = Datatype.never_any_project
let copy = Datatype.undefined
- let varname = Datatype.undefined
end)
(* ------------------------------- Constructors ---------------------------- *)
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index 2384610cb9f8af4512699f51a1cbc2421bf6f758..2ff6f24df697f122f27a031ceb72af5d645c87a0 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -824,10 +824,8 @@ include (
let hash = hash
let pretty = pretty
let rehash = rehash
- let internal_pretty_code = Datatype.pp_fail
let mem_project = Datatype.never_any_project
let copy = Datatype.undefined
- let varname = Datatype.undefined
end):
Datatype.S_with_collections with type t := t)
diff --git a/src/kernel_services/abstract_interp/lmap.ml b/src/kernel_services/abstract_interp/lmap.ml
index afe85f50c5b901176bd733b5884258627c85ea3e..dfc598b3c3d670b8ee5862b3f08230206535680c 100644
--- a/src/kernel_services/abstract_interp/lmap.ml
+++ b/src/kernel_services/abstract_interp/lmap.ml
@@ -591,10 +591,8 @@ struct
let compare = compare
let hash = hash
let pretty = pretty
- let internal_pretty_code = Datatype.undefined
let rehash = Datatype.identity
let copy = Datatype.undefined
- let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
end)
let () = Type.set_ml_name ty None
diff --git a/src/kernel_services/abstract_interp/lmap_bitwise.ml b/src/kernel_services/abstract_interp/lmap_bitwise.ml
index ee6e25cad0d1d230c328933d10ed64192b07ae5e..a9a113e386729a4281e618da8cea4bd2ed4c8498 100644
--- a/src/kernel_services/abstract_interp/lmap_bitwise.ml
+++ b/src/kernel_services/abstract_interp/lmap_bitwise.ml
@@ -238,10 +238,8 @@ struct
let equal = equal
let compare = compare
let pretty = pretty
- let internal_pretty_code = Datatype.undefined
let rehash = Datatype.identity
let copy = Datatype.undefined
- let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
end)
diff --git a/src/kernel_services/abstract_interp/map_lattice.ml b/src/kernel_services/abstract_interp/map_lattice.ml
index 28d864d5708fe0c885895909eb9cd45193c83429..26b609c52adad23cb0aa013707ce137321acf806 100644
--- a/src/kernel_services/abstract_interp/map_lattice.ml
+++ b/src/kernel_services/abstract_interp/map_lattice.ml
@@ -498,10 +498,8 @@ module Make_MapSet_Lattice
let hash = hash
let rehash = Datatype.identity
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.pp_fail
let pretty = pretty
let mem_project = Datatype.never_any_project
- let varname = Datatype.undefined
end): Datatype.S_with_collections with type t := t)
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index 98a53b5f61d76d9e3d6b63eb55c9e7a11188c812..509c41f0d5043f682f8a64c36d5fdbdbb18a5b4c 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -229,9 +229,7 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
let compare = compare
let rehash x = !rehash_ref x
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty = pretty
- let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
end)
include D
@@ -2460,8 +2458,6 @@ module Int_Intervals = struct
Int.packed_descr; Int.packed_descr |] |]
let mem_project = Datatype.never_any_project
- let varname _ = "i"
- let internal_pretty_code = Datatype.undefined
let copy = Datatype.undefined
end)
diff --git a/src/kernel_services/abstract_interp/origin.ml b/src/kernel_services/abstract_interp/origin.ml
index c31e62808d56c7b8072205110d01fd31041f417f..6622574bd63cefd2cc86ffc06a580bc478ea2370 100644
--- a/src/kernel_services/abstract_interp/origin.ml
+++ b/src/kernel_services/abstract_interp/origin.ml
@@ -135,9 +135,7 @@ include Datatype.Make
let hash = hash
let rehash = Datatype.undefined
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty = pretty
- let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
end)
diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index ce0c8902d6ff10d013c553f57e394948600fe0bd..7f7451c7ae1a27ba1a73ccba3fe01ef2e5607efb 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -240,7 +240,6 @@ module D =
let structural_descr = Structural_descr.t_abstract
let rehash = Datatype.identity
- let varname = Datatype.undefined
let pretty fmt = function
| Division_by_zero e ->
@@ -308,7 +307,6 @@ module D =
| Invalid_bool lv ->
Format.fprintf fmt "Invalid_bool(@[%a@])" Lval.pretty lv
- let internal_pretty_code = Datatype.undefined
let copy = Datatype.undefined
let mem_project = Datatype.never_any_project
end)
diff --git a/src/kernel_services/ast_data/globals.ml b/src/kernel_services/ast_data/globals.ml
index cc79e169f7a5eec485c4d144ac0dad50bbf343c3..06f17de617ad1c311b46ac76127c933f0f423cd4 100644
--- a/src/kernel_services/ast_data/globals.ml
+++ b/src/kernel_services/ast_data/globals.ml
@@ -91,17 +91,6 @@ module Vars = struct
let get_astinfo vi = !get_astinfo_ref vi
- let pp_varinfo p fmt v =
- let name, loc = get_astinfo v in
- let pp fmt =
- Format.fprintf fmt "@[<hv 2>Globals.Vars.find_from_astinfo@;%S@;%a@]"
- name
- (Cil_datatype.Localisation.internal_pretty_code Type.Call) loc
- in
- Type.par p Type.Call fmt pp
-
- let () = Varinfo.internal_pretty_code_ref := pp_varinfo
-
let iter_globals f l =
let treat_global = function
| GVar(vi,init,_) -> f vi init
diff --git a/src/kernel_services/ast_data/property_status.ml b/src/kernel_services/ast_data/property_status.ml
index 552171036e72d27253e46c4999b8122a5dd54f35..46c82aeca51a4f89ebbc231346f44927c49b4da1 100644
--- a/src/kernel_services/ast_data/property_status.ml
+++ b/src/kernel_services/ast_data/property_status.ml
@@ -80,9 +80,6 @@ module Emitter_with_properties =
let copy = Datatype.undefined
let pretty fmt e = Usable_emitter.pretty fmt e.emitter
- let internal_pretty_code = Datatype.undefined
- let varname _ = assert false (* unused while [internal_pretty_code]
- unimplemented *)
let mem_project = Datatype.never_any_project
end)
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index c7551b0733be41b396abf71790e09045a5c16ef7..ffa3ca42bd6e2993e9d6151e8c80e019c8297c6d 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -59,17 +59,9 @@ struct
let map f = function
| `Same x -> `Same (f x)
| `Not_present -> `Not_present
- let mk_internal_pretty_code pp prec fmt = function
- | `Not_present -> Format.pp_print_string fmt "`Not_present"
- | `Same x ->
- let pp fmt = Format.fprintf fmt "`Same %a" (pp Type.Call) x in
- Type.par prec Call fmt pp
let mk_pretty pp fmt = function
| `Not_present -> Format.pp_print_string fmt "N/A"
| `Same x -> Format.fprintf fmt " => %a" pp x
- let mk_varname v = function
- | `Not_present -> "x"
- | `Same x -> v x ^ "_c"
let mk_mem_project mem query = function
| `Not_present -> false
| `Same x -> mem query x
@@ -111,12 +103,6 @@ let compare_pc pc1 pc2 =
| _, `Callees_changed -> 1
| `Callees_spec_changed, `Callees_spec_changed -> 0
-let string_of_pc = function
- | `Spec_changed -> "Spec_changed"
- | `Body_changed -> "Body_changed"
- | `Callees_changed -> "Callees_changed"
- | `Callees_spec_changed -> "Callees_spec_changed"
-
let pretty_pc fmt =
let open Format in
function
@@ -163,25 +149,11 @@ struct
| `Partial(x,pc) -> `Partial(f x,pc)
| (#correspondance as x) -> Correspondance_input.map f x
- let mk_internal_pretty_code pp prec fmt = function
- | `Partial (x,flags) ->
- let pp fmt =
- Format.fprintf fmt "`Partial (%a,%s)"
- (pp Type.Call) x (string_of_pc flags)
- in
- Type.par prec Call fmt pp
- | #correspondance as x ->
- Correspondance_input.mk_internal_pretty_code pp prec fmt x
-
let mk_pretty pp fmt = function
| `Partial(x,flags) ->
Format.fprintf fmt "-> %a %a" pp x pretty_pc flags
| #correspondance as x -> Correspondance_input.mk_pretty pp fmt x
- let mk_varname f = function
- | `Partial (x,_) -> f x ^ "_pc"
- | #correspondance as x -> Correspondance_input.mk_varname f x
-
let mk_mem_project f p = function
| `Partial (x,_) -> f p x
| #correspondance as x -> Correspondance_input.mk_mem_project f p x
diff --git a/src/kernel_services/ast_queries/cil_builtins.ml b/src/kernel_services/ast_queries/cil_builtins.ml
index 4d0545f91f3f05c0e4251f395a25a5748f373bbe..9a825e39a8e08641d6d7de780e0b363fbed8d1cc 100644
--- a/src/kernel_services/ast_queries/cil_builtins.ml
+++ b/src/kernel_services/ast_queries/cil_builtins.ml
@@ -160,7 +160,6 @@ module Builtin_template = struct
let hash b = Datatype.String.hash b.name
let equal b1 b2 = b1.name = b2.name
let copy = Datatype.identity
- let internal_pretty_code = Datatype.undefined
let pretty fmt b =
Format.fprintf fmt "%s %s(%a%s)"
b.rettype b.name
@@ -169,7 +168,6 @@ module Builtin_template = struct
let rehash = Datatype.identity
let structural_descr = Structural_descr.t_abstract
let mem_project = Datatype.never_any_project
- let varname b = "_cb_" ^ b.name
end)
end
module Builtin_templates =
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 31b139bdd6bd451ebf2f4fedcb10d11c8cb89481..fc0cb69ce023145ce2fe1f9c6b60ce97aaace365 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -48,9 +48,7 @@ module Make
type t
val name: string
val reprs: t list
- val internal_pretty_code: Type.precedence -> Format.formatter -> t -> unit
val pretty: Format.formatter -> t -> unit
- val varname: t -> string
end) =
Datatype.Make
(struct
@@ -69,9 +67,7 @@ module Make_with_collections
val reprs: t list
val compare: t -> t -> int
val equal: t -> t -> bool
- val internal_pretty_code: Type.precedence -> Format.formatter -> t -> unit
val pretty: Format.formatter -> t -> unit
- val varname: t -> string
val hash: t -> int
val copy: t -> t
end) =
@@ -160,8 +156,6 @@ module Cabs_file = struct
let name = "Cabs_file"
let reprs = [ Datatype.Filepath.dummy, [];
Datatype.Filepath.dummy, [ true, Cabs.GLOBANNOT [] ] ]
- let varname (s, _) = "cabs_" ^ (Filepath.Normalized.to_pretty_string s)
- let internal_pretty_code = Datatype.undefined
let pretty fmt cabs = !pretty_ref fmt cabs
end)
end
@@ -199,9 +193,7 @@ module Position = struct
let hash = Hashtbl.hash
let copy = Datatype.identity
let equal: t -> t -> bool = ( = )
- let internal_pretty_code = Datatype.undefined
let pretty = Filepath.pp_pos
- let varname _ = "pos"
end)
let pp_with_col fmt pos =
Format.fprintf fmt "%a char %d" pretty pos
@@ -224,9 +216,7 @@ module Location = struct
let hash (b, _e) = Hashtbl.hash (b.Filepath.pos_path, b.Filepath.pos_lnum)
let copy = Datatype.identity (* immutable strings *)
let equal : t -> t -> bool = ( = )
- let internal_pretty_code = Datatype.undefined
let pretty fmt loc = !pretty_ref fmt loc
- let varname _ = "loc"
end)
let pretty_long fmt loc =
@@ -274,9 +264,7 @@ module Instr = struct
type t = instr
let name = "Instr"
let reprs = List.map (fun l -> Skip l) Location.reprs
- let internal_pretty_code = Datatype.undefined
let pretty fmt x = !pretty_ref fmt x
- let varname = Datatype.undefined
end)
let loc = function
@@ -300,7 +288,6 @@ module File =
globinit = None;
globinitcalled = false } ]
include Datatype.Undefined
- let varname _ = "ast"
end)
module Stmt_Id = struct
@@ -321,15 +308,7 @@ module Stmt_Id = struct
let hash t1 = t1.sid
let equal t1 t2 = t1.sid = t2.sid
let copy = Datatype.undefined
- let internal_pretty_code p_caller fmt s =
- let pp fmt =
- Format.fprintf fmt
- "@[<hv 2>fst@;@[<hv 2>(Kernel_function.find_from_sid@;%d)@]@]"
- s.sid
- in
- Type.par p_caller Type.Call fmt pp
let pretty fmt s = !pretty_ref fmt s
- let varname _ = "stmt"
end)
let id stmt = stmt.sid
end
@@ -378,20 +357,10 @@ module Kinstr = struct
| Kglobal -> 1 lsl 29
| Kstmt s -> s.sid
let copy = Datatype.undefined
- let internal_pretty_code p fmt = function
- | Kglobal ->
- Format.fprintf fmt "Kglobal"
- | Kstmt s ->
- let pp fmt =
- Format.fprintf fmt "@[<hv 2>Kstmt@;%a@]"
- (Stmt.internal_pretty_code Type.Call) s
- in
- Type.par p Type.Call fmt pp
let pretty fmt = function
| Kglobal ->
Format.fprintf fmt "Kglobal"
| Kstmt s -> Stmt.pretty fmt s
- let varname _ = "ki"
end)
let loc = function
@@ -617,9 +586,7 @@ module Attribute=struct
let hash = hash_attribute config
let equal = Datatype.from_compare
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt t = !pretty_ref fmt t
- let varname = Datatype.undefined
end)
end
@@ -642,9 +609,7 @@ struct
let hash = hash_type M.config
let equal = Datatype.from_compare
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt t = !pretty_typ_ref fmt t
- let varname = Datatype.undefined
end)
end
@@ -736,9 +701,7 @@ module Label = struct
let name = "Label"
let reprs =
[ Label("", Location.unknown, false); Default Location.unknown ]
- let internal_pretty_code = Datatype.undefined
let pretty fmt l = !pretty_ref fmt l
- let varname = Datatype.undefined
let hash = function
| Default _ -> 7
| Case (e, _) -> Exp.hash e
@@ -767,7 +730,6 @@ end
module Varinfo_Id = struct
let pretty_ref = ref (fun _ _ -> assert false)
- let internal_pretty_code_ref = ref (fun _ _ _ -> assert false)
let dummy =
{ vname = "";
vorig_name = "";
@@ -798,9 +760,7 @@ module Varinfo_Id = struct
let hash v = v.vid
let equal v1 v2 = v1.vid = v2.vid
let copy = Datatype.undefined
- let internal_pretty_code p fmt v = !internal_pretty_code_ref p fmt v
let pretty fmt v = !pretty_ref fmt v
- let varname v = "vi_" ^ v.vorig_name
end)
let id v = v.vid
end
@@ -835,9 +795,7 @@ module Compinfo = struct
let hash v = Hashtbl.hash v.ckey
let equal v1 v2 = v1.ckey = v2.ckey
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt f = !pretty_ref fmt f
- let varname = Datatype.undefined
end)
end
@@ -878,9 +836,7 @@ module Fieldinfo = struct
let hash f1 = Hashtbl.hash (fid f1)
let equal f1 f2 = (fid f1) = (fid f2)
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt f = !pretty_ref fmt f
- let varname = Datatype.undefined
end)
end
@@ -1155,9 +1111,7 @@ module Block = struct
let reprs =
[{battrs=[]; blocals=Varinfo.reprs; bstatics = [];
bstmts=Stmt.reprs; bscoping=true}]
- let internal_pretty_code = Datatype.undefined
let pretty fmt b = !pretty_ref fmt b
- let varname = Datatype.undefined
end)
let equal b1 b2 = (b1 == b2)
end
@@ -1224,9 +1178,7 @@ module Lval = struct
let equal = equal_lval
let hash = hash_lval
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt x = !pretty_ref fmt x
- let varname _ = "lv"
end)
end
@@ -1240,9 +1192,7 @@ module LvalStructEq_input = struct
let equal = Datatype.from_compare
let hash = StructEq.hash_lval 13598
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt x = !Lval.pretty_ref fmt x
- let varname _ = "lv"
end
module LvalStructEq = Make_compare_non_strict(LvalStructEq_input)
@@ -1260,9 +1210,7 @@ module Offset = struct
let equal = equal_offset
let hash = hash_offset
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt x = !pretty_ref fmt x
- let varname _ = "offs"
end)
end
@@ -1276,9 +1224,7 @@ module OffsetStructEq_input = struct
let equal = Datatype.from_compare
let hash = StructEq.hash_offset 75489
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt x = !Offset.pretty_ref fmt x
- let varname _ = "offs"
end
module OffsetStructEq = Make_compare_non_strict(OffsetStructEq_input)
@@ -1311,9 +1257,7 @@ module Logic_var = struct
let hash v = v.lv_id
let equal v1 v2 = v1.lv_id = v2.lv_id
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt t = !pretty_ref fmt t
- let varname _ = "logic_var"
end)
end
@@ -1333,9 +1277,7 @@ module Builtin_logic_info = struct
let hash i = Hashtbl.hash i.bl_name
let equal i1 i2 = i1.bl_name = i2.bl_name
let copy = Datatype.identity (* works only if an AST is never modified *)
- let internal_pretty_code = Datatype.undefined
let pretty fmt li = !pretty_ref fmt li
- let varname = Datatype.undefined
end)
end
@@ -1351,9 +1293,7 @@ module Logic_type_info = struct
let equal t1 t2 = t1.lt_name = t2.lt_name
let hash t = Hashtbl.hash t.lt_name
let copy = Datatype.identity (* works only if an AST is never modified *)
- let internal_pretty_code = Datatype.undefined
let pretty fmt lt = !pretty_ref fmt lt
- let varname = Datatype.undefined
end)
end
@@ -1371,9 +1311,7 @@ module Logic_ctor_info = struct
let equal t1 t2 = t1.ctor_name = t2.ctor_name
let hash t = Hashtbl.hash t.ctor_name
let copy = Datatype.identity (* works only if an AST is never modified *)
- let internal_pretty_code = Datatype.undefined
let pretty fmt c = !pretty_ref fmt c
- let varname = Datatype.undefined
end)
end
@@ -1386,9 +1324,7 @@ module Initinfo = struct
let reprs =
{ init = None } ::
List.map (fun t -> { init = Some (CompoundInit(t, [])) }) Typ.reprs
- let internal_pretty_code = Datatype.undefined
let pretty fmt i = !pretty_ref fmt i
- let varname = Datatype.undefined
end)
end
@@ -1412,9 +1348,7 @@ module Logic_info = struct
let equal i1 i2 = Logic_var.equal i1.l_var_info i2.l_var_info
let hash i = Logic_var.hash i.l_var_info
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt li = !pretty_ref fmt li
- let varname _ = "logic_varinfo"
end)
end
@@ -1497,9 +1431,7 @@ module Logic_info_structural = struct
let equal = Datatype.from_compare
let hash i = Logic_var.hash i.l_var_info
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt li = !Logic_info.pretty_ref fmt li
- let varname _ = "logic_varinfo"
end)
end
@@ -2084,9 +2016,8 @@ module Logic_constant = struct
let equal = Datatype.from_compare
let hash = hash_logic_constant
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt lc = !pretty_ref fmt lc
- let varname _ = "lconst"
+
end)
end
@@ -2108,9 +2039,7 @@ module Term = struct
let equal = Datatype.from_compare
let copy = Datatype.undefined
let hash = hash_fct hash_term
- let internal_pretty_code = Datatype.undefined
let pretty fmt t = !pretty_ref fmt t
- let varname _ = "term"
end)
end
@@ -2128,9 +2057,7 @@ module Identified_term = struct
(* NB: Term.copy itself is undefined. *)
{ it_id = x.it_id; it_content = Term.copy x.it_content }
let hash x = x.it_id
- let internal_pretty_code = Datatype.undefined
let pretty fmt t = !pretty_ref fmt t
- let varname _ = "id_term"
end)
end
@@ -2153,9 +2080,7 @@ module Term_lhost = struct
let equal = Datatype.from_compare
let hash = hash_fct hash_tlhost
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt h = !pretty_ref fmt h
- let varname = Datatype.undefined
end)
end
@@ -2170,9 +2095,7 @@ module Term_offset = struct
let equal = Datatype.from_compare
let hash = hash_fct hash_toffset
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt t_o = !pretty_ref fmt t_o
- let varname = Datatype.undefined
end)
end
@@ -2198,9 +2121,7 @@ module Logic_label = struct
let equal = Datatype.from_compare
let copy = Datatype.undefined
let hash = hash_label
- let internal_pretty_code = Datatype.undefined
let pretty fmt l = !pretty_ref fmt l
- let varname _ = "logic_label"
end)
end
@@ -2219,9 +2140,7 @@ module Logic_real = struct
11 * Datatype.String.hash r.r_literal
let equal r1 r2 = compare r1 r2 = 0
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt t = !pretty_ref fmt t
- let varname _ = "logic_real"
end)
end
@@ -2232,9 +2151,7 @@ module Global_annotation = struct
type t = global_annotation
let name = "Global_annotation"
let reprs = List.map (fun l -> Daxiomatic ("", [],[], l)) Location.reprs
- let internal_pretty_code = Datatype.undefined
let pretty fmt v = !pretty_ref fmt v
- let varname = Datatype.undefined
let rec compare g1 g2 =
match g1,g2 with
@@ -2323,9 +2240,7 @@ module Global = struct
type t = global
let name = "Global"
let reprs = [ GText "" ]
- let internal_pretty_code = Datatype.undefined
let pretty fmt v = !pretty_ref fmt v
- let varname = Datatype.undefined
let compare g1 g2 =
match g1, g2 with
@@ -2478,15 +2393,8 @@ module Kf = struct
| Declaration (_, v, Some args, _) ->
!set_formal_decls v args;
x
- let get_name_kf kf = (vi kf).Cil_types.vname
- let internal_pretty_code p_caller fmt kf =
- Type.par p_caller Type.Call fmt
- (fun fmt ->
- Format.fprintf fmt "@[<hv 2>Globals.Functions.find_by_name@;%S@]"
- (get_name_kf kf))
let pretty fmt kf = Varinfo.pretty fmt (vi kf)
let mem_project = Datatype.never_any_project
- let varname kf = "kf_" ^ (get_name_kf kf)
end)
let () = Type.set_ml_name ty (Some "Kernel_function.ty")
@@ -2506,9 +2414,7 @@ module Code_annotation = struct
let equal x y = x.annot_id = y.annot_id
let compare x y = Datatype.Int.compare x.annot_id y.annot_id
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt ca = !pretty_ref fmt ca
- let varname _ = "code_annot"
end)
let loc ca = match ca.annot_content with
@@ -2530,9 +2436,7 @@ module Predicate = struct
[ { pred_name = [ "" ];
pred_loc = Location.unknown;
pred_content = Pfalse } ]
- let internal_pretty_code = Datatype.undefined
let pretty fmt x = !pretty_ref fmt x
- let varname _ = "p"
end)
end
@@ -2544,9 +2448,7 @@ module Toplevel_predicate = struct
let name = "Toplevel_predicate"
let reprs =
[ { tp_statement = List.hd Predicate.reprs; tp_kind = Assert }]
- let internal_pretty_code = Datatype.undefined
let pretty fmt x = !pretty_ref fmt x
- let varname _ = "p"
end)
end
@@ -2562,9 +2464,7 @@ module Identified_predicate = struct
let equal x y = x.ip_id = y.ip_id
let copy = Datatype.undefined
let hash x = x.ip_id
- let internal_pretty_code = Datatype.undefined
let pretty fmt x = !pretty_ref fmt x
- let varname _ = "id_predyes"
end)
end
@@ -2582,9 +2482,7 @@ module PredicateStructEq = struct
let equal = Datatype.from_compare
let copy = Datatype.undefined
let hash = hash_fct hash_predicate
- let internal_pretty_code = Datatype.undefined
let pretty fmt x = !pretty_ref fmt x
- let varname _ = "p"
end)
end
@@ -2650,7 +2548,6 @@ module Fundec = struct
(struct
type t = fundec
let name = "Fundec"
- let varname v = "fd_" ^ v.svar.vorig_name
let reprs = reprs
let structural_descr = Structural_descr.t_abstract
let compare v1 v2 = Datatype.Int.compare v1.svar.vid v2.svar.vid
@@ -2659,7 +2556,6 @@ module Fundec = struct
let rehash = Datatype.identity
let copy = Datatype.undefined
let pretty fmt f = !pretty_ref fmt f
- let internal_pretty_code = Datatype.undefined
let mem_project = Datatype.never_any_project
end)
end
@@ -2676,9 +2572,7 @@ module Lexpr = Make
type t = lexpr
let name = "Lexpr"
let reprs = [ { lexpr_node = PLvar ""; lexpr_loc = Location.unknown } ]
- let internal_pretty_code = Datatype.undefined
let pretty = Datatype.undefined (* TODO *)
- let varname = Datatype.undefined
end)
(**************************************************************************)
@@ -2692,19 +2586,6 @@ module Localisation =
type t = localisation
let name = "Localisation"
let reprs = [ VGlobal ]
- let internal_pretty_code p_caller fmt loc =
- let pp s kf =
- Type.par p_caller Type.Call fmt
- (fun fmt ->
- Format.fprintf fmt "@[<hv 2>%s@;%a@]"
- s
- (Kf.internal_pretty_code Type.Call)
- kf)
- in
- match loc with
- | VGlobal -> Format.fprintf fmt "Cil_types.VGlobal"
- | VLocal kf -> pp "Cil_types.VLocal" kf
- | VFormal kf -> pp "Cil_types.VFormal" kf
let mem_project = Datatype.never_any_project
end)
diff --git a/src/kernel_services/ast_queries/cil_datatype.mli b/src/kernel_services/ast_queries/cil_datatype.mli
index 807648fbb378e86a9e0df39f6810bc800242db47..08df42ea3ba4c412ea73d224d7f01fcc7f5c329f 100644
--- a/src/kernel_services/ast_queries/cil_datatype.mli
+++ b/src/kernel_services/ast_queries/cil_datatype.mli
@@ -268,9 +268,6 @@ module Varinfo: sig
val self: State.t
end
val dummy: t
- (**/**)
- val internal_pretty_code_ref:
- (Type.precedence -> Format.formatter -> t -> unit) ref
end
module Kf: sig
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 7bb60f13bd74e576c7e6f0eec94738a0bcbc9879..b3fa4fca000d301cbed097f3017df518d490e658 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -27,12 +27,6 @@ open Cil_datatype
type cpp_opt_kind = Gnu | Not_gnu | Unknown
-let pretty_cpp_opt_kind fmt =
- function
- | Gnu -> Format.pp_print_string fmt "Gnu"
- | Not_gnu -> Format.pp_print_string fmt "Not_gnu"
- | Unknown -> Format.pp_print_string fmt "Unknown"
-
type file =
| NeedCPP of
Filepath.Normalized.t (* Filename of the [.c] to preprocess. *)
@@ -62,22 +56,6 @@ module D =
let structural_descr = Structural_descr.t_abstract
let mem_project = Datatype.never_any_project
let copy = Datatype.identity (* immutable strings *)
- let internal_pretty_code p_caller fmt t =
- let pp fmt = match t with
- | NoCPP s ->
- Format.fprintf fmt "@[File.NoCPP %a@]" Filepath.Normalized.pretty s
- | External (f,p) ->
- Format.fprintf fmt "@[File.External (%a,%S)@]"
- Filepath.Normalized.pretty f p
- | NeedCPP (f,cmd,extra,kind) ->
- Format.fprintf
- fmt "@[File.NeedCPP (%a,%S,%S,%a)@]"
- Filepath.Normalized.pretty f
- cmd
- (String.concat " " extra)
- pretty_cpp_opt_kind kind
- in
- Type.par p_caller Type.Call fmt pp
end)
include D
@@ -1894,24 +1872,6 @@ let init_from_cmdline () =
Kernel.fatal "@[<v 0>Cannot initialize from C files@ \
Kernel raised Bad_Initialization %s@]" s
-let init_from_cmdline =
- Journal.register
- "File.init_from_cmdline"
- (Datatype.func Datatype.unit Datatype.unit)
- init_from_cmdline
-
-let init_from_c_files =
- Journal.register
- "File.init_from_c_files"
- (Datatype.func (Datatype.list ty) Datatype.unit)
- init_from_c_files
-
-let prepare_from_c_files =
- Journal.register
- "File.prepare_from_c_files"
- (Datatype.func Datatype.unit Datatype.unit)
- prepare_from_c_files
-
let () = Ast.set_default_initialization
(fun () ->
if Files.is_computed () then prepare_from_c_files ()
@@ -1924,21 +1884,8 @@ let pp_file_to fmt_opt =
| None -> Kernel.CodeOutput.output (fun fmt -> pp_ast fmt ast)
| Some fmt -> pp_ast fmt ast)
-let unjournalized_pretty prj (fmt_opt:Format.formatter option) () =
- Project.on prj pp_file_to fmt_opt
-
-let journalized_pretty_ast =
- Journal.register "File.pretty_ast"
- (Datatype.func3
- ~label1:("prj",Some Project.current) Project.ty
- ~label2:("fmt",Some (fun () -> None))
- (let module O = Datatype.Option(Datatype.Formatter) in
- O.ty)
- Datatype.unit Datatype.unit)
- unjournalized_pretty
-
let pretty_ast ?(prj=Project.current ()) ?fmt () =
- journalized_pretty_ast prj fmt ()
+ Project.on prj pp_file_to fmt
let create_rebuilt_project_from_visitor
?reorder ?last ?(preprocess=false) prj_name visitor =
@@ -1952,7 +1899,7 @@ let create_rebuilt_project_from_visitor
in
let cout = open_out (f :> string) in
let fmt = Format.formatter_of_out_channel cout in
- unjournalized_pretty prj (Some fmt) ();
+ pretty_ast ~prj ~fmt ();
let redo () =
(* Kernel.feedback "redoing initialization on file %s" f;*)
Files.reset ();
diff --git a/src/kernel_services/cmdline_parameters/cmdline.ml b/src/kernel_services/cmdline_parameters/cmdline.ml
index 99d2ff53a95b3d6d32c165ea7918406f6c021160..2c79c7550cc7202859a342c271d64bbcf0e02a90 100644
--- a/src/kernel_services/cmdline_parameters/cmdline.ml
+++ b/src/kernel_services/cmdline_parameters/cmdline.ml
@@ -71,8 +71,6 @@ module Kernel_log =
let dkey = Kernel_log.register_category "cmdline"
let quiet_ref = ref false
-let journal_enable_ref = ref !Fc_config.is_gui
-let journal_isset_ref = ref false
let use_obj_ref = ref true
let use_type_ref = ref true
let deterministic = ref false
@@ -379,15 +377,9 @@ let parse known_options_list then_expected options_list =
let non_initial_options_ref = ref []
let () =
- let set_journal b =
- journal_enable_ref := b;
- journal_isset_ref := true
- in
let first_parsing_stage () =
parse
- [ "-journal-enable", Unit (fun () -> set_journal true);
- "-journal-disable", Unit (fun () -> set_journal false);
- "-no-obj", Unit (fun () -> use_obj_ref := false);
+ [ "-no-obj", Unit (fun () -> use_obj_ref := false);
"-no-type", Unit (fun () -> use_type_ref := false);
"-quiet",
Unit (fun () ->
@@ -418,16 +410,10 @@ let () =
if not !use_obj_ref then use_type_ref := false;
if not !use_type_ref then begin
Type.no_obj ();
- if !journal_enable_ref then begin
- Kernel_log.warning "disabling journal in the 'no obj' mode";
- journal_enable_ref := false
- end
end
let quiet = !quiet_ref
-let journal_enable = !journal_enable_ref
-let journal_isset = !journal_isset_ref
let use_obj = !use_obj_ref
let use_type = !use_type_ref
let deterministic = !deterministic
diff --git a/src/kernel_services/cmdline_parameters/cmdline.mli b/src/kernel_services/cmdline_parameters/cmdline.mli
index b30852478e34e2fdafdaeb776ec461b80a1a478c..be3762b11cb77aa4587f19a17d06241c83298c09 100644
--- a/src/kernel_services/cmdline_parameters/cmdline.mli
+++ b/src/kernel_services/cmdline_parameters/cmdline.mli
@@ -360,13 +360,6 @@ val kernel_debug_atleast_ref: (int -> bool) ref
val kernel_verbose_atleast_ref: (int -> bool) ref
(** @since Boron-20100401 *)
-val journal_enable: bool
-(** @since Beryllium-20090601-beta1 *)
-
-val journal_isset: bool
-(** -journal-enable/disable explicitly set on the command line.
- @since Boron-20100401 *)
-
val use_obj: bool
(** @since Beryllium-20090601-beta1 *)
diff --git a/src/kernel_services/cmdline_parameters/parameter_builder.ml b/src/kernel_services/cmdline_parameters/parameter_builder.ml
index 85a68644f91dc5a599f153ed68fdf8dd959c320d..440d90c04a79cfcf10513351b9fd8c873ba2f127 100644
--- a/src/kernel_services/cmdline_parameters/parameter_builder.ml
+++ b/src/kernel_services/cmdline_parameters/parameter_builder.ml
@@ -219,7 +219,7 @@ struct
if is_dynamic then
let plugin = empty_string in
Dynamic.register
- ~plugin X.option_name Typed_parameter.ty ~journalize:false p
+ ~plugin X.option_name Typed_parameter.ty p
else p
let add_aliases ?visible ?deprecated list =
@@ -328,7 +328,7 @@ struct
if is_dynamic then
let plugin = empty_string in
Dynamic.register
- ~plugin X.option_name Typed_parameter.ty ~journalize:false p
+ ~plugin X.option_name Typed_parameter.ty p
else p
end
@@ -437,7 +437,7 @@ struct
if is_dynamic then
let plugin = empty_string in
Dynamic.register
- ~plugin X.option_name Typed_parameter.ty ~journalize:false p
+ ~plugin X.option_name Typed_parameter.ty p
else
p
@@ -527,7 +527,7 @@ struct
if is_dynamic then
let plugin = empty_string in
Dynamic.register
- ~plugin X.option_name Typed_parameter.ty ~journalize:false p
+ ~plugin X.option_name Typed_parameter.ty p
else
p
diff --git a/src/kernel_services/cmdline_parameters/parameter_customize.ml b/src/kernel_services/cmdline_parameters/parameter_customize.ml
index 26a72c9253e3a7803b76946e8c7ea78407175b02..be8b8888d95dc65708e2314b9a5fbf31953c9f88 100644
--- a/src/kernel_services/cmdline_parameters/parameter_customize.ml
+++ b/src/kernel_services/cmdline_parameters/parameter_customize.ml
@@ -25,9 +25,6 @@ let empty_string = ""
let cmdline_stage_ref = ref Cmdline.Configuring
let set_cmdline_stage s = cmdline_stage_ref := s
-let journalize_ref = ref true
-let do_not_journalize () = journalize_ref := false
-
let negative_option_name_ref = ref None
let set_negative_option_name s = negative_option_name_ref := Some s
@@ -107,7 +104,6 @@ let add_function_name_transformation f =
let reset () =
cmdline_stage_ref := Cmdline.Configuring;
- journalize_ref := true;
negative_option_name_ref := None;
negative_option_help_ref := empty_string;
unset_option_name_ref:= empty_string;
diff --git a/src/kernel_services/cmdline_parameters/parameter_customize.mli b/src/kernel_services/cmdline_parameters/parameter_customize.mli
index 2d2d03cc876ed18a95b05afd0f0e1a012a1163dd..4576d52168e884dcbbf452272a03faa9fbabd770 100644
--- a/src/kernel_services/cmdline_parameters/parameter_customize.mli
+++ b/src/kernel_services/cmdline_parameters/parameter_customize.mli
@@ -33,10 +33,6 @@ val set_cmdline_stage: Cmdline.stage -> unit
recognized. Default is [Cmdline.Configuring].
@since Beryllium-20090601-beta1 *)
-val do_not_journalize: unit -> unit
-(** Prevent journalization of the parameter.
- @since Beryllium-20090601-beta1 *)
-
val do_not_projectify: unit -> unit
(** Prevent projectification of the parameter: its state is shared by all the
existing projects. Also imply {!do_not_save} and {!do_not_reset_on_copy}.
@@ -190,7 +186,6 @@ val find_kf_by_name: (string -> Cil_types.kernel_function) ref
(* ************************************************************************* *)
val cmdline_stage_ref: Cmdline.stage ref
-val journalize_ref: bool ref
val negative_option_name_ref: string option ref
val negative_option_help_ref: string ref
val unset_option_name_ref: string ref
diff --git a/src/kernel_services/cmdline_parameters/parameter_state.ml b/src/kernel_services/cmdline_parameters/parameter_state.ml
index 8eb52c61979378a7ff7e22feb97b37b92219a047..1b7b59d67f06eb6aaac438a4d54c5c1f1d4512c6 100644
--- a/src/kernel_services/cmdline_parameters/parameter_state.ml
+++ b/src/kernel_services/cmdline_parameters/parameter_state.ml
@@ -88,7 +88,6 @@ struct
let reset_on_copy = !Parameter_customize.reset_on_copy_ref
let must_save = !Parameter_customize.must_save_ref
let is_visible = !Parameter_customize.is_visible_ref
- let module_name = !Parameter_customize.module_name_ref
let group = !Parameter_customize.group_ref
let stage = !Parameter_customize.cmdline_stage_ref
@@ -187,29 +186,14 @@ struct
let new_ = !x in
if not (X.equal old new_) then f old new_)
- let gen_journalized name ty set =
- let name =
- if is_dynamic then
- Dynamic.Parameter.get_name X.functor_name name X.option_name
- else
- "Kernel." ^ module_name ^ "." ^ name
- in
- if !Parameter_customize.journalize_ref then
- Journal.register ~is_dyn:is_dynamic name (D.func ty D.unit) set
- else
- set
-
(* like set, but do not clear the dependencies *)
- let unsafe_set =
- let set x =
- Is_set.set true;
- let old = Internal_state.get () in
- if not (X.equal x old) then begin
- Internal_state.set x;
- Set_hook.apply (old, x)
- end
- in
- gen_journalized "unsafe_set" X.ty set
+ let unsafe_set x =
+ Is_set.set true;
+ let old = Internal_state.get () in
+ if not (X.equal x old) then begin
+ Internal_state.set x;
+ Set_hook.apply (old, x)
+ end
let force_set x =
let old = Internal_state.get () in
@@ -232,20 +216,15 @@ struct
Internal_state.set x;
Set_hook.apply (old, x)
- let journalized_force_set = gen_journalized "set" X.ty force_set
-
let set x =
Is_set.set true;
- if not (X.equal x (Internal_state.get ())) then journalized_force_set x
+ if not (X.equal x (Internal_state.get ())) then force_set x
- let unguarded_clear =
- gen_journalized "clear" D.unit
- (fun () ->
- force_set (X.default ());
- Is_set.set false)
+ let unguarded_clear () =
+ force_set (X.default ());
+ Is_set.set false
let clear () =
- (* write this call in the journal if and only if there is something to do *)
if Is_set.get () || not (is_default ()) then unguarded_clear ()
let equal = X.equal
@@ -256,7 +235,6 @@ struct
Dynamic.register
~plugin:""
(Dynamic.Parameter.get_name X.functor_name name X.option_name)
- ~journalize:false
ty
f
else
diff --git a/src/kernel_services/cmdline_parameters/parameter_state.mli b/src/kernel_services/cmdline_parameters/parameter_state.mli
index aabe1efd6e247cf30a70a9d670d57dd2477bb5fa..1329f9bff5f0deab8a912e1f22c3db725177eed0 100644
--- a/src/kernel_services/cmdline_parameters/parameter_state.mli
+++ b/src/kernel_services/cmdline_parameters/parameter_state.mli
@@ -63,7 +63,6 @@ sig
val is_dynamic: bool
val register_dynamic:
string -> 'arg Type.t -> 'ret Type.t -> ('arg -> 'ret) -> 'arg -> 'ret
- val gen_journalized: string -> 'arg Type.t -> ('arg -> unit) -> 'arg -> unit
end
(**/**)
diff --git a/src/kernel_services/cmdline_parameters/typed_parameter.ml b/src/kernel_services/cmdline_parameters/typed_parameter.ml
index b875e86a8eb7dc94a283f42cbcce934da6730568..fd25643d8bb4f583c0840baeb97f8823f31207d3 100644
--- a/src/kernel_services/cmdline_parameters/typed_parameter.ml
+++ b/src/kernel_services/cmdline_parameters/typed_parameter.ml
@@ -67,9 +67,6 @@ include
let hash x = Datatype.String.hash x.name
let copy x = x (* The representation of the parameter is immutable *)
let pretty fmt x = Format.pp_print_string fmt x.name
- let internal_pretty_code = Datatype.undefined
- let varname _ = assert false
- (* unused if internal_pretty_code undefined *)
let mem_project = Datatype.never_any_project
end)
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index aa88f10322091cd8ea4672057d06ec95299aa840..64e5c108ab5c3840e18f335d49f175bf582864d0 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -24,28 +24,15 @@ open Cil_types
open Cil_datatype
open Extlib
-type 'a how_to_journalize =
- | Journalize of string * 'a Type.t
- | Journalization_not_required
- | Journalization_must_not_happen of string
-
-let register how_to_journalize r f =
- match how_to_journalize with
- | Journalize (name, ty) -> r := Journal.register ("!Db." ^ name) ty f
- | Journalization_not_required -> r := f
- | Journalization_must_not_happen name ->
- r := Journal.never_write ("!Db." ^ name) f
+let register r f = r := f
let register_compute name deps r f =
let name = "!Db." ^ name in
- let f = Journal.register name (Datatype.func Datatype.unit Datatype.unit) f in
let compute, self = State_builder.apply_once name deps f in
r := compute;
self
-let register_guarded_compute name is_computed r f =
- let name = "!Db." ^ name in
- let f = Journal.register name (Datatype.func Datatype.unit Datatype.unit) f in
+let register_guarded_compute is_computed r f =
let compute () = if not (is_computed ()) then f () in
r := compute
@@ -202,29 +189,13 @@ module Value = struct
let fun_get_args () = FunArgs.get_option ()
- (* This function is *not* journalized *)
- let fun_set_args =
- let module L = Datatype.List(Cvalue.V) in
- Journal.register "(failwith \"Function cannot be journalized: \
- Db.Value.fun_set_args\" : _ -> unit)"
- (Datatype.func L.ty Datatype.unit)
- (fun l ->
- if
- not
- (Option.equal ListArgs.equal (Some l) (FunArgs.get_option ()))
- then begin
- !initial_state_changed ();
- FunArgs.set l
- end)
-
-
- let fun_use_default_args =
- Journal.register "Db.Value.fun_use_default_args"
- (Datatype.func Datatype.unit Datatype.unit)
- (fun () ->
- if FunArgs.get_option () <> None then
- (!initial_state_changed (); FunArgs.clear ()))
+ let fun_set_args l =
+ if not (Option.equal ListArgs.equal (Some l) (FunArgs.get_option ())) then
+ (!initial_state_changed (); FunArgs.set l)
+ let fun_use_default_args () =
+ if FunArgs.get_option () <> None then
+ (!initial_state_changed (); FunArgs.clear ())
(* Initial memory state of the value analysis *)
module VGlobals =
@@ -235,27 +206,19 @@ module Value = struct
let dependencies = [Ast.self]
end)
- (* This function is *not* journalized *)
- let globals_set_initial_state =
- Journal.register "(failwith \"Function cannot be journalized: \
- Db.Value.globals_set_initial_state\" : _ -> unit)"
- (Datatype.func Cvalue.Model.ty Datatype.unit)
- (fun state ->
- if not (Option.equal Cvalue.Model.equal
- (Some state)
- (VGlobals.get_option ()))
- then begin
- !initial_state_changed ();
- VGlobals.set state
- end)
-
-
- let globals_use_default_initial_state =
- Journal.register
- "Db.Value.globals_use_default_initial_state"
- (Datatype.func Datatype.unit Datatype.unit)
- (fun () -> if VGlobals.get_option () <> None then
- (!initial_state_changed (); VGlobals.clear ()))
+ let globals_set_initial_state state =
+ if not (Option.equal Cvalue.Model.equal
+ (Some state)
+ (VGlobals.get_option ()))
+ then begin
+ !initial_state_changed ();
+ VGlobals.set state
+ end
+
+
+ let globals_use_default_initial_state () =
+ if VGlobals.get_option () <> None then
+ (!initial_state_changed (); VGlobals.clear ())
let initial_state_only_globals = mk_fun "Value.initial_state_only_globals"
@@ -319,10 +282,8 @@ module Value = struct
let dependencies = [ self ]
end)
- let mark_as_computed =
- Journal.register "Db.Value.mark_as_computed"
- (Datatype.func Datatype.unit Datatype.unit)
- Table_By_Callstack.mark_as_computed
+ let mark_as_computed () =
+ Table_By_Callstack.mark_as_computed ()
let is_computed () = Table_By_Callstack.is_computed ()
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 0c37f844ea026f80172eb505e9d567e5c5d63b7d..a3619aec348d0cc83547ec00ec64e13d5d6955a9 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -26,7 +26,6 @@
(**
Modules providing general services:
- {!Dynamic}: API for plug-ins linked dynamically
- - {!Journal}: journalisation
- {!Log}: message outputs and printers
- {!Plugin}: general services for plug-ins
- {!Project} and associated files: {!Kind}, {!Datatype} and {!State_builder}.
@@ -53,22 +52,7 @@ open Cil_datatype
(** {2 Registering} *)
(* ************************************************************************* *)
-(** How to journalize the given function.
- @since Beryllium-20090601-beta1 *)
-type 'a how_to_journalize =
- | Journalize of string * 'a Type.t
- (** Journalize the value with the given name and type. *)
- | Journalization_not_required
- (** Journalization of this value is not required
- (usually because it has no effect on the Frama-C global state). *)
- | Journalization_must_not_happen of string
- (** Journalization of this value should not happen
- (usually because it is a low-level function: this function is always
- called from a journalized function).
- The string is the function name which is used for displaying suitable
- error message. *)
-
-val register: 'a how_to_journalize -> 'a ref -> 'a -> unit
+val register: 'a ref -> 'a -> unit
(** Plugins must register values with this function. *)
val register_compute:
@@ -77,9 +61,10 @@ val register_compute:
(unit -> unit) ref -> (unit -> unit) -> State.t
val register_guarded_compute:
- string ->
(unit -> bool) ->
(unit -> unit) ref -> (unit -> unit) -> unit
+(** @before Frama-C+dev there was a string parameter (first position) that was
+ only used for Journalization, that has been removed. *)
(** Frama-C main interface.
@since Lithium-20081201
@@ -188,8 +173,7 @@ module Value : sig
[fun_use_default_args] is called, when the ast is changed, or
if the options [-libentry] or [-main] are changed. *)
- (** Specify the arguments to use. This function is not journalized, and
- will generate an error when the journal is replayed *)
+ (** Specify the arguments to use. *)
val fun_set_args : t list -> unit
val fun_use_default_args : unit -> unit
@@ -212,8 +196,7 @@ module Value : sig
the option [-libentry]) is used when [globals_use_default_initial_state]
is called, or when the ast changes. *)
- (** Specify the initial state to use. This function is not journalized,
- and will generate an error when the journal is replayed *)
+ (** Specify the initial state to use. *)
val globals_set_initial_state : state -> unit
val globals_use_default_initial_state : unit -> unit
diff --git a/src/kernel_services/plugin_entry_points/dynamic.ml b/src/kernel_services/plugin_entry_points/dynamic.ml
index 8ca60609d5e03713020c43c70223417c5c2b9c47..7e6fa5480075aea0ca8ceca8f94efe99fdfccbca 100644
--- a/src/kernel_services/plugin_entry_points/dynamic.ml
+++ b/src/kernel_services/plugin_entry_points/dynamic.ml
@@ -359,29 +359,9 @@ let load_module m =
let dynamic_values = Tbl.create 97
let comments_fordoc = Hashtbl.create 97
-let register ?(comment="") ~plugin name ty ~journalize f =
+let register ?(comment="") ~plugin name ty f =
if Cmdline.use_type then begin
Klog.debug ~level:5 "registering dynamic function %s" name;
- let f =
- if journalize then
- let comment fmt =
- Format.fprintf fmt
- "@[<hov>Applying@;dynamic@;functions@;%S@;of@;type@;%s@]"
- name
- (Type.name ty)
- in
- let jname =
- Format.fprintf
- Format.str_formatter
- "@[<hv 2>Dynamic.get@;~plugin:%S@;%S@;%t@]"
- plugin name
- (Type.pp_ml_name ty Type.Call);
- Format.flush_str_formatter ()
- in
- Journal.register jname ty ~is_dyn:true ~comment f
- else
- f
- in
let key = plugin ^ "." ^ name in
Tbl.add dynamic_values key ty f;
if comment <> "" then Hashtbl.add comments_fordoc key comment ;
diff --git a/src/kernel_services/plugin_entry_points/dynamic.mli b/src/kernel_services/plugin_entry_points/dynamic.mli
index ae7cb6424ba157e60f331e76f20496aa7a95b018..57422faed10585232c41154fbb7e135fd921bcd0 100644
--- a/src/kernel_services/plugin_entry_points/dynamic.mli
+++ b/src/kernel_services/plugin_entry_points/dynamic.mli
@@ -30,11 +30,13 @@
val register:
?comment:string ->
plugin:string ->
- string -> 'a Type.t -> journalize:bool -> 'a -> 'a
+ string -> 'a Type.t -> 'a -> 'a
(** [register ~plugin name ty v] registers [v] with the name
[name], the type [ty] and the plug-in [plugin].
@raise Type.AlreadyExists if [name] already exists. In other words you
cannot register a value with the same name twice.
+ @before Frama-C+dev there was a labeled argument [journalized], that has
+ been removed when Journalization has been removed.
@plugin development guide *)
(* ************************************************************************* *)
@@ -155,7 +157,8 @@ end
*)
val load_packages: string list -> unit
-(** Load the module specification. See -load-module option. *)
+(** Load the module specification. See -load-module option.
+ @modify Magnesium-20151001 new API. *)
val load_module: string -> unit
(** Sets the load path for modules in FRAMAC_PLUGIN, prepending it with [path].
@@ -173,7 +176,8 @@ val is_loaded: string -> bool
val load_plugin_path: unit -> unit
(** Load all plugins in the path set with [set_module_load_path].
Must be invoked only once from boot during extending stage.
- @since Magnesium-20151001 new API. *)
+ @since Magnesium-20151001 new API.
+ @modify Phosphorus-20170501-beta1 changed signature. *)
(**/**)
(*
diff --git a/src/kernel_services/plugin_entry_points/emitter.ml b/src/kernel_services/plugin_entry_points/emitter.ml
index 43d4b82ef8d8a26eec2b40b0bc2bb48636354b04..0349a71692e9d42ea2aefbe5fbb1453c10155f4a 100644
--- a/src/kernel_services/plugin_entry_points/emitter.ml
+++ b/src/kernel_services/plugin_entry_points/emitter.ml
@@ -103,9 +103,6 @@ module D =
let hash x = Datatype.String.hash x.name
let copy x = x (* strings are immutable here *)
let pretty fmt x = Format.pp_print_string fmt x.name
- let internal_pretty_code = Datatype.undefined
- let varname _ = assert false (* unused while [internal_pretty_code]
- unimplemented *)
let mem_project = Datatype.never_any_project
end)
@@ -149,9 +146,6 @@ module Usable_emitter = struct
Format.fprintf fmt "%s (v%d)" name x.version
else
Format.pp_print_string fmt name
- let internal_pretty_code = Datatype.undefined
- let varname _ = assert false (* unused while [internal_pretty_code]
- unimplemented *)
let mem_project = Datatype.never_any_project
end)
diff --git a/src/kernel_services/plugin_entry_points/journal.ml b/src/kernel_services/plugin_entry_points/journal.ml
deleted file mode 100644
index 4c81ac38b9cd345d4a0ffa98eaff99af3c4dc2bc..0000000000000000000000000000000000000000
--- a/src/kernel_services/plugin_entry_points/journal.ml
+++ /dev/null
@@ -1,499 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2022 *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-(* ****************************************************************************)
-(* ****************************************************************************)
-(* ****************************************************************************)
-
-(* Disclaimer
- ----------
- This module uses very unsafe caml features (module Obj).
- Modify it at your own risk.
- Sometimes the caml type system does not help you here.
- Introducing a bug here may introduce some "segmentation faults" in Frama-C *)
-
-(* ****************************************************************************)
-(* ****************************************************************************)
-(* ****************************************************************************)
-
-open Cmdline.Kernel_log
-
-(** Journalization of functions *)
-
-(* ****************************************************************************)
-(** {2 Journal management} *)
-(* ****************************************************************************)
-
-(* [started] prevents journalization of function call
- inside another one. It is [true] iff a journalized function is being
- applied. *)
-let started = ref false
-
-module Sentences = struct
-
- type t =
- { sentence: Format.formatter -> unit;
- raise_exn: bool }
-
- let sentences : t Queue.t = Queue.create ()
-
- let add print exn =
- Queue.add { sentence = print; raise_exn = exn } sentences
-
- let write fmt =
- let finally_raised = ref false in
- (* printing the sentences *)
- Queue.iter
- (fun s -> s.sentence fmt; finally_raised := s.raise_exn)
- sentences;
- (* if any, re-raised the exception raised by the last sentence *)
- Format.fprintf fmt "@[%s@]"
- (if !finally_raised then "raise (Exception (Printexc.to_string exn))"
- else "()");
- (* closing the box opened when catching exception *)
- Queue.iter
- (fun s -> if s.raise_exn then Format.fprintf fmt "@]@]@]@;end")
- sentences
-
- let journal_copy = ref (Queue.create ())
- let save () = journal_copy := Queue.copy sentences
- let restore () =
- Queue.clear sentences;
- Queue.transfer !journal_copy sentences
-
-end
-
-module Abstract_modules = struct
- let tbl: (string, string) Hashtbl.t = Hashtbl.create 7
- let () = Type.add_abstract_types := Hashtbl.replace tbl
- let write fmt =
- Hashtbl.iter
- (fun k v ->
- Format.fprintf fmt
- "@[<hv 2>let module %s=@;@[<hv 0>Type.Abstract\
- (struct let name = %S end) in@]@]@;"
- k v)
- tbl
- let tbl_copy = ref (Hashtbl.create 7)
- let save () = tbl_copy := Hashtbl.copy tbl
- let restore () =
- Hashtbl.clear tbl;
- Hashtbl.iter (fun k v -> Hashtbl.add tbl k v) !tbl_copy
-end
-
-let save () =
- Sentences.save ();
- Abstract_modules.save ()
-
-let restore () =
- Sentences.restore ();
- Abstract_modules.restore ()
-
-let now () = Unix.localtime (Unix.time ())
-
-let default_filename = "frama_c_journal.ml"
-let filename = ref default_filename
-let get_session_file = ref (fun _ -> assert false)
-let get_name () =
- let f = !filename in
- if f == default_filename
- then !get_session_file f
- else Datatype.Filepath.of_string f
-
-let set_name s = filename := s
-
-let print_header fmt =
- let time = now () in
- Format.pp_open_hvbox fmt 0; (* the outermost box *)
- Format.fprintf fmt
- "@[(* Frama-C journal generated at %02d:%02d the %02d/%02d/%d *)@]@;@;"
- time.Unix.tm_hour
- time.Unix.tm_min
- time.Unix.tm_mday
- (time.Unix.tm_mon+1)
- (time.Unix.tm_year + 1900);
- Format.fprintf fmt "@[exception Unreachable@]@;";
- Format.fprintf fmt "@[exception Exception of string@]@;@;";
- Format.fprintf fmt "@[[@@@@@@ warning \"-26\"]@]@;@;";
- Format.fprintf fmt (* open two boxes for start *)
- "(* Run the user commands *)@;@[<hv 2>let run () =@;@[<hv 0>"
-
-let print_trailer fmt =
- let name = Format.asprintf "%a" Datatype.Filepath.pretty (get_name ()) in
- Format.fprintf fmt "@[(* Main *)@]@\n";
- Format.fprintf fmt "@[<hv 2>let main () =@;";
- Format.fprintf fmt
- "@[<hv 0>@[<hv 2>Journal.keep_file@; (Datatype.Filepath.of_string@; (\"%s\"));@]@;"
- name;
- Format.fprintf fmt "try run ()@;";
- Format.fprintf fmt "@[<v>with@;@[<hv 2>| Unreachable ->@ ";
- Format.fprintf fmt
- "@[<hv 2>Kernel.fatal@;\"Journal reaches an assumed dead code\"@;@]@]@;";
- Format.fprintf fmt "@[<hv 2>| Exception s ->@ ";
- Format.fprintf fmt
- "@[<hv 2>Kernel.log@;\"Journal re-raised the exception %%S\"@;s@]@]@;";
- Format.fprintf fmt "@[<hv 2>| exn ->@ ";
- Format.fprintf fmt
- "@[<hv 2>Kernel.fatal@;\"Journal raised an unexpected exception: %%s\"@;";
- Format.fprintf fmt "(Printexc.to_string exn)@]@]@]@]@]@\n@\n";
- Format.fprintf fmt "@[(* Registering *)@]@\n";
- Format.fprintf fmt
- "@[<hv 2>let main : unit -> unit =@;@[<hv 2>Dynamic.register@;~plugin:%S@;\"main\"@;"
- (String.capitalize_ascii (Filename.basename name));
- Format.fprintf fmt
- "@[<hv 2>(Datatype.func@;Datatype.unit@;Datatype.unit)@]@;";
- Format.fprintf fmt "~journalize:false@;main@]@]@\n@\n";
- Format.fprintf fmt "@[(* Hooking *)@]@\n";
- Format.fprintf fmt "@[<hv 2>let () =@;";
- Format.fprintf fmt
- "@[<hv 2>Cmdline.run_after_loading_stage@;main;@]@;";
- Format.fprintf fmt "@[<hv 2>Cmdline.is_going_to_load@;()@]@]@.";
- (* close the outermost box *)
- Format.pp_close_box fmt ()
-
-let preserved_files : Datatype.Filepath.t list ref = ref []
-let keep_file s = preserved_files := s :: !preserved_files
-
-let get_filename =
- let cpt = ref 0 in
- let rec get_filename first =
- let name_fp = get_name () in
- let name = (name_fp:>string) in
- if (not first && Sys.file_exists name) || List.mem name_fp !preserved_files
- then begin
- incr cpt;
- let suf = "_" ^ string_of_int !cpt in
- (try
- let n =
- Str.search_backward
- (Str.regexp "_[0-9]+")
- name
- (String.length name - 1)
- in
- filename := Str.string_before name n ^ suf
- with Not_found ->
- filename := name ^ suf);
- get_filename false
- end else
- name_fp
- in
- fun () -> get_filename true
-
-let write () =
- let write fmt =
- print_header fmt;
- Abstract_modules.write fmt;
- Sentences.write fmt;
- Format.fprintf fmt "@]@]@;@;";
- print_trailer fmt;
- Format.pp_print_flush fmt ()
- in
- let error msg s = error "cannot %s journal (%s)." msg s in
- let filename = get_filename () in
- feedback "writing journal in file `%a'."
- Datatype.Filepath.pretty filename;
- try
- let cout = open_out (filename:>string) in
- let fmt = Format.formatter_of_out_channel cout in
- Format.pp_set_margin fmt 78 (* line length *);
- (try write fmt with Sys_error s -> error "write into" s);
- try close_out cout with Sys_error s -> error "close" s
- with Sys_error s ->
- error "create" s
-
-let () =
- (* write the journal iff it is enable and
- - either an error occurs;
- - or the user explicitly wanted it. *)
- if Cmdline.journal_enable then begin
- Cmdline.at_error_exit (fun _ -> write ());
- if Cmdline.journal_isset then Cmdline.at_normal_exit write
- end
-
-(* ****************************************************************************)
-(** {2 Journalization} *)
-(* ****************************************************************************)
-
-module Binding: sig
- val add: 'a Type.t -> 'a -> string -> unit
- (** [add ty v var] binds the value [v] to the variable name [var]. Thus,
- [pp ty v] prints [var] and not use the standard pretty printer. Very
- useful to pretty print values with no associated pretty printer. *)
-
- exception Name_already_exists of string
- val add_once: 'a Type.t -> 'a -> string -> unit
- (** Same as function [add] above but raise the exception [Already_exists]
- if the binding previously exists *)
-
- val find: 'a Type.t -> 'a -> string
- val iter: ('a Type.t -> 'a -> string -> unit) -> unit
-end = struct
-
- let bindings : string Type.Obj_tbl.t = Type.Obj_tbl.create ()
-
- let add ty v var =
- Type.Obj_tbl.add bindings ty v var (* eta-expansion required *)
-
- (* add bindings for [Format.std_formatter] and [Format.err_formatter] *)
- let () =
- add Datatype.formatter Format.std_formatter "Format.std_formatter";
- add Datatype.formatter Format.err_formatter "Format.err_formatter"
-
- exception Name_already_exists of string
- let check_name s =
- let error () =
- Format.eprintf "[Type] A value of name %s already exists@." s;
- raise (Name_already_exists s)
- in
- Type.Obj_tbl.iter bindings (fun _ _ s' -> if s = s' then error ())
-
- let add_once ty x s =
- check_name s;
- add ty x s
-
- let find ty v = Type.Obj_tbl.find bindings ty v (* eta-expansion required *)
- let iter f = Type.Obj_tbl.iter bindings f (* eta-expansion required *)
-
- (* predefined bindings *)
- let () =
- add Datatype.formatter Format.std_formatter "Format.std_formatter";
- add Datatype.formatter Format.err_formatter "Format.err_formatter"
-
-end
-
-(* JS 2012/02/07: useful only for BM introspection testing ;-) *)
-module Reverse_binding = struct
- module Tbl = Type.String_tbl(struct type 'a t = 'a end)
- exception Unbound_value = Tbl.Unbound_value
- exception Incompatible_type = Tbl.Incompatible_type
-
- let tbl = Tbl.create 97
- let fill () = Binding.iter (fun ty v name -> Tbl.add tbl name ty v)
- let find name ty = Tbl.find tbl name ty
- let iter f = Tbl.iter f tbl
-
- let pretty fmt () =
- iter
- (fun name ty v ->
- Format.fprintf fmt "%s --> %a@." name (Datatype.pretty ty) v)
-
-end
-
-exception Not_writable of string
-let never_write name f =
- if Cmdline.journal_enable && Cmdline.use_type then
- if Obj.tag (Obj.repr f) = Obj.closure_tag then
- Obj.magic
- (fun y ->
- if !started then Obj.magic f y
- else
- let msg =
- Format.asprintf
- "a call to the function %s has to be written in the journal, \
- but this function was never journalized."
- name
- in
- raise (Not_writable msg))
- else
- invalid_arg ("[Journal.never_write] " ^ name ^ " is not a closure")
- else
- f
-
-let pp (type t) (ty: t Type.t) fmt (x:t) =
- assert Cmdline.use_type;
- try Format.fprintf fmt "%s" (Binding.find ty x);
- with Not_found ->
- let pp_error msg =
- Format.fprintf fmt "@[<hov 2>(failwith @[<hov 2>\"%s:@ running the journal will fail.\"@])@;@]" msg
- in
- let pp = Datatype.internal_pretty_code ty in
- if pp == Datatype.undefined then
- pp_error
- (Format.asprintf
- "no printer registered for value of type %s"
- (Type.name ty))
- else if pp == Datatype.pp_fail then
- pp_error
- (Format.asprintf
- "no code for pretty printer of type %s"
- (Type.name ty))
- else
- pp Type.Call fmt x
-
-let gen_binding =
- let ids = Hashtbl.create 7 in
- let rec gen s =
- try
- let n = succ (Hashtbl.find ids s) in
- Hashtbl.replace ids s n;
- gen (s ^ "_" ^ string_of_int n)
- with Not_found ->
- Hashtbl.add ids s 1;
- s
- in
- gen
-
-let extend_continuation f_acc pp_arg opt_label opt_arg arg fmt =
- f_acc fmt;
- match opt_label, opt_arg with
- | None, None (* no label *) -> Format.fprintf fmt "@;%a" pp_arg arg;
- | None, Some _ -> assert false
- | Some _, Some f when f () == arg ->
- (* [arg] is the default value of the optional label *)
- ()
- | Some l, _ (* other label *) -> Format.fprintf fmt "@;~%s:%a" l pp_arg arg
-
-(* print any comment *)
-let print_comment fmt pp = match pp with
- | None -> ()
- | Some pp -> Format.fprintf fmt "(* %t *)@;" pp
-
-let print_sentence f_acc is_dyn comment ?value ty fmt =
- assert Cmdline.use_type;
- print_comment fmt comment;
- (* open a new box for the sentence *)
- Format.fprintf fmt "@[<hv 2>";
- (* add a let binding whenever the return type is not unit *)
- let is_unit = Type.equal ty Datatype.unit in
- if not is_unit then
- Format.fprintf fmt "let %t=@;"
- (fun fmt ->
- let binding =
- let varname = Datatype.varname ty in
- match varname == Datatype.undefined, value with
- | true, _ | _, None ->
- "__" (* no binding nor value: ignore the result *)
- | false, Some value ->
- (* bind to a fresh variable name *)
- let b = gen_binding (varname value) in
- Binding.add ty value b;
- b
- in
- Format.fprintf fmt "%s" binding;
- (* add the return type for dynamic application *)
- if is_dyn then Format.fprintf fmt "@;: %s " (Type.name ty)
- else Format.fprintf fmt " ");
- (* pretty print the sentence itself in a box *)
- Format.fprintf fmt "@[<hv 2>%t@]" f_acc;
- (* close the sentence *)
- if is_unit then Format.fprintf fmt ";@]@;"
- else Format.fprintf fmt "@;<1 -2>in@]@;"
-
-let add_sentence f_acc is_dyn comment ?value ty =
- Sentences.add (print_sentence f_acc is_dyn comment ?value ty) false
-
-let catch_exn f_acc is_dyn comment ret_ty exn =
- let s_exn = Printexc.to_string exn in
- (* [s_exn] is not necessarily a valid OCaml exception.
- So don't use it in OCaml code. *)
- let comment fmt =
- Format.fprintf fmt "@[<hv 2>exception %s@;raised on: @]%t" s_exn
- (fun fmt -> Option.iter (fun f -> f fmt) comment)
- in
- let print fmt =
- (* open a new box for the sentence *)
- Format.fprintf fmt
- "@[<hv 2>begin try@;@[<hv>%t@[<hv 2>raise Unreachable@]@]@]@;"
- (print_sentence f_acc is_dyn (Some comment) ret_ty);
- (* two opened boxes closed at end *)
- Format.fprintf fmt
- "@[<v>with@;@[<hv 2>| Unreachable as exn -> raise exn@]@;";
- Format.fprintf fmt
- "@[<hv 2>| exn (* %s *) ->@;@[<hv>@[(* continuing: *)@]@;" s_exn
- in
- Sentences.add print true
-
-let rec journalize_function: 't.
- (Format.formatter -> unit) -> 't Type.t -> bool ->
- (Format.formatter -> unit) option -> 't -> 't =
- fun (type t) (type a) (type b) f_acc (ty: t Type.t) is_dyn comment (x:t)
- ->
- assert Cmdline.use_type;
- if Type.Function.is_instance_of ty then begin
- (* [ty] is a function type value:
- there exists [a] and [b] such than [t = a -> b] *)
- let ty: (a -> b) Type.t = Obj.magic (ty: t Type.t) in
- let f: a -> b = Obj.magic (x: t) in
- let (a: a Type.t), (b: b Type.t), opt_label =
- Type.Function.get_instance ty
- in
- let opt_arg = Type.Function.get_optional_argument ty in
- let f (y: a) : b =
- if !started then
- (* prevent journalisation if you're journalizing another function *)
- f y
- else begin
- try
- (* [started] prevents journalization of function call
- inside another one *)
- started := true;
- (* apply the closure [x] to its argument [y] *)
- let xy = f y in
- started := false;
- (* extend the continuation and continue *)
- let f_acc = extend_continuation f_acc (pp a) opt_label opt_arg y in
- journalize_function f_acc b is_dyn comment xy
- with
- | Not_writable name ->
- started := false;
- fatal
- "a call to the function %S cannot be written in the journal"
- name
- | exn as e ->
- let f_acc = extend_continuation f_acc (pp a) opt_label opt_arg y in
- catch_exn f_acc is_dyn comment b exn;
- started := false;
- raise e
- end in
- (* cast back the closure of type [a -> b] into [t] *)
- (Obj.magic (f: a -> b): t)
- end else begin
- if not !started then add_sentence f_acc is_dyn comment ~value:x ty;
- x
- end
-
-let register s ty ?comment ?(is_dyn=false) x =
- if Cmdline.journal_enable then begin
- assert Cmdline.use_type;
- if s = "" then
- abort "[Journal.register] the given name should not be \"\"";
- Binding.add_once ty x s;
- if Type.Function.is_instance_of ty then begin
- let f_acc fmt = pp ty fmt x in
- journalize_function f_acc ty is_dyn comment x
- end else
- x
- end else
- x
-
-let prevent f x =
- let old = !started in
- started := true;
- let res = try f x with exn -> started := old; raise exn in
- started := old;
- res
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/plugin_entry_points/journal.mli b/src/kernel_services/plugin_entry_points/journal.mli
deleted file mode 100644
index f9be3ee7a31b714322c560bbe4e62871328f29e5..0000000000000000000000000000000000000000
--- a/src/kernel_services/plugin_entry_points/journal.mli
+++ /dev/null
@@ -1,120 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2022 *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-(** Journalization of functions.
- @plugin development guide *)
-
-(* ****************************************************************************)
-(** {2 Journalization} *)
-(* ****************************************************************************)
-
-val register:
- string ->
- 'a Type.t ->
- ?comment:(Format.formatter -> unit) ->
- ?is_dyn:bool ->
- 'a ->
- 'a
-(** [register name ty ~comment ~is_dyn v] journalizes the value [v]
- of type [ty] with the name [name]. [name] must exactly match the caml
- long name of the value (i.e. "List.iter" and not "iter" even though the
- module List is already opened). Journalisation of anonymous value is
- not possible.
-
- If the [comment] argument is set, the given pretty printer will be
- applied in an OCaml comment when the function is journalized.
-
- Set [is_dyn] to [true] to journalize a dynamic function. *)
-
-val never_write: string -> 'a -> 'a
-(** [never_write name f] returns a closure [g] observationally equal to [f]
- except that trying to write a call to [g] in the journal is an error. If
- [f] is not a closure, then [never_write name f] raises
- [Invalid_argument]. *)
-
-val prevent: ('a -> 'b) -> 'a -> 'b
-(** [prevent f x] applies [x] to [f] without printing anything in the
- journal, even if [f] is journalized. *)
-
-module Binding: sig
- val add: 'a Type.t -> 'a -> string -> unit
- (** [add ty v var] binds the value [v] to the variable name [var]. Thus,
- [pp ty v] prints [var] and not use the standard pretty printer. Very
- useful to pretty print values with no associated pretty printer. *)
-
- exception Name_already_exists of string
- val add_once: 'a Type.t -> 'a -> string -> unit
- (** Same as function [add] above but raise the exception [Already_exists]
- if the binding previously exists *)
-end
-
-(* JS 2012/02/07: useful only for BM introspection testing ;-) *)
-module Reverse_binding: sig
-
- (* Raised by [find] *)
- exception Unbound_value of string
- exception Incompatible_type of string
-
- val fill: unit -> unit
- val find: string -> 'a Type.t -> 'a
- val iter: (string -> 'a Type.t -> 'a -> unit) -> unit
- val pretty: Format.formatter -> unit -> unit
-end
-
-(* ****************************************************************************)
-(** {2 Journal management} *)
-(* ****************************************************************************)
-
-val get_name: unit -> Datatype.Filepath.t
-(** @return the filename which the journal will be written into. *)
-
-val set_name: string -> unit
-(** [set_name name] changes the filename into the journal is generated. *)
-
-val write: unit -> unit
-(** [write ()] writes the content of the journal into the file set by
- [set_name] (or in "frama_c_journal.ml" by default);
- without clearing the journal. *)
-
-val save: unit -> unit
-(** Save the current state of the journal for future restoration.
- @since Beryllium-20090901 *)
-
-val restore: unit -> unit
-(** Restore a previously saved journal.
- @since Beryllium-20090901 *)
-
-(* ****************************************************************************)
-(** {2 Internal use only} *)
-(* ****************************************************************************)
-
-val keep_file: Datatype.Filepath.t -> unit
-(** This function is not to be used explicitly. Only offers functions
- retrieving when running a journal file. *)
-
-val get_session_file: (string -> Datatype.Filepath.t) ref
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 3ef630f87377615d376089c541fcb003c681f604..9c2da0653eaf6df1e10fd9afc4c02432d4322fe4 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -320,7 +320,6 @@ module Kernel_function_set(X: Input_with_arg) =
let () = Parameter_customize.set_group help
let () = Parameter_customize.set_cmdline_stage Cmdline.Exiting
-let () = Parameter_customize.do_not_journalize ()
let () = Parameter_customize.set_negative_option_name ""
module GeneralHelp =
False
@@ -335,7 +334,6 @@ let () = GeneralHelp.add_aliases [ "-h"; "-help"]
let () = Parameter_customize.set_group help
let () = Parameter_customize.set_cmdline_stage Cmdline.Exiting
-let () = Parameter_customize.do_not_journalize ()
let () = Parameter_customize.set_negative_option_name ""
module ListPlugins =
False
@@ -445,7 +443,6 @@ module PrintConfigJson =
let () = Parameter_customize.set_group help
let () = Parameter_customize.set_cmdline_stage Cmdline.Exiting
-let () = Parameter_customize.do_not_journalize ()
let () = Parameter_customize.set_negative_option_name ""
module AutocompleteHelp =
P.String_set
@@ -474,7 +471,6 @@ let _ =
let () = Parameter_customize.set_group help
let () = Parameter_customize.set_cmdline_stage Cmdline.Extending
-let () = Parameter_customize.do_not_journalize ()
let () = Parameter_customize.set_negative_option_name ""
module Explain =
False
@@ -498,7 +494,6 @@ let () =
let () = Parameter_customize.set_group messages
let () = Parameter_customize.do_not_projectify ()
-let () = Parameter_customize.do_not_journalize ()
let () = Parameter_customize.set_cmdline_stage Cmdline.Early
let () = Parameter_customize.is_reconfigurable ()
module GeneralVerbose =
@@ -520,7 +515,6 @@ let () =
let () = Parameter_customize.set_group messages
let () = Parameter_customize.do_not_projectify ()
-let () = Parameter_customize.do_not_journalize ()
let () = Parameter_customize.set_cmdline_stage Cmdline.Early
let () = Parameter_customize.is_reconfigurable ()
module GeneralDebug =
@@ -548,7 +542,6 @@ let () = Parameter_customize.set_negative_option_name ""
let () = Parameter_customize.set_cmdline_stage Cmdline.Early
let () = Parameter_customize.is_reconfigurable ()
let () = Parameter_customize.do_not_projectify ()
-let () = Parameter_customize.do_not_journalize ()
module Quiet =
Bool
(struct
@@ -563,7 +556,6 @@ let () =
let () = Parameter_customize.set_group messages
let () = Parameter_customize.set_cmdline_stage Cmdline.Extended
-let () = Parameter_customize.do_not_journalize ()
let () = Parameter_customize.do_not_projectify ()
module Unicode = struct
include True
@@ -573,9 +565,7 @@ module Unicode = struct
let help = "use utf8 in messages"
end)
(* This function behaves nicely with the Gui, that detects if command-line
- arguments have been set by the user at some point. One possible improvement
- would be to bypass journalization entirely, but this requires an API
- change in Plugin *)
+ arguments have been set by the user at some point. *)
let without_unicode f arg =
let old, default = get (), not (is_set ()) in
off ();
@@ -906,45 +896,6 @@ let bootstrap_loader () =
let () = Cmdline.load_all_plugins := bootstrap_loader
-module Journal = struct
- let () = Parameter_customize.set_negative_option_name "-journal-disable"
- let () = Parameter_customize.set_cmdline_stage Cmdline.Early
- let () = Parameter_customize.set_group saveload
- let () = Parameter_customize.do_not_projectify ()
- module Enable = struct
- include Bool
- (struct
- let module_name = "Journal.Enable"
- let default = Cmdline.journal_enable
- let option_name = "-journal-enable"
- let help = "dump a journal while Frama-C exit"
- end)
- let is_set () = Cmdline.journal_isset
- end
- let () = Parameter_customize.set_group saveload
- let () = Parameter_customize.do_not_projectify ()
- module Name =
- String
- (struct
- let module_name = "Journal.Name"
- let option_name = "-journal-name"
- let default =
- let dir =
- (* duplicate code from Plugin.Session *)
- if Session.is_set ()
- then
- (Session.get () :> string)
- else
- try Sys.getenv "FRAMAC_SESSION"
- with Not_found -> "./.frama-c"
- in
- dir ^ "/frama_c_journal.ml"
- let arg_name = "s"
- let help = "set the filename of the journal"
- end)
- let () = Name.add_set_hook (fun _ s -> Journal.set_name s);
-end
-
let () = Parameter_customize.set_cmdline_stage Cmdline.Extending
let () = Parameter_customize.set_group saveload
let () = Parameter_customize.do_not_projectify ()
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index b58ecaa79ad262e327b13fb21811893d43e33080..ab6ff6dd95dbce1b514fdc89d174d1864e74da84 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -370,17 +370,6 @@ module LoadModule: Parameter_sig.String_list
module AutoLoadPlugins: Parameter_sig.Bool
(** Behavior of option "-autoload-plugins" *)
-(** Kernel for journalization. *)
-module Journal: sig
-
- module Enable: Parameter_sig.Bool
- (** Behavior of option "-journal-enable" *)
-
- module Name: Parameter_sig.String
- (** Behavior of option "-journal-name" *)
-
-end
-
module Session_dir: Parameter_sig.Filepath
(** Directory in which session files are searched.
@since Neon-20140301
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index 493cea1aaf76821266d0ebe68c52c132dbc5a7a5..c7ff75869fc85686e3b5c56cd5a6a3c2a6ad9306 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -453,11 +453,6 @@ struct
]
let visible_ref = !session_visible_ref
end)
- let () =
- if is_kernel ()
- then
- Journal.get_session_file :=
- (fun s -> Session.get_file ~mode:`Create_path s)
module Config =
Make_specific_dir
@@ -513,7 +508,6 @@ struct
let output_mode modname optname =
Parameter_customize.set_group messages;
Parameter_customize.do_not_projectify ();
- Parameter_customize.do_not_journalize ();
Parameter_customize.is_reconfigurable ();
if is_kernel () then begin
Parameter_customize.set_cmdline_stage Cmdline.Early;
diff --git a/src/libraries/datatype/datatype.ml b/src/libraries/datatype/datatype.ml
index 0db6b38c6c5659189e009ccf723ca23329f88d65..73a64e236999349175c7d5a58230654659ced653 100644
--- a/src/libraries/datatype/datatype.ml
+++ b/src/libraries/datatype/datatype.ml
@@ -29,10 +29,7 @@ type 'a t =
compare: 'a -> 'a -> int;
hash: 'a -> int;
copy: 'a -> 'a;
- internal_pretty_code: Type.precedence -> Format.formatter -> 'a -> unit;
- pretty_code: Format.formatter -> 'a -> unit;
pretty: Format.formatter -> 'a -> unit;
- varname: 'a -> string;
mem_project: (Project_skeleton.t -> bool) -> 'a -> bool }
type 'a info = 'a t
@@ -51,10 +48,7 @@ module type S_no_copy = sig
val equal: t -> t -> bool
val compare: t -> t -> int
val hash: t -> int
- val pretty_code: Format.formatter -> t -> unit
- val internal_pretty_code: Type.precedence -> Format.formatter -> t -> unit
val pretty: Format.formatter -> t -> unit
- val varname: t -> string
val mem_project: (Project_skeleton.t -> bool) -> t -> bool
end
@@ -82,11 +76,7 @@ let equal ty = (internal_info "equal" ty).equal
let compare ty = (internal_info "compare" ty).compare
let hash ty = (internal_info "hash" ty).hash
let copy ty = (internal_info "copy" ty).copy
-let internal_pretty_code ty =
- (internal_info "internal_pretty_code" ty).internal_pretty_code
-let pretty_code ty = (internal_info "pretty_code" ty).pretty_code
let pretty ty = (internal_info "pretty" ty).pretty
-let varname ty = (internal_info "varname" ty).varname
let mem_project ty = (internal_info "mem_project" ty).mem_project
let info ty = internal_info "info" ty
@@ -99,8 +89,6 @@ let undefined _ = assert false
let identity x = x
let never_any_project _ _ = false
let from_compare _ _ = assert false
-let from_pretty_code _ _ = assert false
-let pp_fail _ _ _ = assert false
module type Undefined = sig
val structural_descr: Structural_descr.t
@@ -109,9 +97,7 @@ module type Undefined = sig
val hash: 'a -> int
val rehash: 'a -> 'a
val copy: 'a -> 'a
- val internal_pretty_code: Type.precedence -> Format.formatter -> 'a -> unit
val pretty: Format.formatter -> 'a -> unit
- val varname: 'a -> string
val mem_project: (Project_skeleton.t -> bool) -> 'a -> bool
end
@@ -120,9 +106,7 @@ module Partial_undefined = struct
let compare = undefined
let hash = undefined
let copy = undefined
- let internal_pretty_code = undefined
let pretty = undefined
- let varname = undefined
let mem_project = undefined
end
@@ -143,11 +127,6 @@ end
(** {2 Generic builders} *)
(* ********************************************************************** *)
-let valid_varname s =
- let r = Str.regexp "[^A-Za-z0-9_]+" in
- let s = Str.global_replace r "__" s in
- String.uncapitalize_ascii s
-
let check f fname tname fstr =
assert
(if f == undefined && Type.may_use_obj () then begin
@@ -168,9 +147,7 @@ module Build
val hash: t -> int
val rehash: t -> t
val copy: t -> t
- val internal_pretty_code: Type.precedence -> Format.formatter -> t -> unit
val pretty: Format.formatter -> t -> unit
- val varname: t -> string
val mem_project: (Project_skeleton.t -> bool) -> t -> bool
end) =
struct
@@ -186,29 +163,7 @@ struct
let hash = T.hash
let rehash = T.rehash
let copy = T.copy
- let internal_pretty_code = T.internal_pretty_code
-
- let pretty_code =
- if T.internal_pretty_code == undefined then undefined
- else if T.internal_pretty_code == pp_fail then pp_fail Type.NoPar
- else fun fmt x ->
- (* Format.printf "pretty code %s@." name;*)
- let buf = Buffer.create 17 in
- let buffmt = Format.formatter_of_buffer buf in
- Format.fprintf buffmt "%a@?" (T.internal_pretty_code Type.NoPar) x;
- let f =
- Scanf.format_from_string (String.escaped (Buffer.contents buf)) ""
- in
- Format.fprintf fmt f
-
- let pretty =
- if T.pretty == from_pretty_code then pretty_code
- else T.pretty
-
- let varname =
- if T.varname == undefined then undefined
- else fun x -> valid_varname (T.varname x)
-
+ let pretty = T.pretty
let mem_project = T.mem_project
let info =
@@ -216,10 +171,7 @@ struct
compare = compare;
hash = hash;
copy = copy;
- internal_pretty_code = internal_pretty_code;
- pretty_code = pretty_code;
pretty = pretty;
- varname = varname;
mem_project = mem_project }
let () = Infos.add info_tbl T.ty info
@@ -261,9 +213,7 @@ module type Make_input = sig
val compare: t -> t -> int
val hash: t -> int
val copy: t -> t
- val internal_pretty_code: Type.precedence -> Format.formatter -> t -> unit
val pretty: Format.formatter -> t -> unit
- val varname: t -> string
val mem_project: (Project_skeleton.t -> bool) -> t -> bool
end
@@ -353,14 +303,9 @@ module type Polymorphic2_input = sig
('a -> 'a -> int) -> ('b -> 'b -> int) -> ('a, 'b) t -> ('a, 'b) t -> int
val mk_hash: ('a -> int) -> ('b -> int) -> ('a, 'b) t -> int
val map: ('a -> 'a) -> ('b -> 'b) -> ('a, 'b) t -> ('a, 'b) t
- val mk_internal_pretty_code:
- (Type.precedence -> Format.formatter -> 'a -> unit) ->
- (Type.precedence -> Format.formatter -> 'b -> unit) ->
- Type.precedence -> Format.formatter -> ('a, 'b) t -> unit
val mk_pretty:
(Format.formatter -> 'a -> unit) -> (Format.formatter -> 'b -> unit) ->
Format.formatter -> ('a, 'b) t -> unit
- val mk_varname: ('a -> string) -> ('b -> string) -> ('a, 'b) t -> string
val mk_mem_project:
((Project_skeleton.t -> bool) -> 'a -> bool) ->
((Project_skeleton.t -> bool) -> 'b -> bool) ->
@@ -423,14 +368,7 @@ module Polymorphic2(P: Polymorphic2_input) = struct
else*) P.map f1 f2
in
build mk T1.copy T2.copy
- let internal_pretty_code =
- let mk f1 f2 =
- if f1 == pp_fail || f2 == pp_fail then pp_fail
- else fun p fmt x -> P.mk_internal_pretty_code f1 f2 p fmt x
- in
- build mk T1.internal_pretty_code T2.internal_pretty_code
let pretty = build P.mk_pretty T1.pretty T2.pretty
- let varname = build P.mk_varname T1.varname T2.varname
let mem_project =
let mk f1 f2 =
if P.mk_mem_project == undefined then undefined
@@ -475,19 +413,11 @@ module Polymorphic3
('a -> int) -> ('b -> int) -> ('c -> int) -> ('a, 'b, 'c) t -> int
val map:
('a -> 'a) -> ('b -> 'b) -> ('c -> 'c) -> ('a, 'b, 'c) t -> ('a, 'b, 'c) t
- val mk_internal_pretty_code:
- (Type.precedence -> Format.formatter -> 'a -> unit) ->
- (Type.precedence -> Format.formatter -> 'b -> unit) ->
- (Type.precedence -> Format.formatter -> 'c -> unit) ->
- Type.precedence -> Format.formatter -> ('a, 'b, 'c) t -> unit
val mk_pretty:
(Format.formatter -> 'a -> unit) ->
(Format.formatter -> 'b -> unit) ->
(Format.formatter -> 'c -> unit) ->
Format.formatter -> ('a, 'b, 'c) t -> unit
- val mk_varname:
- ('a -> string) -> ('b -> string) -> ('c -> string) ->
- ('a, 'b, 'c) t -> string
val mk_mem_project:
((Project_skeleton.t -> bool) -> 'a -> bool) ->
((Project_skeleton.t -> bool) -> 'b -> bool) ->
@@ -554,17 +484,7 @@ struct
else*) P.map f1 f2 f3
in
build mk T1.copy T2.copy T3.copy
- let internal_pretty_code =
- let mk f1 f2 f3 =
- if f1 == pp_fail || f2 == pp_fail || f3 == pp_fail then pp_fail
- else fun p fmt x -> P.mk_internal_pretty_code f1 f2 f3 p fmt x
- in
- build mk
- T1.internal_pretty_code
- T2.internal_pretty_code
- T3.internal_pretty_code
let pretty = build P.mk_pretty T1.pretty T2.pretty T3.pretty
- let varname = build P.mk_varname T1.varname T2.varname T3.varname
let mem_project =
let mk f1 f2 f3 =
if P.mk_mem_project == undefined then undefined
@@ -619,21 +539,12 @@ module Polymorphic4
val map:
('a -> 'a) -> ('b -> 'b) -> ('c -> 'c) -> ('d -> 'd) ->
('a, 'b, 'c, 'd) t -> ('a, 'b, 'c, 'd) t
- val mk_internal_pretty_code:
- (Type.precedence -> Format.formatter -> 'a -> unit) ->
- (Type.precedence -> Format.formatter -> 'b -> unit) ->
- (Type.precedence -> Format.formatter -> 'c -> unit) ->
- (Type.precedence -> Format.formatter -> 'd -> unit) ->
- Type.precedence -> Format.formatter -> ('a, 'b, 'c, 'd) t -> unit
val mk_pretty:
(Format.formatter -> 'a -> unit) ->
(Format.formatter -> 'b -> unit) ->
(Format.formatter -> 'c -> unit) ->
(Format.formatter -> 'd -> unit) ->
Format.formatter -> ('a, 'b, 'c, 'd) t -> unit
- val mk_varname:
- ('a -> string) -> ('b -> string) -> ('c -> string) -> ('d -> string) ->
- ('a, 'b, 'c, 'd) t -> string
val mk_mem_project:
((Project_skeleton.t -> bool) -> 'a -> bool) ->
((Project_skeleton.t -> bool) -> 'b -> bool) ->
@@ -704,20 +615,7 @@ struct
else*) P.map f1 f2 f3 f4
in
build mk T1.copy T2.copy T3.copy T4.copy
- let internal_pretty_code =
- let mk f1 f2 f3 f4 =
- if f1 == pp_fail || f2 == pp_fail || f3 == pp_fail || f4 == pp_fail
- then pp_fail
- else fun p fmt x -> P.mk_internal_pretty_code f1 f2 f3 f4 p fmt x
- in
- build mk
- T1.internal_pretty_code
- T2.internal_pretty_code
- T3.internal_pretty_code
- T4.internal_pretty_code
let pretty = build P.mk_pretty T1.pretty T2.pretty T3.pretty T4.pretty
- let varname =
- build P.mk_varname T1.varname T2.varname T3.varname T4.varname
let mem_project =
let mk f1 f2 f3 f4 =
if P.mk_mem_project == undefined then undefined
@@ -763,16 +661,9 @@ module Pair_arg = struct
if x == y then 0 else let n = f1 x1 y1 in if n = 0 then f2 x2 y2 else n
let mk_hash f1 f2 (x1,x2) = f1 x1 + 1351 * f2 x2
let map f1 f2 (x1,x2) = f1 x1, f2 x2
- let mk_internal_pretty_code f1 f2 p fmt (x1, x2) =
- let pp fmt =
- Format.fprintf
- fmt "@[<hv 2>%a,@;%a@]" (f1 Type.Tuple) x1 (f2 Type.Tuple) x2
- in
- Type.par p Type.Tuple fmt pp
- let mk_pretty f1 f2 fmt p =
- Format.fprintf fmt "@[%a@]" (* Type.par put the parenthesis *)
- (mk_internal_pretty_code (fun _ -> f1) (fun _ -> f2) Type.Basic) p
- let mk_varname = undefined
+ let mk_pretty f1 f2 fmt (x1, x2) =
+ let pp fmt = Format.fprintf fmt "@[<hv 2>%a,@;%a@]" f1 x1 f2 x2 in
+ Type.par Type.Basic Type.Tuple fmt pp
let mk_mem_project mem1 mem2 f (x1, x2) = mem1 f x1 && mem2 f x2
end
@@ -819,10 +710,7 @@ let pair (type typ1) (type typ2) (ty1: typ1 Type.t) (ty2: typ2 Type.t) =
let compare = compare X.ty
let hash = hash X.ty
let copy = copy X.ty
- let internal_pretty_code = internal_pretty_code X.ty
- let pretty_code = pretty_code X.ty
- let pretty = from_pretty_code
- let varname = varname ty
+ let pretty = pretty X.ty
let mem_project = mem_project X.ty
end
in
@@ -848,9 +736,7 @@ struct
let hash = undefined
let rehash = undefined
let copy = undefined
- let internal_pretty_code = undefined
let pretty = undefined
- let varname _ = "f"
let mem_project = never_any_project
let reprs =
if Type.may_use_obj () then Type.reprs ty else [ fun _ -> assert false ]
@@ -890,12 +776,8 @@ module type Polymorphic_input = sig
val mk_compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
val mk_hash: ('a -> int) -> 'a t -> int
val map: ('a -> 'a) -> 'a t -> 'a t
- val mk_internal_pretty_code:
- (Type.precedence -> Format.formatter -> 'a -> unit) ->
- Type.precedence -> Format.formatter -> 'a t -> unit
val mk_pretty:
(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
- val mk_varname: ('a -> string) -> 'a t -> string
val mk_mem_project:
((Project_skeleton.t -> bool) -> 'a -> bool) ->
(Project_skeleton.t -> bool) -> 'a t -> bool
@@ -958,15 +840,7 @@ module Polymorphic_gen(P: Polymorphic_input) = struct
(*if f == identity then identity else*)
fun x -> P.map X.copy x
let rehash = R.rehash
-
- let internal_pretty_code =
- let mk f =
- if f == pp_fail then pp_fail
- else fun p fmt x -> P.mk_internal_pretty_code f p fmt x
- in
- build mk X.internal_pretty_code
let pretty = build P.mk_pretty X.pretty
- let varname = build P.mk_varname X.varname
let mem_project =
let mk f =
if P.mk_mem_project == undefined then undefined
@@ -1014,12 +888,9 @@ module Poly_ref =
let mk_compare f x y = if x == y then 0 else f !x !y
let mk_hash f x = f !x
let map f x = ref (f !x)
- let mk_internal_pretty_code f p fmt x =
- let pp fmt = Format.fprintf fmt "@[<hv 2>ref@;%a@]" (f Type.Call) !x in
- Type.par p Type.Call fmt pp
let mk_pretty f fmt x =
- mk_internal_pretty_code (fun _ -> f) Type.Basic fmt x
- let mk_varname = undefined
+ let pp fmt = Format.fprintf fmt "@[<hv 2>ref@;%a@]" f !x in
+ Type.par Type.Basic Type.Call fmt pp
let mk_mem_project mem f x = mem f !x
end)
@@ -1038,10 +909,7 @@ let t_ref (type typ) (ty: typ Type.t) =
let compare = compare ty
let hash = hash ty
let copy = copy ty
- let internal_pretty_code = internal_pretty_code ty
- let pretty_code = pretty_code ty
- let pretty = from_pretty_code
- let varname = varname ty
+ let pretty = pretty ty
let mem_project = mem_project ty
end)
in
@@ -1073,16 +941,13 @@ module Poly_option =
| Some x, Some y -> f x y
let mk_hash f = function None -> 0 | Some x -> f x
let map f = function None -> None | Some x -> Some (f x)
- let mk_internal_pretty_code f p fmt = function
+ let mk_pretty f fmt = function
| None -> Format.fprintf fmt "None"
| Some x ->
let pp fmt =
- Format.fprintf fmt "@[<hv 2>Some@;%a@]" (f Type.Call) x
+ Format.fprintf fmt "@[<hv 2>Some@;%a@]" f x
in
- Type.par p Type.Call fmt pp
- let mk_pretty f fmt x =
- mk_internal_pretty_code (fun _ -> f) Type.Basic fmt x
- let mk_varname = undefined
+ Type.par Type.Basic Type.Call fmt pp
let mk_mem_project mem f = function None -> false | Some x -> mem f x
end)
@@ -1102,10 +967,7 @@ let option (type typ) (ty: typ Type.t) =
let compare = compare ty
let hash = hash ty
let copy = copy ty
- let internal_pretty_code = internal_pretty_code ty
- let pretty_code = pretty_code ty
- let pretty = from_pretty_code
- let varname = varname ty
+ let pretty = pretty ty
let mem_project = mem_project ty
end)
in
@@ -1146,21 +1008,18 @@ module Poly_list =
(0,1) l)
with Too_long n -> n
let map = List.map
- let mk_internal_pretty_code f p fmt l =
+ let mk_pretty f fmt l =
let pp fmt =
Format.fprintf fmt "@[<hv 2>[ %t ]@]"
(fun fmt ->
let rec print fmt = function
| [] -> ()
- | [ x ] -> Format.fprintf fmt "%a" (f Type.List) x
- | x :: l -> Format.fprintf fmt "%a;@;%a" (f Type.List) x print l
+ | [ x ] -> Format.fprintf fmt "%a" f x
+ | x :: l -> Format.fprintf fmt "%a;@;%a" f x print l
in
print fmt l)
in
- Type.par p Type.Basic fmt pp (* Never enclose lists in parentheses *)
- let mk_pretty f fmt x =
- mk_internal_pretty_code (fun _ -> f) Type.Basic fmt x
- let mk_varname = undefined
+ Type.par Type.Basic Type.Basic fmt pp (* Never enclose lists in parentheses *)
let mk_mem_project mem f = List.exists (mem f)
end)
@@ -1180,10 +1039,7 @@ let list (type typ) (ty: typ Type.t) =
let compare = compare ty
let hash = hash ty
let copy = copy ty
- let internal_pretty_code = internal_pretty_code ty
- let pretty_code = pretty_code ty
- let pretty = from_pretty_code
- let varname = varname ty
+ let pretty = pretty ty
let mem_project = mem_project ty
end)
in
@@ -1234,22 +1090,19 @@ module Poly_array =
!acc
;;
let map = Array.map
- let mk_internal_pretty_code f p fmt a =
+ let mk_pretty f fmt a =
let pp fmt =
Format.fprintf fmt "@[<hv 2>[| %t |]@]"
(fun fmt ->
let length = Array.length a in
match length with
| 0 -> ()
- | _ -> (Format.fprintf fmt "%a" (f Type.List) a.(0);
+ | _ -> (Format.fprintf fmt "%a" f a.(0);
for i = 1 to (length - 1) do
- Format.fprintf fmt ";@;%a" (f Type.List) a.(i)
+ Format.fprintf fmt ";@;%a" f a.(i)
done))
in
- Type.par p Type.Basic fmt pp (* Never enclose arrays in parentheses *)
- let mk_pretty f fmt x =
- mk_internal_pretty_code (fun _ -> f) Type.Basic fmt x
- let mk_varname = undefined
+ Type.par Type.Basic Type.Basic fmt pp (* Never enclose arrays in parentheses *)
let mk_mem_project mem f a =
try
for i = 0 to (Array.length a - 1) do
@@ -1274,10 +1127,7 @@ let array (type typ) (ty: typ Type.t) =
let compare = compare ty
let hash = hash ty
let copy = copy ty
- let internal_pretty_code = internal_pretty_code ty
- let pretty_code = pretty_code ty
- let pretty = from_pretty_code
- let varname = varname ty
+ let pretty = pretty ty
let mem_project = mem_project ty
end)
in
@@ -1304,9 +1154,7 @@ module Poly_queue =
let mk_compare = undefined
let mk_hash = undefined
let map = undefined
- let mk_internal_pretty_code = undefined
let mk_pretty = undefined
- let mk_varname = undefined
let mk_mem_project mem f q =
try Queue.iter (fun x -> if mem f x then raise Exit) q; false
with Exit -> true
@@ -1327,10 +1175,7 @@ let queue (type typ) (ty: typ Type.t) =
let compare = compare ty
let hash = hash ty
let copy = copy ty
- let internal_pretty_code = internal_pretty_code ty
- let pretty_code = pretty_code ty
- let pretty = from_pretty_code
- let varname = varname ty
+ let pretty = pretty ty
let mem_project = mem_project ty
end)
in
@@ -1375,27 +1220,6 @@ struct
(* if E.copy == identity then identity
else*) fun s -> S.fold (fun x -> S.add (E.copy x)) s S.empty
- let internal_pretty_code p_caller fmt s =
- if is_empty s then
- Format.fprintf fmt "%s.empty" Info.module_name
- else
- let pp fmt =
- if S.cardinal s = 1 then
- Format.fprintf fmt "@[<hv 2>%s.singleton@;%a@]"
- Info.module_name
- (E.internal_pretty_code Type.Call)
- (Caml_list.hd (S.elements s))
- else
- Format.fprintf fmt
- "@[<hv 2>List.fold_left@;\
- (fun acc s -> %s.add s acc)@;%s.empty@;%a@]"
- Info.module_name
- Info.module_name
- (let module L = List(E) in L.internal_pretty_code Type.Call)
- (S.elements s)
- in
- Type.par p_caller Type.Call fmt pp
-
let pretty fmt s =
let pp_elt pp fmt v =
Format.fprintf fmt "@[%a@]" pp v
@@ -1404,7 +1228,6 @@ struct
~pre:"@[<hov 2>{@ " ~sep:";@ " ~suf:"@ }@]"
S.iter (pp_elt E.pretty) fmt s
- let varname = undefined
let mem_project p s =
try S.iter (fun x -> if E.mem_project p x then raise Exit) s; false
with Exit -> true
@@ -1424,10 +1247,7 @@ struct
let equal = P.equal
let compare = P.compare
let hash = P.hash
- let internal_pretty_code = P.internal_pretty_code
- let pretty_code = P.pretty_code
let pretty = P.pretty
- let varname = P.varname
let mem_project = P.mem_project
let copy = P.copy
@@ -1459,28 +1279,6 @@ struct
let mk_equal = M.equal
let mk_hash = undefined
let map = M.map
- let mk_internal_pretty_code = undefined
- (*f_value p_caller fmt map =
- (* [JS 2011/04/01] untested code! *)
- let pp_empty fmt = Format.fprintf fmt "%s.empty" Info.module_name in
- if M.is_empty map then
- Type.par p_caller Type.Basic fmt pp_empty
- else
- let pp fmt =
- Format.fprintf
- fmt "@[<hv 2>@[<hv 2>let map =@;%t@;<1 -2>in@]" pp_empty;
- M.iter
- (fun k v ->
- Format.fprintf
- fmt
- "@[<hv 2>let map =@;%s.add@;@[<hv 2>map@;%a@;%a@]@;<1 -2>in@]"
- Info.module_name
- (Key.internal_pretty_code Type.Call) k
- (f_value Type.Call) v)
- map;
- Format.fprintf fmt "@[map@]@]"
- in
- Type.par p_caller Type.Call fmt pp*)
let mk_pretty f_value fmt map =
Format.fprintf fmt "@[{{ ";
M.iter
@@ -1490,9 +1288,6 @@ struct
f_value v)
map;
Format.fprintf fmt " }}@]"
- let mk_varname _ =
- if Key.varname == undefined then undefined
- else fun _ -> Format.sprintf "%s_map" Key.name
let mk_mem_project =
if Key.mem_project == undefined then undefined
else
@@ -1570,9 +1365,7 @@ struct
let h2 = H.create (H.length tbl) (* may be very memory-consuming *) in
H.iter (fun k v -> H.add h2 k v) h;
h2
- let mk_internal_pretty_code = undefined
- let mk_pretty = from_pretty_code
- let mk_varname = undefined
+ let mk_pretty = undefined
let mk_mem_project =
if Key.mem_project == undefined then undefined
else
@@ -1624,7 +1417,6 @@ struct
let descr = Descr.of_type ty
let packed_descr = Descr.pack descr
let reprs = Type.reprs ty
- let pretty_code = undefined
end)
in M.ty
@@ -1729,7 +1521,6 @@ module Simple_type
val reprs: t list
val pretty: Format.formatter -> t -> unit
val copy: t -> t
- val varname: t -> string
val compare: t -> t -> int
val equal: t -> t -> bool
end) =
@@ -1748,10 +1539,7 @@ struct
let hash = FCHashtbl.hash
let rehash = identity
let copy = X.copy
- let internal_pretty_code =
- if X.pretty == undefined then undefined else fun _ -> X.pretty
let pretty = X.pretty
- let varname = X.varname
let mem_project = never_any_project
end))
(struct let module_name = module_name end)
@@ -1770,7 +1558,6 @@ module Unit =
let compare () () = 0
let equal () () = true
let pretty fmt () = Format.fprintf fmt "()"
- let varname = undefined
end)
let unit = Unit.ty
@@ -1784,7 +1571,6 @@ module Bool =
let compare : bool -> bool -> int = Stdlib.compare
let equal : bool -> bool -> bool = (=)
let pretty fmt b = Format.fprintf fmt "%B" b
- let varname _ = "b"
end)
let bool = Bool.ty
@@ -1798,7 +1584,6 @@ module Int = struct
let compare : int -> int -> int = Stdlib.compare
let equal : int -> int -> bool = (=)
let pretty fmt n = Format.fprintf fmt "%d" n
- let varname _ = "n"
end)
let compare : int -> int -> int = Stdlib.compare
end
@@ -1814,7 +1599,6 @@ module Int32 =
let compare = Int32.compare
let equal : int32 -> int32 -> bool = (=)
let pretty fmt n = Format.fprintf fmt "%ld" n
- let varname _ = "n32"
end)
let int32 = Int32.ty
@@ -1828,7 +1612,6 @@ module Int64 =
let compare = Int64.compare
let equal : int64 -> int64 -> bool = (=)
let pretty fmt n = Format.fprintf fmt "%Ld" n
- let varname _ = "n64"
end)
let int64 = Int64.ty
@@ -1842,7 +1625,6 @@ module Nativeint =
let compare = Nativeint.compare
let equal : nativeint -> nativeint -> bool = (=)
let pretty fmt n = Format.fprintf fmt "%nd" n
- let varname _ = "native_n"
end)
let nativeint = Nativeint.ty
@@ -1856,7 +1638,6 @@ module Float =
let compare : float -> float -> int = Stdlib.compare
let equal : float -> float -> bool = (=)
let pretty fmt f = Format.fprintf fmt "%f" f
- let varname _ = "f"
end)
let float = Float.ty
@@ -1870,7 +1651,6 @@ module Char =
let compare = Char.compare
let equal : char -> char -> bool = (=)
let pretty fmt c = Format.fprintf fmt "%c" c
- let varname _ = "c"
end)
let char = Char.ty
@@ -1884,7 +1664,6 @@ module String =
let compare = String.compare
let equal : string -> string -> bool = (=)
let pretty fmt s = Format.fprintf fmt "%S" s
- let varname _ = "s"
end)
let string = String.ty
@@ -1900,9 +1679,7 @@ module Formatter =
let hash = undefined
let rehash = undefined
let copy = undefined
- let internal_pretty_code = undefined
let pretty = undefined
- let varname _ = "fmt"
let mem_project = never_any_project
end)
let formatter = Formatter.ty
@@ -1919,17 +1696,8 @@ module Integer =
let hash = Integer.hash
let rehash = identity
let copy = identity
- let internal_pretty_code par fmt n =
- let pp fmt =
- Format.fprintf
- fmt
- "Integer.of_string %S"
- (Integer.to_string n)
- in
- Type.par par Type.Call fmt pp
(* TODO: this should take into account kernel's option -big-ints-hex *)
let pretty = Integer.pretty
- let varname _ = "integer_n"
let mem_project = never_any_project
end)
let integer = Integer.ty
@@ -1944,7 +1712,6 @@ module Filepath = struct
let compare = Filepath.Normalized.compare
let equal : t -> t -> bool = (=)
let pretty = Filepath.Normalized.pretty
- let varname _ = "p"
end)
let dummy = Filepath.Normalized.empty
let of_string ?existence ?base_name s =
@@ -1977,21 +1744,11 @@ module Triple_arg = struct
else n
let mk_hash f1 f2 f3 (x1,x2,x3) = f1 x1 + 1351 * f2 x2 + 257 * f3 x3
let map f1 f2 f3 (x1,x2,x3) = f1 x1, f2 x2, f3 x3
- let mk_internal_pretty_code f1 f2 f3 p fmt (x1, x2, x3) =
+ let mk_pretty f1 f2 f3 fmt (x1, x2, x3) =
let pp fmt =
- Format.fprintf
- fmt "@[<hv 2>%a,@;%a,@;%a@]"
- (f1 Type.Tuple) x1
- (f2 Type.Tuple) x2
- (f3 Type.Tuple) x3
+ Format.fprintf fmt "@[<hv 2>%a,@;%a,@;%a@]" f1 x1 f2 x2 f3 x3
in
- Type.par p Type.Tuple fmt pp
- let mk_pretty f1 f2 f3 fmt p =
- Format.fprintf fmt "@[(%a)@]"
- (mk_internal_pretty_code
- (fun _ -> f1) (fun _ -> f2) (fun _ -> f3) Type.Basic)
- p
- let mk_varname = undefined
+ Type.par Type.Basic Type.Tuple fmt pp
let mk_mem_project mem1 mem2 mem3 f (x1, x2, x3) =
mem1 f x1 && mem2 f x2 && mem3 f x3
end
@@ -2042,10 +1799,7 @@ let triple
let compare = compare X.ty
let hash = hash X.ty
let copy = copy X.ty
- let internal_pretty_code = internal_pretty_code X.ty
- let pretty_code = pretty_code X.ty
- let pretty = from_pretty_code
- let varname = varname ty
+ let pretty = pretty X.ty
let mem_project = mem_project X.ty
end
in
@@ -2086,22 +1840,11 @@ module Quadruple_arg = struct
let mk_hash f1 f2 f3 f4 (x1,x2,x3,x4) =
f1 x1 + 1351 * f2 x2 + 257 * f3 x3 + 997 * f4 x4
let map f1 f2 f3 f4 (x1,x2,x3,x4) = f1 x1, f2 x2, f3 x3, f4 x4
- let mk_internal_pretty_code f1 f2 f3 f4 p fmt (x1, x2, x3, x4) =
+ let mk_pretty f1 f2 f3 f4 fmt (x1, x2, x3, x4) =
let pp fmt =
- Format.fprintf
- fmt "@[<hv 2>%a,@;%a,@;%a,@;%a@]"
- (f1 Type.Tuple) x1
- (f2 Type.Tuple) x2
- (f3 Type.Tuple) x3
- (f4 Type.Tuple) x4
+ Format.fprintf fmt "@[<hv 2>%a,@;%a,@;%a,@;%a@]" f1 x1 f2 x2 f3 x3 f4 x4
in
- Type.par p Type.Tuple fmt pp
- let mk_pretty f1 f2 f3 f4 fmt p =
- Format.fprintf fmt "@[(%a)@]"
- (mk_internal_pretty_code
- (fun _ -> f1) (fun _ -> f2) (fun _ -> f3) (fun _ -> f4) Type.Basic)
- p
- let mk_varname = undefined
+ Type.par Type.Basic Type.Tuple fmt pp
let mk_mem_project mem1 mem2 mem3 mem4 f (x1, x2, x3, x4) =
mem1 f x1 && mem2 f x2 && mem3 f x3 && mem4 f x4
end
@@ -2157,10 +1900,7 @@ let quadruple
let compare = compare X.ty
let hash = hash X.ty
let copy = copy X.ty
- let internal_pretty_code = internal_pretty_code X.ty
- let pretty_code = pretty_code X.ty
- let pretty = from_pretty_code
- let varname = varname ty
+ let pretty = pretty X.ty
let mem_project = mem_project X.ty
end
in
diff --git a/src/libraries/datatype/datatype.mli b/src/libraries/datatype/datatype.mli
index fb520585b8f4155b5c48fc2210699e5c7f033c87..50a1588d6d588434f49419d9ed3c414d71d9253c 100644
--- a/src/libraries/datatype/datatype.mli
+++ b/src/libraries/datatype/datatype.mli
@@ -30,16 +30,16 @@
(* ********************************************************************** *)
(** Values associated to each datatype.
- Some others are provided directly in module {!Type}. *)
+ Some others are provided directly in module {!Type}.
+ @before Frama-C+dev there was additional fields only used for Journalization
+ that has been removed.
+*)
type 'a t = private
{ equal: 'a -> 'a -> bool;
compare: 'a -> 'a -> int;
hash: 'a -> int;
copy: 'a -> 'a;
- internal_pretty_code: Type.precedence -> Format.formatter -> 'a -> unit;
- pretty_code: Format.formatter -> 'a -> unit;
pretty: Format.formatter -> 'a -> unit;
- varname: 'a -> string;
mem_project: (Project_skeleton.t -> bool) -> 'a -> bool }
(** A type with its type value. *)
@@ -48,7 +48,10 @@ module type Ty = sig
val ty: t Type.t
end
-(** All values associated to a datatype, excepted [copy]. *)
+(** All values associated to a datatype, excepted [copy].
+ @before Frama-C+dev there was several additional values only used for
+ Journalization that has been removed.
+*)
module type S_no_copy = sig
include Ty
@@ -74,21 +77,9 @@ module type S_no_copy = sig
val hash: t -> int
(** Hash function: same spec than [Hashtbl.hash]. *)
- val pretty_code: Format.formatter -> t -> unit
- (** Pretty print each value in an ML-like style: the result must be a valid
- OCaml expression. Only useful for journalisation. *)
-
- val internal_pretty_code: Type.precedence -> Format.formatter -> t -> unit
- (** Same spec than [pretty_code], but must take care of the precedence of the
- context in order to put parenthesis if required. See {!Type.par}. *)
-
val pretty: Format.formatter -> t -> unit
(** Pretty print each value in an user-friendly way. *)
- val varname: t -> string
- (** A good prefix name to use for an OCaml variable of this type. Only useful
- for journalisation. *)
-
val mem_project: (Project_skeleton.t -> bool) -> t -> bool
(** [mem_project f x] must return [true] iff there is a value [p] of type
[Project.t] in [x] such that [f p] returns [true]. *)
@@ -111,11 +102,7 @@ val equal: 'a Type.t -> 'a -> 'a -> bool
val compare: 'a Type.t -> 'a -> 'a -> int
val hash: 'a Type.t -> 'a -> int
val copy: 'a Type.t -> 'a -> 'a
-val internal_pretty_code:
- 'a Type.t -> Type.precedence -> Format.formatter -> 'a -> unit
-val pretty_code: 'a Type.t -> Format.formatter -> 'a -> unit
val pretty: 'a Type.t -> Format.formatter -> 'a -> unit
-val varname: 'a Type.t -> 'a -> string
val mem_project: 'a Type.t -> (Project_skeleton.t -> bool) -> 'a -> bool
(* ********************************************************************** *)
@@ -135,22 +122,17 @@ val from_compare: 'a -> 'a -> bool
(** Must be used for [equal] in order to implement it by [compare x y = 0]
(with your own [compare] function). *)
-val from_pretty_code: Format.formatter -> 'a -> unit
-(** Must be used for [pretty] in order to implement it by [pretty_code]
- provided by the datatype from your own [internal_pretty_code] function. *)
-
val never_any_project: (Project_skeleton.t -> bool) -> 'a -> bool
(** Must be used for [mem_project] if values of your type does never contain
any project.
@plugin development guide *)
-val pp_fail: Type.precedence -> Format.formatter -> 'a -> unit
-(** Must be used for [internal_pretty_code] if this pretty-printer must
- fail only when called.
- @plugin development guide *)
-
(** Sub-signature of {!S}.
- @plugin development guide *)
+ @plugin development guide
+
+ @before Frama-C+dev there was several additional values only used for
+ Journalization that has been removed.
+*)
module type Undefined = sig
val structural_descr: Structural_descr.t
val equal: 'a -> 'a -> bool
@@ -158,9 +140,7 @@ module type Undefined = sig
val hash: 'a -> int
val rehash: 'a -> 'a
val copy: 'a -> 'a
- val internal_pretty_code: Type.precedence -> Format.formatter -> 'a -> unit
val pretty: Format.formatter -> 'a -> unit
- val varname: 'a -> string
val mem_project: (Project_skeleton.t -> bool) -> 'a -> bool
end
@@ -187,7 +167,11 @@ module Serializable_undefined: Undefined
(** Input signature of {!Make} and {!Make_with_collections}.
Values to implement in order to get a datatype.
- Feel free to use easy builders (see above) for easy implementation. *)
+ Feel free to use easy builders (see above) for easy implementation.
+
+ @before Frama-C+dev there was several additional values only used for
+ Journalization that has been removed.
+*)
module type Make_input = sig
type t (** Type for this datatype *)
@@ -215,9 +199,7 @@ module type Make_input = sig
val compare: t -> t -> int
val hash: t -> int
val copy: t -> t
- val internal_pretty_code: Type.precedence -> Format.formatter -> t -> unit
val pretty: Format.formatter -> t -> unit
- val varname: t -> string
val mem_project: (Project_skeleton.t -> bool) -> t -> bool
end
@@ -366,7 +348,11 @@ module type Polymorphic = sig
end
(** Functor for polymorphic types with only 1 type variable.
- @plugin development guide *)
+ @plugin development guide
+
+ @before Frama-C+dev the functor had several additional values only used for
+ Journalization that has been removed.
+*)
module Polymorphic
(P: sig
include Type.Polymorphic_input
@@ -374,12 +360,8 @@ module Polymorphic
val mk_compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
val mk_hash: ('a -> int) -> 'a t -> int
val map: ('a -> 'a) -> 'a t -> 'a t
- val mk_internal_pretty_code:
- (Type.precedence -> Format.formatter -> 'a -> unit) ->
- Type.precedence -> Format.formatter -> 'a t -> unit
val mk_pretty:
(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
- val mk_varname: ('a -> string) -> 'a t -> string
val mk_mem_project:
((Project_skeleton.t -> bool) -> 'a -> bool) ->
(Project_skeleton.t -> bool) -> 'a t -> bool
@@ -393,7 +375,11 @@ module type Polymorphic2 = sig
end
(** Functor for polymorphic types with 2 type variables.
- @plugin development guide *)
+ @plugin development guide
+
+ @before Frama-C+dev the functor had several additional values only used for
+ Journalization that has been removed.
+*)
module Polymorphic2
(P: sig
include Type.Polymorphic2_input
@@ -404,14 +390,9 @@ module Polymorphic2
('a -> 'a -> int) -> ('b -> 'b -> int) -> ('a, 'b) t -> ('a, 'b) t -> int
val mk_hash: ('a -> int) -> ('b -> int) -> ('a, 'b) t -> int
val map: ('a -> 'a) -> ('b -> 'b) -> ('a, 'b) t -> ('a, 'b) t
- val mk_internal_pretty_code:
- (Type.precedence -> Format.formatter -> 'a -> unit) ->
- (Type.precedence -> Format.formatter -> 'b -> unit) ->
- Type.precedence -> Format.formatter -> ('a, 'b) t -> unit
val mk_pretty:
(Format.formatter -> 'a -> unit) -> (Format.formatter -> 'b -> unit) ->
Format.formatter -> ('a, 'b) t -> unit
- val mk_varname: ('a -> string) -> ('b -> string) -> ('a, 'b) t -> string
val mk_mem_project:
((Project_skeleton.t -> bool) -> 'a -> bool) ->
((Project_skeleton.t -> bool) -> 'b -> bool) ->
@@ -428,7 +409,10 @@ end
(** Functor for polymorphic types with 3 type variables.
@since Oxygen-20120901
- @plugin development guide *)
+ @plugin development guide
+ @before Frama-C+dev the functor had several additional values only used for
+ Journalization that has been removed.
+*)
module Polymorphic3
(P: sig
include Type.Polymorphic3_input
@@ -443,19 +427,11 @@ module Polymorphic3
('a -> int) -> ('b -> int) -> ('c -> int) -> ('a, 'b, 'c) t -> int
val map:
('a -> 'a) -> ('b -> 'b) -> ('c -> 'c) -> ('a, 'b, 'c) t -> ('a, 'b, 'c) t
- val mk_internal_pretty_code:
- (Type.precedence -> Format.formatter -> 'a -> unit) ->
- (Type.precedence -> Format.formatter -> 'b -> unit) ->
- (Type.precedence -> Format.formatter -> 'c -> unit) ->
- Type.precedence -> Format.formatter -> ('a, 'b, 'c) t -> unit
val mk_pretty:
(Format.formatter -> 'a -> unit) ->
(Format.formatter -> 'b -> unit) ->
(Format.formatter -> 'c -> unit) ->
Format.formatter -> ('a, 'b, 'c) t -> unit
- val mk_varname:
- ('a -> string) -> ('b -> string) -> ('c -> string) ->
- ('a, 'b, 'c) t -> string
val mk_mem_project:
((Project_skeleton.t -> bool) -> 'a -> bool) ->
((Project_skeleton.t -> bool) -> 'b -> bool) ->
@@ -474,7 +450,10 @@ end
(** Functor for polymorphic types with 4 type variables.
@since Oxygen-20120901
- @plugin development guide *)
+ @plugin development guide
+ @before Frama-C+dev the functor had several additional values only used for
+ Journalization that has been removed.
+*)
module Polymorphic4
(P: sig
include Type.Polymorphic4_input
@@ -493,21 +472,12 @@ module Polymorphic4
val map:
('a -> 'a) -> ('b -> 'b) -> ('c -> 'c) -> ('d -> 'd) ->
('a, 'b, 'c, 'd) t -> ('a, 'b, 'c, 'd) t
- val mk_internal_pretty_code:
- (Type.precedence -> Format.formatter -> 'a -> unit) ->
- (Type.precedence -> Format.formatter -> 'b -> unit) ->
- (Type.precedence -> Format.formatter -> 'c -> unit) ->
- (Type.precedence -> Format.formatter -> 'd -> unit) ->
- Type.precedence -> Format.formatter -> ('a, 'b, 'c, 'd) t -> unit
val mk_pretty:
(Format.formatter -> 'a -> unit) ->
(Format.formatter -> 'b -> unit) ->
(Format.formatter -> 'c -> unit) ->
(Format.formatter -> 'd -> unit) ->
Format.formatter -> ('a, 'b, 'c, 'd) t -> unit
- val mk_varname:
- ('a -> string) -> ('b -> string) -> ('c -> string) -> ('d -> string) ->
- ('a, 'b, 'c, 'd) t -> string
val mk_mem_project:
((Project_skeleton.t -> bool) -> 'a -> bool) ->
((Project_skeleton.t -> bool) -> 'b -> bool) ->
diff --git a/src/libraries/project/project.ml b/src/libraries/project/project.ml
index 846407b26e1ddf5773036e0fb42a7ba7a713575c..691c2a71679150a14e37fffcab248713a8604bb0 100644
--- a/src/libraries/project/project.ml
+++ b/src/libraries/project/project.ml
@@ -51,14 +51,7 @@ module D =
let hash p = p.pid
let rehash x = !rehash_ref x
let copy = Datatype.undefined
- let internal_pretty_code p_caller fmt p =
- let pp f =
- Format.fprintf
- f "@[<hv 2>Project.from_unique_name@;%S@]" p.unique_name
- in
- Type.par p_caller Type.Call fmt pp
let pretty fmt p = Format.fprintf fmt "project %S" p.unique_name
- let varname p = "p_" ^ p.name
let mem_project f x = f x
end)
include (D: Datatype.S_no_copy with type t = Project_skeleton.t)
@@ -249,8 +242,6 @@ let guarded_feedback selection level fmt_msg =
else
Pretty_utils.nullprintf fmt_msg
-let dft_sel () = State_selection.full
-
module Q = Qstack.Make(struct type t = project let equal = equal end)
let projects = Q.create ()
@@ -283,20 +274,14 @@ module Mem = struct
end
module Setter = Make_setter(Mem)
-let unjournalized_set_name p s =
+let set_name p s =
feedback ~dkey ~level:2 "renaming project %S to %S" p.unique_name s;
Setter.set_name p s
-let set_name =
- Journal.register
- "Project.set_name"
- (Datatype.func2 ty Datatype.string Datatype.unit)
- unjournalized_set_name
-
module Create_Hook = Hook.Build(struct type t = project end)
let register_create_hook = Create_Hook.extend
-let force_create name =
+let create name =
feedback ~dkey ~level:2 "creating project %S" name;
let p = Setter.make name in
feedback ~dkey ~level:3 "its unique name is %S" p.unique_name;
@@ -305,18 +290,6 @@ let force_create name =
Create_Hook.apply p;
p
-let journalized_create =
- Journal.register
- "Project.create" (Datatype.func Datatype.string ty) force_create
-
-(* do not journalise the first call to [create] *)
-let create =
- let first = ref true in
- fun name ->
- let p = if !first then force_create name else journalized_create name in
- first := false;
- p
-
let get_name p = p.name
let get_unique_name p = p.unique_name
@@ -328,7 +301,7 @@ module Set_Current_Hook = Hook.Build(struct type t = project end)
let register_after_set_current_hook ~user_only =
if user_only then Set_Current_Hook_User.extend else Set_Current_Hook.extend
-let unjournalized_set_current =
+let force_set_current =
let apply_hook = ref false in
fun on selection p ->
if not (Q.mem p projects) then
@@ -350,16 +323,8 @@ let unjournalized_set_current =
apply_hook := false
end
-let journalized_set_current =
- let lbl = Datatype.optlabel_func in
- Journal.register "Project.set_current"
- (lbl "on" (fun () -> false) Datatype.bool
- (lbl "selection" dft_sel State_selection.ty
- (Datatype.func ty Datatype.unit)))
- unjournalized_set_current
-
let set_current ?(on=false) ?(selection=State_selection.full) p =
- if not (equal p (current ())) then journalized_set_current on selection p
+ if not (equal p (current ())) then force_set_current on selection p
let set_current_as_last_created () =
Option.iter (fun p -> set_current p) !last_created_by_copy_ref
@@ -367,12 +332,7 @@ let set_current_as_last_created () =
(** Indicates if we should keep [p] as the current project when calling {!on p}. *)
let keep_current: bool ref = ref false
-let unjournalized_set_keep_current b = keep_current := b
-
-let set_keep_current =
- Journal.register "Project.set_keep_current"
- (Datatype.func Datatype.bool Datatype.unit)
- unjournalized_set_keep_current
+let set_keep_current b = keep_current := b
let on ?selection p f x =
let old_current = current () in
@@ -415,7 +375,7 @@ exception Cannot_remove of string
module Before_remove = Hook.Build(struct type t = project end)
let register_before_remove_hook = Before_remove.extend
-let unjournalized_remove project =
+let remove ?(project=current()) () =
feedback ~dkey ~level:2 "removing project %S" project.unique_name;
if Q.length projects = 1 then raise (Cannot_remove project.unique_name);
Before_remove.apply project;
@@ -435,15 +395,6 @@ let unjournalized_remove project =
!last_created_by_copy_ref;
(* clear all the states of other projects referring to the delete project *)
Q.iter (States_operations.clear_some_projects (equal project)) projects
-(* Gc.major ()*)
-
-let journalized_remove =
- Journal.register "Project.remove"
- (Datatype.optlabel_func
- "project" current ty (Datatype.func Datatype.unit Datatype.unit))
- (fun project () -> unjournalized_remove project)
-
-let remove ?(project=current()) () = journalized_remove project ()
let remove_all () =
feedback ~dkey ~level:2 "removing all existing projects";
@@ -456,19 +407,11 @@ let remove_all () =
with NoProject ->
()
-let journalized_copy =
- let lbl = Datatype.optlabel_func in
- Journal.register "Project.copy"
- (lbl "selection" dft_sel State_selection.ty
- (lbl "src" current ty (Datatype.func ty Datatype.unit)))
- (fun selection src dst ->
- guarded_feedback selection 2 "copying project from %S to %S"
- src.unique_name dst.unique_name;
- States_operations.commit ~selection src;
- States_operations.copy ~selection src dst)
-
let copy ?(selection=State_selection.full) ?(src=current()) dst =
- journalized_copy selection src dst
+ guarded_feedback selection 2 "copying project from %S to %S"
+ src.unique_name dst.unique_name;
+ States_operations.commit ~selection src;
+ States_operations.copy ~selection src dst
module Before_Clear_Hook = Hook.Build(struct type t = project end)
let register_todo_before_clear = Before_Clear_Hook.extend
@@ -476,31 +419,16 @@ let register_todo_before_clear = Before_Clear_Hook.extend
module After_Clear_Hook = Hook.Build(struct type t = project end)
let register_todo_after_clear = After_Clear_Hook.extend
-let journalized_clear =
- let lbl = Datatype.optlabel_func in
- Journal.register "Project.clear"
- (lbl "selection" dft_sel State_selection.ty
- (lbl "project" current ty (Datatype.func Datatype.unit Datatype.unit)))
- (fun selection project () ->
- guarded_feedback selection 2 "clearing project %S" project.unique_name;
- Before_Clear_Hook.apply project;
- States_operations.clear ~selection project;
- After_Clear_Hook.apply project;
- (*Gc.major ()*))
-
let clear ?(selection=State_selection.full) ?(project=current()) () =
- journalized_clear selection project ()
+ guarded_feedback selection 2 "clearing project %S" project.unique_name;
+ Before_Clear_Hook.apply project;
+ States_operations.clear ~selection project;
+ After_Clear_Hook.apply project
-let unjournalized_clear_all () =
+let clear_all () =
Q.iter States_operations.clear projects;
Gc.full_major ()
-let clear_all =
- Journal.register
- "Project.clear_all"
- (Datatype.func Datatype.unit Datatype.unit)
- unjournalized_clear_all
-
(* ************************************************************************** *)
(* Save/load *)
(* ************************************************************************** *)
@@ -540,36 +468,16 @@ let save_projects selection projects filename =
end else
abort "saving a file is not supported in the 'no obj' mode"
-let unjournalized_save selection project filename =
+let save ?(selection=State_selection.full) ?(project=current()) filename =
guarded_feedback selection 2 "saving project %S into file %a"
project.unique_name Filepath.Normalized.pretty filename;
save_projects selection (Q.singleton project) filename
-let journalized_save =
- let lbl = Datatype.optlabel_func in
- Journal.register "Project.save"
- (lbl "selection" dft_sel State_selection.ty
- (lbl "project" current ty (Datatype.func Datatype.Filepath.ty Datatype.unit)))
- unjournalized_save
-
-let save ?(selection=State_selection.full) ?(project=current()) filename =
- journalized_save selection project filename
-
-let unjournalized_save_all selection filename =
+let save_all ?(selection=State_selection.full) filename =
guarded_feedback selection 2 "saving the current session into file %a"
Filepath.Normalized.pretty filename;
save_projects selection projects filename
-let journalized_save_all =
- let lbl = Datatype.optlabel_func in
- Journal.register "Project.save_all"
- (lbl "selection" dft_sel State_selection.ty
- (Datatype.func Datatype.Filepath.ty Datatype.unit))
- unjournalized_save_all
-
-let save_all ?(selection=State_selection.full) filename =
- journalized_save_all selection filename
-
module Descr = struct
let project_under_copy_ref: project option ref = ref None
@@ -655,7 +563,7 @@ module Descr = struct
(fun () ->
(* Local states must be up-to-date according to [p] when
unmarshalling states of [p] *)
- unjournalized_set_current true selection p;
+ force_set_current true selection p;
Before_load.apply ();
Descr.t_list tbl_on_disk)
in
@@ -738,56 +646,39 @@ let load_projects ~project_under_copy selection ?name filename =
temporarily. *)
let true_current = current () in
Q.add last projects;
- unjournalized_set_current true selection true_current;
+ force_set_current true selection true_current;
Q.remove last projects;
After_global_load.apply ();
loaded_projects
end else
abort "loading a file is not supported in the 'no obj' mode"
-let unjournalized_load ~project_under_copy selection name filename =
+let load_with_copy
+ ?project_under_copy ?(selection=State_selection.full) ?name filename =
guarded_feedback selection 2 "loading the project saved in file %a"
Filepath.Normalized.pretty filename;
match load_projects ~project_under_copy selection ?name filename with
| [ p ] -> p
| [] | _ :: _ :: _ -> assert false
-let journalized_load =
- let lbl = Datatype.optlabel_func in
- Journal.register "Project.load"
- (lbl "selection" dft_sel State_selection.ty
- (lbl "name" (fun () -> None)
- (Datatype.option Datatype.string) (Datatype.func Datatype.Filepath.ty ty)))
- (unjournalized_load ~project_under_copy:None)
-
-let load ?(selection=State_selection.full) ?name filename =
- journalized_load selection name filename
+let load = load_with_copy ?project_under_copy:None
-let unjournalized_load_all selection filename =
+let load_all ?(selection=State_selection.full) filename =
remove_all ();
guarded_feedback selection 2 "loading the session saved in file %a"
Filepath.Normalized.pretty filename;
try
ignore (load_projects ~project_under_copy:None selection filename)
with IOError _ as e ->
- unjournalized_set_current false selection (create "default");
+ force_set_current false selection (create "default");
raise e
-let journalized_load_all =
- let lbl = Datatype.optlabel_func in
- Journal.register "Project.load_all"
- (lbl "selection" dft_sel State_selection.ty
- (Datatype.func Datatype.Filepath.ty Datatype.unit))
- unjournalized_load_all
-
-let load_all ?(selection=State_selection.full) filename =
- journalized_load_all selection filename
-
module Create_by_copy_hook = Hook.Build(struct type t = project * project end)
let create_by_copy_hook f =
Create_by_copy_hook.extend (fun (src, dst) -> f src dst)
-let unjournalized_create_by_copy selection src last name =
+let create_by_copy
+ ?(selection=State_selection.full) ?(src=current()) ~last name =
guarded_feedback selection 2 "creating project %S by copying project %S"
name (src.unique_name);
let filename =
@@ -797,10 +688,7 @@ let unjournalized_create_by_copy selection src last name =
in
save ~selection ~project:src filename;
try
- let prj =
- unjournalized_load
- ~project_under_copy:(Some src) selection (Some name) filename
- in
+ let prj = load_with_copy ~project_under_copy:src ~selection ~name filename in
Extlib.safe_remove (filename:>string);
if last then last_created_by_copy_ref := Some prj;
Create_by_copy_hook.apply (src, prj);
@@ -809,19 +697,6 @@ let unjournalized_create_by_copy selection src last name =
Extlib.safe_remove (filename:>string);
raise e
-let journalized_create_by_copy =
- let lbl = Datatype.optlabel_func in
- Journal.register "Project.create_by_copy"
- (lbl "selection" dft_sel State_selection.ty
- (lbl "src" current ty
- (Datatype.func2
- ~label1:("last", None) Datatype.bool Datatype.string ty)))
- unjournalized_create_by_copy
-
-let create_by_copy
- ?(selection=State_selection.full) ?(src=current()) ~last name =
- journalized_create_by_copy selection src last name
-
(* ************************************************************************** *)
(** {2 Undoing} *)
(* ************************************************************************** *)
@@ -834,15 +709,11 @@ module Undo = struct
let clear_breakpoint () = Extlib.safe_remove (!filename:>string)
let restore () =
- if Cmdline.use_obj then begin
- try
- Journal.prevent load_all !filename;
- Journal.restore ();
- clear_breakpoint ()
- with IOError s ->
- feedback ~dkey "cannot restore the last breakpoint: %S" s;
- clear_breakpoint ()
- end
+ try
+ clear_breakpoint ()
+ with IOError s ->
+ feedback ~dkey "cannot restore the last breakpoint: %S" s;
+ clear_breakpoint ()
let breakpoint () =
if Cmdline.use_obj then begin
@@ -851,8 +722,6 @@ module Undo = struct
(try Extlib.temp_file_cleanup_at_exit short_filename ".sav"
with Extlib.Temp_file_error s ->
abort "cannot create temporary file: %s" s);
- Journal.prevent save_all !filename;
- Journal.save ()
end
end
diff --git a/src/libraries/project/state.ml b/src/libraries/project/state.ml
index c714007a60e0bc233cdcb00a4653c4661e4f3a64..011a5bfe5cdc8bada235b36ae5f1338ac7f8e193 100644
--- a/src/libraries/project/state.ml
+++ b/src/libraries/project/state.ml
@@ -104,13 +104,7 @@ include Datatype.Make_with_collections
let hash x = Hashtbl.hash x.unique_name
let copy = Datatype.undefined
let rehash = Datatype.undefined
- let internal_pretty_code p_caller fmt s =
- let pp fmt =
- Format.fprintf fmt "@[<hv 2>State.get@;%S@]" s.unique_name
- in
- Type.par p_caller Type.Call fmt pp
let pretty fmt s = Format.fprintf fmt "state %S" s.unique_name
- let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
end)
diff --git a/src/libraries/project/state_selection.ml b/src/libraries/project/state_selection.ml
index 1b47451c304629169556911d8dfe05cb382a6880..b24af0f01b80dca77c9a2099ab4ba78a72e6ba22 100644
--- a/src/libraries/project/state_selection.ml
+++ b/src/libraries/project/state_selection.ml
@@ -84,26 +84,6 @@ include Datatype.Make
type t = state_selection
let name = "State_selection"
let reprs = [ full; empty; singleton State.dummy ]
- let internal_pretty_code p_caller fmt (s, _) = match s with
- | Full -> Format.fprintf fmt "@[State_selection.full@]"
- | Subset sel ->
- match Selection.fold_vertex (fun s acc -> s :: acc) sel [] with
- | [] -> Format.fprintf fmt "@[State_selection.empty@]"
- | [ s ] ->
- let pp fmt =
- Format.fprintf fmt "@[<hv 2>State_selection.singleton@;%a@]"
- (State.internal_pretty_code Type.Call)
- s
- in
- Type.par p_caller Type.Call fmt pp
- | l ->
- let module D = Datatype.List(State) in
- let pp fmt =
- Format.fprintf fmt "@[<hv 2>State_selection.of_list@;%a@]"
- (D.internal_pretty_code Type.Call)
- l
- in
- Type.par p_caller Type.Call fmt pp
end)
let transitive_closure next_vertices s =
diff --git a/src/libraries/utils/hptmap.ml b/src/libraries/utils/hptmap.ml
index 2a29fcb5437f90b027183178cc4279b67ca55df2..6a722557d67e9a3fc127bc5cc0249e7da5158051 100644
--- a/src/libraries/utils/hptmap.ml
+++ b/src/libraries/utils/hptmap.ml
@@ -680,9 +680,7 @@ struct
else fun x -> !rehash_ref x
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.pp_fail
let pretty = pretty
- let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
end)
let () = Type.set_ml_name D.ty None
diff --git a/src/libraries/utils/rangemap.ml b/src/libraries/utils/rangemap.ml
index 867f43b8443c24d327c065a841f9373a0b700318..d59ee5c547bb5bcc7fcdf7356b342a92f22340b7 100644
--- a/src/libraries/utils/rangemap.ml
+++ b/src/libraries/utils/rangemap.ml
@@ -533,9 +533,7 @@ module Make(Ord: Datatype.S)(Value: Value) = struct
create l x d r
in aux
- let internal_pretty_code = Datatype.undefined
let pretty = Datatype.undefined
- let varname = Datatype.undefined
let mem_project =
if Ord.mem_project == Datatype.never_any_project &&
Value.mem_project == Datatype.never_any_project then
diff --git a/src/plugins/aorai/aorai_register.ml b/src/plugins/aorai/aorai_register.ml
index e2f73a54e0f0fc7adc6380f3d43fdf63785f96dc..fc14083f9095118082fadeba09c794c68e9da12e 100644
--- a/src/plugins/aorai/aorai_register.ml
+++ b/src/plugins/aorai/aorai_register.ml
@@ -323,7 +323,6 @@ let run =
~plugin:"Aorai"
"run"
(Datatype.func Datatype.unit Datatype.unit)
- ~journalize:true
run
let run, _ =
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index 2fb166151250623148259f3b087a508891f3ef4c..bf0f05f91967628ee7717176885947da9bdd75e2 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -45,10 +45,7 @@ module Aorai_state =
let rehash = Datatype.identity
let compare x y = Datatype.Int.compare x.nums y.nums
let copy = Datatype.identity
- let internal_pretty_code = Datatype.undefined
let pretty fmt x = Format.fprintf fmt "state_%d" x.nums
- let varname _ =
- assert false (* unused while internal_pretty_code is undefined *)
let mem_project = Datatype.never_any_project
end
)
@@ -67,9 +64,7 @@ module Aorai_typed_trans =
let rehash = Datatype.identity
let compare x y = Datatype.Int.compare x.numt y.numt
let copy = Datatype.identity
- let internal_pretty_code = Datatype.undefined
let pretty = Promelaoutput.Typed.print_transition
- let varname _ = assert false
let mem_project = Datatype.never_any_project
end)
@@ -1815,7 +1810,6 @@ module Range = Datatype.Make_with_collections
Bounded(Datatype.Int.copy c1, Cil_datatype.Term.copy c2)
| Unbounded c1 -> Unbounded (Datatype.Int.copy c1)
| Unknown -> Unknown
- let internal_pretty_code _ = Datatype.from_pretty_code
let pretty fmt = function
| Fixed c1 -> Format.fprintf fmt "%d" c1
| Interval (c1,c2) ->
@@ -1825,7 +1819,6 @@ module Range = Datatype.Make_with_collections
Cil_datatype.Term.pretty c2
| Unbounded c1 -> Format.fprintf fmt "[%d..]" c1
| Unknown -> Format.fprintf fmt "[..]"
- let varname _ = "r"
let mem_project = Datatype.never_any_project
end)
diff --git a/src/plugins/callgraph/cg.ml b/src/plugins/callgraph/cg.ml
index 5daf8249498f3ebf1ed13cff9c0a9929fd05e3cb..c1a42ab458a316647efacfecb124afe183f459f2 100644
--- a/src/plugins/callgraph/cg.ml
+++ b/src/plugins/callgraph/cg.ml
@@ -277,16 +277,6 @@ let dump () =
let g = Subgraph.get () in
Options.dump GV.output_graph g
-include Journalize.Make
- (struct
- let name = "Cg"
- let dump = dump
- let compute = compute
- type t = G.t
- let ty = D.ty
- let get = get
- end)
-
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/plugins/callgraph/journalize.ml b/src/plugins/callgraph/journalize.ml
deleted file mode 100644
index 88a8231294d3e528393897852946db9def1501ce..0000000000000000000000000000000000000000
--- a/src/plugins/callgraph/journalize.ml
+++ /dev/null
@@ -1,45 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2022 *)
-(* 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 Make
- (C: sig
- val name: string
- val dump: unit -> unit
- val compute: unit -> unit
- type t
- val ty: t Type.t
- val get: unit -> t
- end) =
-struct
- let name = "Callgraph." ^ C.name
- let unit_unit = Datatype.func Datatype.unit Datatype.unit
- let dump = Journal.register (name ^ ".dump") unit_unit C.dump
- let compute = Journal.register (name ^ ".compute") unit_unit C.compute
- let get =
- Journal.register (name ^ ".get") (Datatype.func Datatype.unit C.ty) C.get
-end
-
-(*
-Local Variables:
-compile-command: "make -C ../.."
-End:
-*)
diff --git a/src/plugins/callgraph/journalize.mli b/src/plugins/callgraph/journalize.mli
deleted file mode 100644
index c1c89a0ff8fdcb700a4a8f41bd3ea6c31c715f95..0000000000000000000000000000000000000000
--- a/src/plugins/callgraph/journalize.mli
+++ /dev/null
@@ -1,44 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2022 *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-(** Journalize the API of a callgraph *)
-
-module Make
- (C: sig
- val name: string
- val dump: unit -> unit
- val compute: unit -> unit
- type t
- val ty: t Type.t
- val get: unit -> t
- end):
-sig
- val dump: unit -> unit
- val compute: unit -> unit
- val get: unit -> C.t
-end
-
-(*
-Local Variables:
-compile-command: "make -C ../.."
-End:
-*)
diff --git a/src/plugins/callgraph/services.ml b/src/plugins/callgraph/services.ml
index c281d5027b21fc09b4e4c04ab20f8337ffd5ab7a..6ff1bb2aa2f462c83e3dadb1b559943c41152dd2 100644
--- a/src/plugins/callgraph/services.ml
+++ b/src/plugins/callgraph/services.ml
@@ -111,16 +111,6 @@ let dump () =
Service_graph.frama_c_display false;
Options.dump S.output_graph sg
-include Journalize.Make
- (struct
- let name = "Services"
- let dump = dump
- let compute = compute
- type t = S.Service_graph.t
- let ty = S.Service_graph.Datatype.ty
- let get = get
- end)
-
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/plugins/callgraph/uses.ml b/src/plugins/callgraph/uses.ml
index 98be81c862733550f75b86003253d1f1c9adc272..a4b6931b84b78193287ac24a94b80af2b5134273 100644
--- a/src/plugins/callgraph/uses.ml
+++ b/src/plugins/callgraph/uses.ml
@@ -79,7 +79,6 @@ let _iter_in_rev_order =
~plugin:Options.name
"iter_in_rev_order"
Datatype.(func (func Kernel_function.ty unit) unit)
- ~journalize:false
iter_in_rev_order
let iter_on_aux iter_dir f kf =
@@ -132,7 +131,6 @@ let _accept_base =
~plugin:Options.name
"accept_base"
Datatype.(func2 Kernel_function.ty Base.ty bool)
- ~journalize:false
(fun kf b -> accept_base ~with_formals:true ~with_locals:true kf b)
let nb_calls () =
diff --git a/src/plugins/constant_propagation/api.ml b/src/plugins/constant_propagation/api.ml
index 58e6e1fad7e4643ee0c661f0671d35671cf417c4..b493138ca518026cddf832ade9121294518784d2 100644
--- a/src/plugins/constant_propagation/api.ml
+++ b/src/plugins/constant_propagation/api.ml
@@ -350,33 +350,21 @@ module Result =
let selection_command_line_option =
State_selection.singleton PropagationParameters.SemanticConstFolding.self
-let journalized_get =
- let get fnames cast_intro =
- Result.memo
- (fun _ ->
- Eva.Analysis.compute ();
- let fresh_project =
- FC_file.create_project_from_visitor
- (PropagationParameters.Project_name.get ())
- (fun prj -> new propagate prj fnames ~cast_intro)
- in
- let ctx = Parameter_state.get_selection_context () in
- let ctx = State_selection.diff ctx selection_command_line_option in
- Project.copy ~selection:ctx fresh_project;
- fresh_project)
- (fnames, cast_intro)
- in
- Journal.register
- "Constant_Propagation.get"
- (Datatype.func2
- Cil_datatype.Fundec.Set.ty
- ~label2:("cast_intro",None)
- Datatype.bool
- Project.ty)
- get
-
(* add labels *)
-let get fnames ~cast_intro = journalized_get fnames cast_intro
+let get fnames ~cast_intro =
+ Result.memo
+ (fun _ ->
+ Eva.Analysis.compute ();
+ let fresh_project =
+ FC_file.create_project_from_visitor
+ (PropagationParameters.Project_name.get ())
+ (fun prj -> new propagate prj fnames ~cast_intro)
+ in
+ let ctx = Parameter_state.get_selection_context () in
+ let ctx = State_selection.diff ctx selection_command_line_option in
+ Project.copy ~selection:ctx fresh_project;
+ fresh_project)
+ (fnames, cast_intro)
(** Constant Propagation *)
@@ -395,15 +383,11 @@ let compute () =
let compute, self =
let name = "Constant_Propagation.compute" in
- let journalized_compute =
- Journal.register name (Datatype.func Datatype.unit Datatype.unit)
- compute
- in
let deps = [ PropagationParameters.SemanticConstFold.self;
PropagationParameters.SemanticConstFolding.self;
Result.self ]
in
- State_builder.apply_once name deps journalized_compute
+ State_builder.apply_once name deps compute
let main () =
let force_semantic_folding =
@@ -411,7 +395,6 @@ let main () =
|| not (Cil_datatype.Fundec.Set.is_empty
(PropagationParameters.SemanticConstFold.get ()))
in
- (* must called the function stored in [Db] for journalisation purpose *)
if force_semantic_folding then compute ()
let () =
diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
index 99645c1fefece09541eeab47ee7f74a0e3412235..7d518f77beeadbf5e13922fef48ee097164f6ec1 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
+++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
@@ -82,7 +82,7 @@ module Pred_or_term =
| PoT_pred p -> Printer.pp_predicate fmt p
| PoT_term t -> Printer.pp_term fmt t
- let varname _ = "pred_or_term"
+
end)
(** [Ext_logic_label] associates a statement to a label when necessary. For
diff --git a/src/plugins/e-acsl/src/main.ml b/src/plugins/e-acsl/src/main.ml
index a050b44b6e0bfb6549cfe4063923a9ce4179c293..949b0a3a927bc9b4404c3514cc904b8d672426c1 100644
--- a/src/plugins/e-acsl/src/main.ml
+++ b/src/plugins/e-acsl/src/main.ml
@@ -92,7 +92,6 @@ let generate_code =
let generate_code =
Dynamic.register
~plugin:"E_ACSL"
- ~journalize:true
"generate_code"
(Datatype.func Datatype.string Project.ty)
generate_code
diff --git a/src/plugins/e-acsl/tests/test_config_dev b/src/plugins/e-acsl/tests/test_config_dev
index 0ce872fd8895a63e08ee03b78a2810b1d85955cf..f2563a6a21328fa04b3b2d0ef5260f2a637d142a 100644
--- a/src/plugins/e-acsl/tests/test_config_dev
+++ b/src/plugins/e-acsl/tests/test_config_dev
@@ -5,7 +5,7 @@ COMMENT: Default options for `e-acsl-gcc.sh`
MACRO: ROOT_EACSL_GCC_MISC_OPTS -q -X --no-assert-print-data
COMMENT: Default options for the frama-c invocation
-MACRO: ROOT_EACSL_GCC_FC_EXTRA -journal-disable -verbose 0
+MACRO: ROOT_EACSL_GCC_FC_EXTRA -verbose 0
PLUGIN: E_ACSL eva,scope,variadic rtegen
diff --git a/src/plugins/from/callwise.ml b/src/plugins/from/callwise.ml
index 0538e56b092f8ab3c20d58f1d2d0d317cc6492d5..4891f63d8760583be27bb554abdaccb5c4690a77 100644
--- a/src/plugins/from/callwise.ml
+++ b/src/plugins/from/callwise.ml
@@ -202,7 +202,6 @@ let force_compute_all_calldeps ()=
(* Registration for call-wise from *)
let () =
Db.register_guarded_compute
- "From.compute_all_calldeps"
Tbl.is_computed
Db.From.compute_all_calldeps
force_compute_all_calldeps;
diff --git a/src/plugins/impact/register.ml b/src/plugins/impact/register.ml
index b78599c9a0505c0da9aea5f58d858b423ca83cd2..6dfc46429bd86b280c90ba5418fb0e552a2314bb 100644
--- a/src/plugins/impact/register.ml
+++ b/src/plugins/impact/register.ml
@@ -148,25 +148,9 @@ let compute_pragmas () =
stmts;
;;
-let compute_pragmas =
- Journal.register
- "Impact.compute_pragmas"
- (Datatype.func Datatype.unit (Datatype.list Stmt.ty))
- compute_pragmas
-
-let from_stmt =
- Journal.register
- "Impact.from_stmt"
- (Datatype.func Stmt.ty (Datatype.list Stmt.ty))
- compute_from_stmt
-
-let from_nodes =
- Journal.register
- "Impact.from_nodes"
- (Datatype.func2 Kernel_function.ty
- (Datatype.list PdgTypes.Node.ty)
- (PdgTypes.NodeSet.ty))
- compute_from_nodes
+let from_stmt = compute_from_stmt
+
+let from_nodes = compute_from_nodes
let main () =
if Options.is_on () then begin
diff --git a/src/plugins/impact/register_gui.ml b/src/plugins/impact/register_gui.ml
index 7bab54731cca8a0cea1b44c18d227f15e00d86c8..5146cb4a509f753a2e4ef66c8eac70c68377cf11 100644
--- a/src/plugins/impact/register_gui.ml
+++ b/src/plugins/impact/register_gui.ml
@@ -203,7 +203,6 @@ let impact_statement =
(Datatype.func
Cil_datatype.Stmt.ty
(Datatype.list Cil_datatype.Stmt.ty)))
- ~journalize:true
impact_statement
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/cwe125.sarif b/src/plugins/markdown-report/tests/sarif/oracle/cwe125.sarif
index 3769a8fc34c9937c920179b4cc011f400febe713..2492553138546f46918a6768c6ba357925416d2d 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/cwe125.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/cwe125.sarif
@@ -16,10 +16,9 @@
"invocations": [
{
"commandLine":
- "frama-c -journal-disable -check -no-autoload-plugins -add-symbolic-path :. -load-module=eva,from,scope,markdown_report cwe125.c -save ./cwe125_parse.sav",
+ "frama-c -check -no-autoload-plugins -add-symbolic-path :. -load-module=eva,from,scope,markdown_report cwe125.c -save ./cwe125_parse.sav",
"arguments": [
- "-journal-disable", "-check", "-no-autoload-plugins",
- "-add-symbolic-path", ":.",
+ "-check", "-no-autoload-plugins", "-add-symbolic-path", ":.",
"-load-module=eva,from,scope,markdown_report", "cwe125.c",
"-save", "./cwe125_parse.sav"
],
@@ -28,10 +27,9 @@
},
{
"commandLine":
- "frama-c -journal-disable -check -no-autoload-plugins -add-symbolic-path :. -load-module=eva,from,scope,markdown_report -load ./cwe125_parse.sav -eva -save ./cwe125_eva.sav",
+ "frama-c -check -no-autoload-plugins -add-symbolic-path :. -load-module=eva,from,scope,markdown_report -load ./cwe125_parse.sav -eva -save ./cwe125_eva.sav",
"arguments": [
- "-journal-disable", "-check", "-no-autoload-plugins",
- "-add-symbolic-path", ":.",
+ "-check", "-no-autoload-plugins", "-add-symbolic-path", ":.",
"-load-module=eva,from,scope,markdown_report", "-load",
"./cwe125_parse.sav", "-eva", "-save", "./cwe125_eva.sav"
],
@@ -40,10 +38,9 @@
},
{
"commandLine":
- "frama-c -journal-disable -check -no-autoload-plugins -add-symbolic-path :. -load-module=eva,from,scope,markdown_report -load ./cwe125_eva.sav -then -mdr-out ./cwe125.sarif -mdr-gen sarif -mdr-no-print-libc -mdr-sarif-deterministic",
+ "frama-c -check -no-autoload-plugins -add-symbolic-path :. -load-module=eva,from,scope,markdown_report -load ./cwe125_eva.sav -then -mdr-out ./cwe125.sarif -mdr-gen sarif -mdr-no-print-libc -mdr-sarif-deterministic",
"arguments": [
- "-journal-disable", "-check", "-no-autoload-plugins",
- "-add-symbolic-path", ":.",
+ "-check", "-no-autoload-plugins", "-add-symbolic-path", ":.",
"-load-module=eva,from,scope,markdown_report", "-load",
"./cwe125_eva.sav", "-then", "-mdr-out", "./cwe125.sarif",
"-mdr-gen", "sarif", "-mdr-no-print-libc",
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif b/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
index 289318d160e25da79dfcb8918643ebccb0bd5b0c..f5cfcd6dea5dc27f0acfa63b9387f2f4b924a661 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
@@ -16,10 +16,9 @@
"invocations": [
{
"commandLine":
- "frama-c -journal-disable -check -no-autoload-plugins -add-symbolic-path :. -load-module=eva,from,scope,markdown_report std_string.c -eva -then -mdr-sarif-deterministic -mdr-gen sarif -mdr-out ./std_string.sarif",
+ "frama-c -check -no-autoload-plugins -add-symbolic-path :. -load-module=eva,from,scope,markdown_report std_string.c -eva -then -mdr-sarif-deterministic -mdr-gen sarif -mdr-out ./std_string.sarif",
"arguments": [
- "-journal-disable", "-check", "-no-autoload-plugins",
- "-add-symbolic-path", ":.",
+ "-check", "-no-autoload-plugins", "-add-symbolic-path", ":.",
"-load-module=eva,from,scope,markdown_report", "std_string.c",
"-eva", "-then", "-mdr-sarif-deterministic", "-mdr-gen", "sarif",
"-mdr-out", "./std_string.sarif"
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif b/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif
index 959696dfba7c771680aa1d287e4cf7e9b4fd3d3f..42708bf75372a88ed5ac6e0dd75257c9dd2f3dd1 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif
@@ -16,10 +16,9 @@
"invocations": [
{
"commandLine":
- "frama-c -journal-disable -check -no-autoload-plugins -add-symbolic-path :. -load-module=eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic libc.c -mdr-out ./with-libc.sarif",
+ "frama-c -check -no-autoload-plugins -add-symbolic-path :. -load-module=eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic libc.c -mdr-out ./with-libc.sarif",
"arguments": [
- "-journal-disable", "-check", "-no-autoload-plugins",
- "-add-symbolic-path", ":.",
+ "-check", "-no-autoload-plugins", "-add-symbolic-path", ":.",
"-load-module=eva,from,scope,markdown_report", "-eva",
"-eva-no-results", "-mdr-gen", "sarif",
"-mdr-sarif-deterministic", "libc.c", "-mdr-out",
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif b/src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif
index 23babca6ce70631edc4076a7a4ee4f1705e533c4..00f3d299424eb204322729e64d0831c86c96458c 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif
@@ -16,10 +16,9 @@
"invocations": [
{
"commandLine":
- "frama-c -journal-disable -check -no-autoload-plugins -add-symbolic-path :. -load-module=eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic libc.c -mdr-no-print-libc -mdr-out ./without-libc.sarif",
+ "frama-c -check -no-autoload-plugins -add-symbolic-path :. -load-module=eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic libc.c -mdr-no-print-libc -mdr-out ./without-libc.sarif",
"arguments": [
- "-journal-disable", "-check", "-no-autoload-plugins",
- "-add-symbolic-path", ":.",
+ "-check", "-no-autoload-plugins", "-add-symbolic-path", ":.",
"-load-module=eva,from,scope,markdown_report", "-eva",
"-eva-no-results", "-mdr-gen", "sarif",
"-mdr-sarif-deterministic", "libc.c", "-mdr-no-print-libc",
diff --git a/src/plugins/metrics/register.ml b/src/plugins/metrics/register.ml
index 349543839aea2274c7a6926dd1a3d0efb93f2af9..92e2daf9f3777637f83fdd884cd6b04a5121ec6c 100644
--- a/src/plugins/metrics/register.ml
+++ b/src/plugins/metrics/register.ml
@@ -32,7 +32,7 @@ let syntactic ?(libc=Metrics_parameters.Libc.get ()) () =
begin
match AstType.get () with
| "cil" -> Metrics_cilast.compute_on_cilast ~libc
- (* Cabs metrics are experimental. unregistered, unjournalized *)
+ (* Cabs metrics are experimental. unregistered *)
| "cabs" -> Metrics_cabs.compute_on_cabs ()
| "acsl" -> Metrics_acsl.dump()
| _ -> assert false (* the possible values are checked by the kernel*)
diff --git a/src/plugins/obfuscator/obfuscator_kind.ml b/src/plugins/obfuscator/obfuscator_kind.ml
index 4cf3258f806d50e1e1d39be7292142a129296d32..92896d1c8af3e71feb2c632c29bc5884c63cf722 100644
--- a/src/plugins/obfuscator/obfuscator_kind.ml
+++ b/src/plugins/obfuscator/obfuscator_kind.ml
@@ -85,8 +85,7 @@ include Datatype.Make_with_collections
let hash (k:k) = Hashtbl.hash k
let equal (k1:k) k2 = k1 = k2
let compare (k1:k) k2 = Stdlib.compare k1 k2
- let varname _ = "k"
- let internal_pretty_code = Datatype.undefined
+
let copy = Datatype.identity
let structural_descr = Structural_descr.t_abstract
let rehash = Datatype.identity
diff --git a/src/plugins/obfuscator/obfuscator_register.ml b/src/plugins/obfuscator/obfuscator_register.ml
index d51b878bd548fe63463c00e4e83a3438860d237f..0361178598aed44a764873c1ce4724a1b2b8d2cb 100644
--- a/src/plugins/obfuscator/obfuscator_register.ml
+++ b/src/plugins/obfuscator/obfuscator_register.ml
@@ -62,7 +62,6 @@ let force_run =
~plugin:"Obfuscator"
"force_run"
(Datatype.func Datatype.unit Datatype.unit)
- ~journalize:true
force_run
let run () =
diff --git a/src/plugins/occurrence/register.ml b/src/plugins/occurrence/register.ml
index a1a465e163fdb4ae82dca62bf0e6246eae3b283c..bd78fc766d3b73356947fd2c133532ad0d8caee1 100644
--- a/src/plugins/occurrence/register.ml
+++ b/src/plugins/occurrence/register.ml
@@ -241,24 +241,8 @@ let print_all () =
let self = Occurrences.self
let get_last_result = Occurrences.get_last_result
-
-let get =
- Journal.register
- "Occurrence.get"
- (Datatype.func
- Varinfo.ty
- (* [JS 2011/04/01] Datatype.list buggy in presence of journalisation.
- See comment in datatype.ml *)
- (*(Datatype.list (Datatype.pair Kinstr.ty Lval.ty))*)
- (let module L = Datatype.List(Occurrence_datatype) in L.ty))
- get
-
-let print_all =
- Journal.register
- "Occurrence.print_all"
- (Datatype.func Datatype.unit Datatype.unit)
- (* pb: print_all should take a formatter as argument *)
- print_all
+let get = get
+let print_all = print_all
(* ************************************************************************** *)
(* Main *)
diff --git a/src/plugins/occurrence/register_gui.ml b/src/plugins/occurrence/register_gui.ml
index dca96b2801708b3d86462a2d10a3c4da18cca3a9..7373045d1acdcbf4c410eabf22cc2e818c463fb5 100644
--- a/src/plugins/occurrence/register_gui.ml
+++ b/src/plugins/occurrence/register_gui.ml
@@ -74,7 +74,6 @@ let filter_accesses l =
let _ignore =
Dynamic.register
~plugin:"Occurrence"
- ~journalize:false
"Enabled.set"
(Datatype.func Datatype.bool Datatype.unit)
Enabled.set
@@ -82,7 +81,6 @@ let _ignore =
let _ignore =
Dynamic.register
~plugin:"Occurrence"
- ~journalize:false
"Enabled.get"
(Datatype.func Datatype.unit Datatype.bool)
Enabled.get
diff --git a/src/plugins/pdg_types/pdgTypes.ml b/src/plugins/pdg_types/pdgTypes.ml
index afbaaced4783c835beed71eb744ce1d972674fdd..0618c1e4bcb34020ea772071d4db3b2d624e8ffa 100644
--- a/src/plugins/pdg_types/pdgTypes.ml
+++ b/src/plugins/pdg_types/pdgTypes.ml
@@ -80,8 +80,6 @@ end
let pretty = print_id
let rehash = Datatype.identity
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
- let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
end)
: Datatype.S_with_collections with type t := t)
diff --git a/src/plugins/print_api/print_interface.ml b/src/plugins/print_api/print_interface.ml
index 51e2949bd621997395bbb3cb64725a1cdb4cb4eb..5e38cda7e38e1aabd56a31996018080b0260388f 100644
--- a/src/plugins/print_api/print_interface.ml
+++ b/src/plugins/print_api/print_interface.ml
@@ -362,7 +362,6 @@ let print =
It takes the path where to create this file as an argument."
~plugin:"Print_api"
"run"
- ~journalize:true
(Datatype.func Datatype.string Datatype.unit)
print
diff --git a/src/plugins/qed/Makefile b/src/plugins/qed/Makefile
index 1e228735cfdbda735e556a1f34cd89d87b909053..873a5f150ab8c404495b75ace852464303a0796c 100644
--- a/src/plugins/qed/Makefile
+++ b/src/plugins/qed/Makefile
@@ -25,10 +25,10 @@
# --------------------------------------------------------------------------
ifndef FRAMAC_SHARE
-FRAMAC_SHARE :=$(shell frama-c -journal-disable -print-path)
+FRAMAC_SHARE :=$(shell frama-c -print-path)
endif
ifndef FRAMAC_LIBDIR
-FRAMAC_LIBDIR :=$(shell frama-c -journal-disable -print-libpath)
+FRAMAC_LIBDIR :=$(shell frama-c -print-libpath)
endif
PLUGIN_DIR ?=.
diff --git a/src/plugins/report/csv.ml b/src/plugins/report/csv.ml
index 2ed83a86b0a0f81a85364ad77bcfccf153d44a4b..f38d3827e8c69d7bf1c2ff430ad7b5e8ee625e6b 100644
--- a/src/plugins/report/csv.ml
+++ b/src/plugins/report/csv.ml
@@ -88,7 +88,6 @@ let output file =
let print_csv =
Dynamic.register
~plugin:"Report"
- ~journalize:true
"print_csv"
(Datatype.func Datatype.string Datatype.unit)
output
diff --git a/src/plugins/report/register.ml b/src/plugins/report/register.ml
index 7c1388c121a55c9a0e105573b52e9022b71dbbc0..50da909d0040d34c73cf47824a9f4cb73bf56159 100644
--- a/src/plugins/report/register.ml
+++ b/src/plugins/report/register.ml
@@ -31,7 +31,6 @@ let print () =
let print =
Dynamic.register
~plugin:"Report"
- ~journalize:true
"print"
(Datatype.func Datatype.unit Datatype.unit)
print
diff --git a/src/plugins/rte/register.ml b/src/plugins/rte/register.ml
index f1bb9f659395303290045c7132f16e4d2d08d656..12af98e3b6dcb4ed74098961dd63be4c80a2e86b 100644
--- a/src/plugins/rte/register.ml
+++ b/src/plugins/rte/register.ml
@@ -56,49 +56,40 @@ let compute () =
Globals.Functions.iter
(fun kf -> if include_function kf then !Db.RteGen.annotate_kf kf)
-
-(* journal utilities *)
-
-let journal_register ?comment is_dyn name ty_arg fctref fct =
- let ty = Datatype.func ty_arg Datatype.unit in
- Db.register (Db.Journalize("RteGen." ^ name, ty)) fctref fct;
- if is_dyn then
- let _ignore =
- Dynamic.register ?comment ~plugin:"RteGen" name ty ~journalize:true fct
- in
- ()
-
-let nojournal_register fctref fct =
- Db.register Db.Journalization_not_required fctref (fun () -> fct)
-
let () =
- journal_register false
- "annotate_kf" Kernel_function.ty Db.RteGen.annotate_kf Visit.annotate;
- journal_register false "compute" Datatype.unit Db.RteGen.compute compute;
- journal_register true
- ~comment:"Generate all RTE annotations in the \
- given function."
- "do_all_rte" Kernel_function.ty Db.RteGen.do_all_rte do_all_rte;
- journal_register false
- ~comment:"Generate all RTE annotations except pre-conditions \
- in the given function."
- "do_rte" Kernel_function.ty Db.RteGen.do_rte do_rte;
+ Db.register Db.RteGen.annotate_kf Visit.annotate;
+ Db.register Db.RteGen.compute compute;
+ Db.register Db.RteGen.do_rte do_rte;
+
+ Db.register Db.RteGen.do_all_rte do_all_rte;
+ let _ignore =
+ Dynamic.register
+ ~comment:"Generate all RTE annotations in the given function."
+ ~plugin:"RteGen"
+ "do_all_rte"
+ (Datatype.func Kernel_function.ty Datatype.unit)
+ do_all_rte
+ in
+
let open Generator in
let open Db.RteGen in
- nojournal_register get_signedOv_status Signed_overflow.accessor;
- nojournal_register get_divMod_status Div_mod.accessor;
- nojournal_register get_initialized_status Initialized.accessor;
- nojournal_register get_signed_downCast_status Signed_downcast.accessor;
- nojournal_register get_memAccess_status Mem_access.accessor;
- nojournal_register get_pointerCall_status Pointer_call.accessor;
- nojournal_register get_unsignedOv_status Unsigned_overflow.accessor;
- nojournal_register get_unsignedDownCast_status Unsigned_downcast.accessor;
- nojournal_register get_pointer_downcast_status Pointer_downcast.accessor;
- nojournal_register get_float_to_int_status Float_to_int.accessor;
- nojournal_register get_finite_float_status Finite_float.accessor;
- nojournal_register get_pointer_value_status Pointer_value.accessor;
- nojournal_register get_bool_value_status Bool_value.accessor ;
- nojournal_register get_all_status all_statuses;
+ let register_getter fctref fct =
+ Db.register fctref (fun () -> fct)
+ in
+ register_getter get_signedOv_status Signed_overflow.accessor;
+ register_getter get_divMod_status Div_mod.accessor;
+ register_getter get_initialized_status Initialized.accessor;
+ register_getter get_signed_downCast_status Signed_downcast.accessor;
+ register_getter get_memAccess_status Mem_access.accessor;
+ register_getter get_pointerCall_status Pointer_call.accessor;
+ register_getter get_unsignedOv_status Unsigned_overflow.accessor;
+ register_getter get_unsignedDownCast_status Unsigned_downcast.accessor;
+ register_getter get_pointer_downcast_status Pointer_downcast.accessor;
+ register_getter get_float_to_int_status Float_to_int.accessor;
+ register_getter get_finite_float_status Finite_float.accessor;
+ register_getter get_pointer_value_status Pointer_value.accessor;
+ register_getter get_bool_value_status Bool_value.accessor ;
+ register_getter get_all_status all_statuses;
;;
(* dynamic registration *)
@@ -109,7 +100,6 @@ let _ =
~plugin:"RteGen"
"emitter"
Emitter.ty
- ~journalize:false
Generator.emitter
(* retrieve list of generated rte annotations for a given stmt *)
@@ -122,7 +112,6 @@ let _ignore =
(Datatype.func
Cil_datatype.Stmt.ty
(let module L = Datatype.List(Cil_datatype.Code_annotation) in L.ty))
- ~journalize:true
Generator.get_registered_annotations
let _ignore =
@@ -133,7 +122,6 @@ let _ignore =
"stmt_annotations"
(Datatype.func2 Kernel_function.ty Cil_datatype.Stmt.ty
(let module L = Datatype.List(Cil_datatype.Code_annotation) in L.ty))
- ~journalize:false
Visit.get_annotations_stmt
let _ignore =
@@ -144,7 +132,6 @@ let _ignore =
"exp_annotations"
(Datatype.func3 Kernel_function.ty Cil_datatype.Stmt.ty Cil_datatype.Exp.ty
(let module L = Datatype.List(Cil_datatype.Code_annotation) in L.ty))
- ~journalize:false
Visit.get_annotations_exp
let _ignore =
@@ -153,7 +140,6 @@ let _ignore =
~plugin:"RteGen"
"all_statuses"
Datatype.(list (triple string (func2 kf bool unit) (func kf bool)))
- ~journalize:false
Generator.all_statuses
let main () =
diff --git a/src/plugins/scope/datascope.ml b/src/plugins/scope/datascope.ml
index 479ed60f40766d58b89b0f80a9f57b1c5ef50e40..571263696fd43639f7b508b5d6aef3f0785c5230 100644
--- a/src/plugins/scope/datascope.ml
+++ b/src/plugins/scope/datascope.ml
@@ -639,48 +639,9 @@ let rm_asserts () =
CA_Map.iter aux to_be_removed
end
-let get_data_scope_at_stmt =
- Journal.register
- "Scope.Datascope.get_data_scope_at_stmt"
- (Datatype.func3
- Kernel_function.ty
- Cil_datatype.Stmt.ty
- Cil_datatype.Lval.ty
- (Datatype.pair
- Cil_datatype.Stmt.Hptset.ty
- (Datatype.pair Cil_datatype.Stmt.Hptset.ty
- Cil_datatype.Stmt.Hptset.ty)))
- get_data_scope_at_stmt
-
-let get_prop_scope_at_stmt =
- Journal.register
- "Scope.Datascope.get_prop_scope_at_stmt"
- (Datatype.func3
- Kernel_function.ty
- Cil_datatype.Stmt.ty
- Cil_datatype.Code_annotation.ty
- (Datatype.pair
- (Cil_datatype.Stmt.Hptset.ty)
- (Datatype.list Cil_datatype.Code_annotation.ty)))
- get_prop_scope_at_stmt
-
-let check_asserts =
- Journal.register
- "Scope.Datascope.check_asserts"
- (Datatype.func Datatype.unit (Datatype.list Cil_datatype.Code_annotation.ty))
- check_asserts
-
-let rm_asserts =
- Journal.register
- "Scope.Datascope.rm_asserts"
- (Datatype.func Datatype.unit Datatype.unit)
- rm_asserts
let () =
- Db.register
- (Db.Journalize
- ("Value.rm_asserts", Datatype.func Datatype.unit Datatype.unit))
- Db.Value.rm_asserts rm_asserts
+ Db.register Db.Value.rm_asserts rm_asserts
let rm_asserts =
Dynamic.register
@@ -688,7 +649,6 @@ let rm_asserts =
~plugin:name
"rm_asserts"
Datatype.(func unit unit)
- ~journalize:true
rm_asserts
(*
diff --git a/src/plugins/scope/defs.ml b/src/plugins/scope/defs.ml
index 5011918f24e5533ee5c2c2a578eb6ec135e7aab0..2e7fbdbdf8694c5424314143013f4681865576b5 100644
--- a/src/plugins/scope/defs.ml
+++ b/src/plugins/scope/defs.ml
@@ -225,22 +225,6 @@ let compute_with_def_type kf stmt lval =
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
-module D = Datatype.Option
- (Datatype.Pair(Stmt.Hptset)(Datatype.Option(Locations.Zone)))
-
-module DT = Datatype.Option
- (Datatype.Pair
- (Stmt.Map.Make(Datatype.Pair(Datatype.Bool)(Datatype.Bool)))
- (Datatype.Option(Locations.Zone)))
-
-let get_defs =
- Journal.register
- "Scope.Defs.get_defs"
- (Datatype.func3 Kernel_function.ty Stmt.ty Lval.ty (D.ty))
- compute
-
-let get_defs_with_type =
- Journal.register
- "Scope.Defs.get_defs_with_type"
- (Datatype.func3 Kernel_function.ty Stmt.ty Lval.ty (DT.ty))
- compute_with_def_type
+let get_defs = compute
+
+let get_defs_with_type = compute_with_def_type
diff --git a/src/plugins/security_slicing/components.ml b/src/plugins/security_slicing/components.ml
index 7786adf110e9fb15a44296b8944471e838fee245..629fa05f3835588deac0848a4d24514a7f93b89f 100644
--- a/src/plugins/security_slicing/components.ml
+++ b/src/plugins/security_slicing/components.ml
@@ -734,7 +734,6 @@ end
let register name arg =
Dynamic.register
- ~journalize:true
~plugin:"Security_slicing"
name
(Datatype.func Stmt.ty (Datatype.list Stmt.ty))
@@ -752,7 +751,6 @@ let impact_analysis =
Dynamic.register
~plugin:"Security_slicing"
"impact_analysis"
- ~journalize:true
(Datatype.func2 Kernel_function.ty Stmt.ty (Datatype.list Stmt.ty))
(Component.forward Component.Impact)
@@ -841,7 +839,6 @@ let () =
let get_component =
Dynamic.register
- ~journalize:true
"Security.get_component"
(Datatype.func Kernel_type.stmt (Datatype.list Kernel_type.stmt))
(fun s -> compute (); Components.find s)
@@ -880,7 +877,6 @@ let slice ctrl =
let slice =
Dynamic.register
"Security_slicing.slice"
- ~journalize:true
(Datatype.func Datatype.bool Project.ty)
slice
*)
diff --git a/src/plugins/slicing/Slicing.mli b/src/plugins/slicing/Slicing.mli
old mode 100644
new mode 100755
index 3b17ef709fdb50f3f6dc147f12c5f42151d6542f..1751112ca3dacd3a63e01d2f1598308c41fdc705
--- a/src/plugins/slicing/Slicing.mli
+++ b/src/plugins/slicing/Slicing.mli
@@ -109,7 +109,7 @@ module Api:sig
type t
val dyn_t : t Type.t
- (** For dynamic type checking and journalization. *)
+ (** For dynamic type checking. *)
val make : data:bool -> addr:bool -> ctrl:bool -> t
(** To construct a mark such as
@@ -165,13 +165,13 @@ module Api:sig
(** Internal selection. *)
val dyn_t : t Type.t
- (** For dynamic type checking and journalization. *)
+ (** For dynamic type checking. *)
type set
(** Set of colored selections. *)
val dyn_set : set Type.t
- (** For dynamic type checking and journalization. *)
+ (** For dynamic type checking. *)
(** {3 Journalized selectors} *)
@@ -264,8 +264,6 @@ module Api:sig
kernel_function -> set)
(** To select the annotations related to a function. *)
- (** {3 Selectors that are not journalized} *)
-
val select_func_zone :
(set -> Mark.t -> Locations.Zone.t -> kernel_function -> set)
(** To select an output zone related to a function. *)
@@ -306,7 +304,7 @@ module Api:sig
- mark the node with a spare_mark and propagate so that
the dependencies that were not selected yet will be marked spare. *)
- (** {3 Not for casual users and not journalized} *)
+ (** {3 Not for casual users} *)
val get_function : t -> kernel_function
(** May be used to get the function related to an internal selection. *)
@@ -410,7 +408,7 @@ module Api:sig
(** Abstract data type for function slice. *)
val dyn_t : t Type.t
- (** For dynamic type checking and journalization. *)
+ (** For dynamic type checking. *)
val create : kernel_function -> t
(** Used to get an empty slice (nothing selected) related to a
@@ -497,7 +495,7 @@ module Api:sig
val add_persistent_cmdline : unit -> unit
(** Add persistent selection from the command line. *)
- (** {3 Not for casual users and not journalized} *)
+ (** {3 Not for casual users} *)
val add_slice_selection_internal:Slice.t -> Select.t -> unit
(** May be used to add a selection request for a function slice
diff --git a/src/plugins/slicing/api.ml b/src/plugins/slicing/api.ml
index 4f188601176098412d2a35e81ffbae854fbc8c2e..bdc35b91066fc7c4fca741519f497a7dfdd21702 100644
--- a/src/plugins/slicing/api.ml
+++ b/src/plugins/slicing/api.ml
@@ -21,7 +21,6 @@
(**************************************************************************)
open Cil_types
-open Cil_datatype
(* ---------------------------------------------------------------------- *)
(** Global data management *)
@@ -45,24 +44,12 @@ let self = SlicingState.self
(* ---------------------------------------------------------------------- *)
-(** {2 Functions with journalized side effects } *)
-
let set_modes calls callers sliceUndef keepAnnotations () =
SlicingParameters.Mode.Calls.set calls ;
SlicingParameters.Mode.Callers.set callers ;
SlicingParameters.Mode.SliceUndef.set sliceUndef;
SlicingParameters.Mode.KeepAnnotations.set keepAnnotations
-let set_modes =
- Journal.register "Slicing.Api.set_modes"
- (Datatype.func4
- ~label1:("calls", None) Datatype.int
- ~label2:("callers", None) Datatype.bool
- ~label3:("sliceUndef", None) Datatype.bool
- ~label4:("keepAnnotations", None) Datatype.bool
- (Datatype.func
- Datatype.unit
- Datatype.unit))
- set_modes
+
let set_modes ?(calls=SlicingParameters.Mode.Calls.get ())
?(callers=SlicingParameters.Mode.Callers.get ())
?(sliceUndef=SlicingParameters.Mode.SliceUndef.get ())
@@ -78,49 +65,16 @@ module Project = struct
(** {2 Values } *)
let default_slice_names = SlicingTransform.default_slice_names
- let () =
- Journal.Binding.add
- (Datatype.func3
- Kernel_function.ty Datatype.bool Datatype.int Datatype.string)
- default_slice_names
- "Slicing.Api.Project.default_slice_names"
-
- (** {2 Functions with journalized side effects } *)
-
- let reset_slicing = Journal.register "Slicing.Api.Project.reset_slicing"
- (Datatype.func Datatype.unit Datatype.unit)
- SlicingState.reset_slicing
-
- let extract f_slice_names = SlicingTransform.extract ~f_slice_names
- let extract = Journal.register "Slicing.Api.Project.extract"
- (Datatype.func2
- ~label1:("f_slice_names",
- Some (fun () -> default_slice_names))
- (Datatype.func3
- Kernel_function.ty Datatype.bool Datatype.int Datatype.string)
- Datatype.string
- Project.ty)
- extract
+
+ let reset_slicing = SlicingState.reset_slicing
+
let extract ?(f_slice_names=default_slice_names) new_proj_name =
- extract f_slice_names new_proj_name
-
- let print_dot = PrintSlice.build_dot_project
- let print_dot = Journal.register "Slicing.Api.Project.print_dot"
- (Datatype.func2
- ~label1:("filename", None) Datatype.string
- ~label2:("title", None) Datatype.string
- Datatype.unit)
- print_dot
+ SlicingTransform.extract ~f_slice_names new_proj_name
+
let print_dot ~filename ~title =
- print_dot filename title
+ PrintSlice.build_dot_project filename title
- let change_slicing_level =
- Journal.register "Slicing.Api.Project.change_slicing_level"
- (Datatype.func2
- Kernel_function.ty
- Datatype.int
- Datatype.unit)
- SlicingMacros.change_slicing_level
+ let change_slicing_level = SlicingMacros.change_slicing_level
(** {2 No needs of Journalization} *)
@@ -162,195 +116,15 @@ module Select = struct
type t = SlicingTypes.sl_select
let dyn_t = SlicingTypes.Sl_select.ty
- type set = SlicingCmds.set
+
module S = Cil_datatype.Varinfo.Map.Make(SlicingTypes.Fct_user_crit)
let dyn_set = S.ty
- (** {2 Journalized selectors } *)
-
- let empty_selects = Journal.register
- "Slicing.Api.Select.empty_selects"
- dyn_set
- Cil_datatype.Varinfo.Map.empty
-
- let select_stmt set spare = SlicingCmds.select_stmt set ~spare
- let select_stmt = Journal.register "Slicing.Api.Select.select_stmt"
- (Datatype.func4
- dyn_set
- ~label2:("spare", None) Datatype.bool
- Stmt.ty
- Kernel_function.ty
- dyn_set)
- select_stmt
- let select_stmt set ~spare =
- select_stmt set spare
-
- let select_stmt_ctrl set spare = SlicingCmds.select_stmt_ctrl set ~spare
- let select_stmt_ctrl = Journal.register "Slicing.Api.Select.select_stmt_ctrl"
- (Datatype.func4
- dyn_set
- ~label2:("spare", None) Datatype.bool
- Stmt.ty
- Kernel_function.ty
- dyn_set)
- select_stmt_ctrl
- let select_stmt_ctrl set ~spare =
- select_stmt_ctrl set spare
-
- let select_stmt_lval_rw set mark rd wr stmt eval =
- SlicingCmds.select_stmt_lval_rw set mark ~rd ~wr stmt ~eval
- let select_stmt_lval_rw = Journal.register
- "Slicing.ApiSelect.select_stmt_lval_rw"
- (Datatype.func4
- dyn_set
- SlicingTypes.dyn_sl_mark
- ~label3:("rd", None) Datatype.String.Set.ty
- ~label4:("wr", None) Datatype.String.Set.ty
- (Datatype.func3
- Stmt.ty
- ~label2:("eval", None) Stmt.ty
- Kernel_function.ty
- dyn_set))
- select_stmt_lval_rw
- let select_stmt_lval_rw set mark ~rd ~wr stmt ~eval =
- select_stmt_lval_rw set mark rd wr stmt eval
-
- let select_stmt_lval set mark lval before stmt eval =
- SlicingCmds.select_stmt_lval set mark lval ~before stmt ~eval
- let select_stmt_lval = Journal.register "Slicing.Api.Select.select_stmt_lval"
- (Datatype.func4
- dyn_set
- Mark.dyn_t
- Datatype.String.Set.ty
- ~label4:("before", None) Datatype.bool
- (Datatype.func3
- Stmt.ty
- ~label2:("eval", None) Stmt.ty
- Kernel_function.ty
- dyn_set))
- select_stmt_lval
- let select_stmt_lval set mark lval ~before stmt ~eval =
- select_stmt_lval set mark lval before stmt eval
-
- let select_stmt_annots set mark spare threat user_assert slicing_pragma loop_inv loop_var =
- SlicingCmds.select_stmt_annots set mark ~spare ~threat ~user_assert ~slicing_pragma ~loop_inv ~loop_var
- let select_stmt_annots = Journal.register
- "Slicing.Api.Select.select_stmt_annots"
- (Datatype.func4
- dyn_set
- Mark.dyn_t
- ~label3:("spare", None) Datatype.bool
- ~label4:("threat", None) Datatype.bool
- (Datatype.func4
- ~label1:("user_assert", None) Datatype.bool
- ~label2:("slicing_pragma", None) Datatype.bool
- ~label3:("loop_inv", None) Datatype.bool
- ~label4:("loop_var", None) Datatype.bool
- (Datatype.func2
- Stmt.ty
- Kernel_function.ty
- dyn_set)))
- select_stmt_annots
- let select_stmt_annots set mark ~spare ~threat ~user_assert ~slicing_pragma ~loop_inv ~loop_var =
- select_stmt_annots set mark spare threat user_assert slicing_pragma loop_inv loop_var
-
- let select_func_lval = Journal.register "Slicing.Api.Select.select_func_lval"
- (Datatype.func4
- dyn_set
- Mark.dyn_t
- Datatype.String.Set.ty
- Kernel_function.ty
- dyn_set)
- SlicingCmds.select_func_lval
-
- let select_func_lval_rw set mark rd wr eval =
- SlicingCmds.select_func_lval_rw set mark ~rd ~wr ~eval
- let select_func_lval_rw = Journal.register
- "Slicing.Api.Select.select_func_lval_rw"
- (Datatype.func4
- dyn_set
- Mark.dyn_t
- ~label3:("rd", None) Datatype.String.Set.ty
- ~label4:("wr", None) Datatype.String.Set.ty
- (Datatype.func2
- ~label1:("eval", None) Stmt.ty
- Kernel_function.ty
- dyn_set))
- select_func_lval_rw
- let select_func_lval_rw set mark ~rd ~wr ~eval =
- select_func_lval_rw set mark rd wr eval
-
- let select_func_return set spare =
- SlicingCmds.select_func_return set ~spare
- let select_func_return = Journal.register
- "Slicing.Api.Select.select_func_return"
- (Datatype.func3
- dyn_set
- ~label2:("spare", None) Datatype.bool
- Kernel_function.ty
- dyn_set)
- select_func_return
- let select_func_return set ~spare = select_func_return set spare
-
- let select_func_calls_to set spare =
- SlicingCmds.select_func_calls_to set ~spare
- let select_func_calls_to = Journal.register
- "Slicing.Api.Select.select_func_calls_to"
- (Datatype.func3
- dyn_set
- ~label2:("spare", None) Datatype.bool
- Kernel_function.ty
- dyn_set)
- select_func_calls_to
- let select_func_calls_to set ~spare =
- select_func_calls_to set spare
-
- let select_func_calls_into set spare =
- SlicingCmds.select_func_calls_into set ~spare
- let select_func_calls_into = Journal.register
- "Slicing.Api.Select.select_func_calls_into"
- (Datatype.func3
- dyn_set
- ~label2:("spare", None) Datatype.bool
- Kernel_function.ty
- dyn_set)
- select_func_calls_into
- let select_func_calls_into set ~spare =
- select_func_calls_into set spare
-
- let select_func_annots set mark spare threat user_assert slicing_pragma loop_inv loop_var =
- SlicingCmds.select_func_annots set mark ~spare ~threat ~user_assert ~slicing_pragma ~loop_inv ~loop_var
- let select_func_annots = Journal.register
- "Slicing.Api.Select.select_func_annots"
- (Datatype.func4
- dyn_set
- Mark.dyn_t
- ~label3:("spare", None) Datatype.bool
- ~label4:("threat", None) Datatype.bool
- (Datatype.func4
- ~label1:("user_assert", None) Datatype.bool
- ~label2:("slicing_pragma", None) Datatype.bool
- ~label3:("loop_inv", None) Datatype.bool
- ~label4:("loop_var", None) Datatype.bool
- (Datatype.func Kernel_function.ty dyn_set)))
- select_func_annots
- let select_func_annots set mark ~spare ~threat ~user_assert ~slicing_pragma ~loop_inv ~loop_var =
- select_func_annots set mark spare threat user_assert slicing_pragma loop_inv loop_var
-
- (** {2 No Journalization} *)
-
- let select_func_zone = SlicingCmds.select_func_zone
- let select_stmt_term = SlicingCmds.select_stmt_term
- let select_stmt_pred = SlicingCmds.select_stmt_pred
- let select_stmt_annot = SlicingCmds.select_stmt_annot
- let select_stmt_zone = SlicingCmds.select_stmt_zone
-
- let select_pdg_nodes = SlicingCmds.select_pdg_nodes
-
- (** {2 No Journalization} *)
-
- let get_function = SlicingCmds.get_select_kf
- let merge_internal = SlicingSelect.merge_db_select
+ let empty_selects = Cil_datatype.Varinfo.Map.empty
+
+ include SlicingCmds
+ let get_function = get_select_kf
+ let merge_internal = SlicingSelect.merge_db_select
let add_to_selects_internal = SlicingSelect.Selections.add_to_selects
let iter_selects_internal = SlicingSelect.Selections.iter_selects_internal
let fold_selects_internal = SlicingSelect.Selections.fold_selects_internal
@@ -381,22 +155,14 @@ module Slice = struct
type t = SlicingTypes.sl_fct_slice
let dyn_t = SlicingTypes.dyn_sl_fct_slice
- (** {2 Functions with journalized side effects } *)
-
let create =
- Journal.register "Slicing.Api.Slice.create"
- (Datatype.func Kernel_function.ty dyn_t)
- SlicingProject.create_slice
+ SlicingProject.create_slice
let remove =
- Journal.register "Slicing.Api.Slice.remove"
- (Datatype.func dyn_t Datatype.unit)
- SlicingProject.remove_ff
+ SlicingProject.remove_ff
let remove_uncalled =
- Journal.register "Slicing.Api.Slice.remove_uncalled"
- (Datatype.func Datatype.unit Datatype.unit)
- SlicingProject.remove_uncalled_slices
+ SlicingProject.remove_uncalled_slices
(** {2 No needs of Journalization} *)
@@ -454,108 +220,50 @@ end
(** {1 Slicing request} *)
module Request = struct
- (** {2 Functions with journalized side effects } *)
-
let apply_all propagate_to_callers =
SlicingCmds.apply_all ~propagate_to_callers
- let apply_all = Journal.register "Slicing.Api.Request.apply_all"
- (Datatype.func
- ~label:("propagate_to_callers", None) Datatype.bool
- Datatype.unit)
- apply_all
let apply_all ~propagate_to_callers =
apply_all propagate_to_callers
let apply_all_internal =
- Journal.register "Slicing.Api.Request.apply_all_internal"
- (Datatype.func Datatype.unit Datatype.unit)
- SlicingCmds.apply_all_actions
+ SlicingCmds.apply_all_actions
let apply_next_internal =
- Journal.register "Slicing.Api.Request.apply_next_internal"
- (Datatype.func Datatype.unit Datatype.unit)
- SlicingCmds.apply_next_action
+ SlicingCmds.apply_next_action
let propagate_user_marks =
- Journal.register "Slicing.Api.Request.propagate_user_marks"
- (Datatype.func Datatype.unit Datatype.unit)
- SlicingCmds.topologic_propagation
-
- let copy_slice = Journal.register "Slicing.Api.Request.copy_slice"
- (Datatype.func
- Slice.dyn_t
- Slice.dyn_t)
- copy_slice
-
- let split_slice = Journal.register "Slicing.Api.Request.split_slice"
- (Datatype.func
- Slice.dyn_t
- (Datatype.list Slice.dyn_t))
- split_slice
-
- let merge_slices ff_1 ff_2 replace =
- merge_slices ff_1 ff_2 ~replace
- let merge_slices = Journal.register "Slicing.Api.Request.merge_slices"
- (Datatype.func3
- Slice.dyn_t
- Slice.dyn_t
- ~label3:("replace", None) Datatype.bool
- Slice.dyn_t)
- merge_slices
+ SlicingCmds.topologic_propagation
+
+ let copy_slice = copy_slice
+
+ let split_slice = split_slice
+
let merge_slices ff_1 ff_2 ~replace =
- merge_slices ff_1 ff_2 replace
+ merge_slices ff_1 ff_2 ~replace
let add_call_slice caller to_call =
SlicingSelect.call_ff_in_caller ~caller ~to_call
- let add_call_slice =
- Journal.register "Slicing.Api.Request.add_call_slice"
- (Datatype.func2
- ~label1:("caller", None) Slice.dyn_t
- ~label2:("to_call", None) Slice.dyn_t
- Datatype.unit)
- add_call_slice
let add_call_slice ~caller ~to_call =
add_call_slice caller to_call
let add_call_fun caller to_call =
SlicingSelect.call_fsrc_in_caller ~caller ~to_call
- let add_call_fun =
- Journal.register "Slicing.Api.Request.add_call_fun"
- (Datatype.func2
- ~label1:("caller", None) Slice.dyn_t
- ~label2:("to_call", None) Kernel_function.ty
- Datatype.unit)
- add_call_fun
let add_call_fun ~caller ~to_call =
add_call_fun caller to_call
let add_call_min_fun caller to_call =
SlicingSelect.call_min_f_in_caller ~caller ~to_call
- let add_call_min_fun =
- Journal.register "Slicing.Api.Request.add_call_min_fun"
- (Datatype.func2
- ~label1:("caller", None) Slice.dyn_t
- ~label2:("to_call", None) Kernel_function.ty
- Datatype.unit)
- add_call_min_fun
let add_call_min_fun ~caller ~to_call =
add_call_min_fun caller to_call
- let add_selection = Journal.register "Slicing.Request.add_selection"
- (Datatype.func
- Select.dyn_set Datatype.unit)
- SlicingCmds.add_selection
+ let add_selection =
+ SlicingCmds.add_selection
let add_persistent_selection =
- Journal.register "Slicing.Request.add_persistent_selection"
- (Datatype.func
- Select.dyn_set Datatype.unit)
- SlicingCmds.add_persistent_selection
+ SlicingCmds.add_persistent_selection
let add_persistent_cmdline =
- Journal.register "Slicing.Request.add_persistent_cmdline"
- (Datatype.func Datatype.unit Datatype.unit)
- SlicingCmds.add_persistent_cmdline
+ SlicingCmds.add_persistent_cmdline
(** {2 No needs of Journalization} *)
diff --git a/src/plugins/slicing/api.mli b/src/plugins/slicing/api.mli
index b489bb90605a8bc465dc42b3ac37f82ca83ed428..2a0af61952fbb5e2b4ef8ed5550aed059a351773 100644
--- a/src/plugins/slicing/api.mli
+++ b/src/plugins/slicing/api.mli
@@ -28,8 +28,6 @@ val self : State.t
(* ---------------------------------------------------------------------- *)
-(** {2 Functions with journalized side effects } *)
-
(** Set the used slicing modes. *)
val set_modes :
?calls:SlicingParameters.Mode.Calls.t ->
@@ -42,8 +40,6 @@ val set_modes :
(** {1 Slicing project management.} *)
module Project : sig
- (** {2 Functions with journalized side effects } *)
-
(** Init/reset a slicing project. *)
val reset_slicing : unit -> unit
@@ -102,7 +98,7 @@ module Mark : sig
(** Abstract data type for mark value. *)
type t = SlicingTypes.sl_mark
- (** For dynamic type checking and journalization. *)
+ (** For dynamic type checking. *)
val dyn_t : t Type.t
(** {2 No needs of Journalization} *)
@@ -158,13 +154,13 @@ module Select : sig
(** Internal selection. *)
type t = SlicingTypes.sl_select
- (** For dynamic type checking and journalization. *)
+ (** For dynamic type checking. *)
val dyn_t : t Type.t
(** Set of colored selections. *)
type set = SlicingCmds.set
- (** For dynamic type checking and journalization. *)
+ (** For dynamic type checking. *)
val dyn_set : set Type.t
(** {2 Selectors.} *)
@@ -429,8 +425,6 @@ module Slice : sig
type t = SlicingTypes.sl_fct_slice
val dyn_t : t Type.t
- (** {2 Functions with journalized side effects } *)
-
val create : Cil_types.kernel_function -> t
val remove : t -> unit
@@ -474,8 +468,6 @@ end
(** {1 Slicing request} *)
module Request : sig
- (** {2 Functions with journalized side effects } *)
-
val apply_all : propagate_to_callers:bool -> unit
val apply_all_internal : unit -> unit
diff --git a/src/plugins/slicing/slicingInternals.ml b/src/plugins/slicing/slicingInternals.ml
index 849167e818a6e85c001f7a2a84a342583d24898c..4169f6937d3d208c157d24e958faf9d96b4aea93 100644
--- a/src/plugins/slicing/slicingInternals.ml
+++ b/src/plugins/slicing/slicingInternals.ml
@@ -206,7 +206,7 @@ and criterion =
(** {2 Internals values} *)
-(** {3 For the journalization of these internals types} *)
+(** {3 For the datatypes of these internals types} *)
let dummy_pdg_mark = {m1 = Spare ; m2 = Spare }
(** The whole project. *)
diff --git a/src/plugins/slicing/slicingInternals.mli b/src/plugins/slicing/slicingInternals.mli
index e7e9074c4f76f3f46dde2de8ee60591b0164c680..0e6dc51a49ccfd353bbe3d0e3c6729e68a48eb96 100644
--- a/src/plugins/slicing/slicingInternals.mli
+++ b/src/plugins/slicing/slicingInternals.mli
@@ -194,7 +194,7 @@ and criterion =
(** {2 Internals values} *)
-(** {3 For the journalization of these internals types} *)
+(** {3 For the datatypes of these internals types} *)
val dummy_pdg_mark : pdg_mark
diff --git a/src/plugins/slicing/slicingTypes.ml b/src/plugins/slicing/slicingTypes.ml
index f7aec3942446d5c1085b06b1c40b82f132023dbb..343d08a8f13a70053957f7cbb3de2133a0394a8c 100644
--- a/src/plugins/slicing/slicingTypes.ml
+++ b/src/plugins/slicing/slicingTypes.ml
@@ -65,7 +65,6 @@ module Fct_user_crit =
let reprs = [ SlicingInternals.dummy_fct_user_crit ]
let name = "SlicingTypes.Fct_user_crit"
let mem_project = Datatype.never_any_project
- let varname _ = "user_criteria"
end)
(** Function slice *)
@@ -74,8 +73,6 @@ type sl_fct_slice = SlicingInternals.fct_slice
(** Marks : used to put 'colors' in the result *)
type sl_mark = SlicingInternals.pdg_mark
-(** {3 For the journalization of values of these types} *)
-
let pp_sl_project p_caller fmt _p =
let pp fmt =
Format.fprintf fmt
@@ -90,8 +87,6 @@ module Sl_project =
type t = sl_project
let reprs = [ SlicingInternals.dummy_project ]
let name = "SlicingTypes.Sl_project"
- let internal_pretty_code = pp_sl_project
- let varname _s = "sl_project_"
let mem_project = Datatype.never_any_project
end)
@@ -105,7 +100,6 @@ module Sl_select =
(fun v -> v, SlicingInternals.dummy_fct_user_crit)
Cil_datatype.Varinfo.reprs
let name = "SlicingTypes.Sl_select"
- let varname _s = "sl_select"
let mem_project = Datatype.never_any_project
end)
@@ -113,7 +107,7 @@ let pp_sl_fct_slice p_caller fmt ff =
let pp fmt =
Format.fprintf fmt
"@[<hv 2>!Db.Slicing.Slice.from_num_id@;%a@;%d@]"
- (Kernel_function.internal_pretty_code Type.Call)
+ Kernel_function.pretty
ff.SlicingInternals.ff_fct.SlicingInternals.fi_kf
ff.SlicingInternals.ff_id
in
@@ -127,13 +121,12 @@ module Sl_fct_slice =
type t = fct_slice
let name = "SlicingTypes.Sl_fct_slice"
let reprs = [ dummy_fct_slice ]
- let internal_pretty_code = pp_sl_fct_slice
let mem_project = Datatype.never_any_project
end)
let dyn_sl_fct_slice = Sl_fct_slice.ty
-let pp_sl_mark p fmt m =
+let pp_sl_mark fmt m =
let pp = match m.SlicingInternals.m1, m.SlicingInternals.m2 with
| SlicingInternals.Spare, _ -> None
| _, SlicingInternals.Spare -> None
@@ -163,7 +156,7 @@ let pp_sl_mark p fmt m =
fun fmt ->
Format.fprintf fmt "@[<hv 2>SlicingInternals.create_sl_mark@;~m1:%a@;~m2:%a@]"
pp m.SlicingInternals.m1 pp m.SlicingInternals.m2
- in Type.par p Type.Call fmt pp
+ in pp fmt
module Sl_mark =
Datatype.Make_with_collections
@@ -177,10 +170,8 @@ module Sl_mark =
let hash = Hashtbl.hash
let copy = Datatype.undefined
let rehash = Datatype.undefined
- let internal_pretty_code = pp_sl_mark
- let pretty = Datatype.from_pretty_code
+ let pretty = pp_sl_mark
let mem_project = Datatype.never_any_project
- let varname = Datatype.undefined
end)
let dyn_sl_mark = Sl_mark.ty
diff --git a/src/plugins/slicing/slicingTypes.mli b/src/plugins/slicing/slicingTypes.mli
index fa1b7086ea0894379223e283aeebab93f1db5a51..9f8fd66d1779e3fd1b53de195a08b4b7eef5171f 100644
--- a/src/plugins/slicing/slicingTypes.mli
+++ b/src/plugins/slicing/slicingTypes.mli
@@ -65,8 +65,6 @@ type sl_fct_slice = SlicingInternals.fct_slice
(** Marks : used to put 'colors' in the result *)
type sl_mark = SlicingInternals.pdg_mark
-(** {3 For the journalization of values of these types} *)
-
val pp_sl_project : Type.precedence -> Format.formatter -> 'a -> unit
module Sl_project : Datatype.S with type t = sl_project
@@ -80,9 +78,6 @@ module Sl_fct_slice : Datatype.S with type t = SlicingInternals.fct_slice
val dyn_sl_fct_slice : Sl_fct_slice.t Type.t
-val pp_sl_mark :
- Type.precedence -> Format.formatter -> SlicingInternals.pdg_mark -> unit
-
module Sl_mark : Datatype.S_with_collections with
type t = SlicingInternals.pdg_mark
diff --git a/src/plugins/sparecode/register.ml b/src/plugins/sparecode/register.ml
index f446712652869570f8f842ce390501f68b4e551d..b684d758b6bc1fcc216d63385568821a4f334c92 100644
--- a/src/plugins/sparecode/register.ml
+++ b/src/plugins/sparecode/register.ml
@@ -49,28 +49,16 @@ module P = Sparecode_params
(** {2 State_builder} *)
-let unjournalized_rm_unused_globals new_proj_name project =
- P.feedback "remove unused global declarations from project '%s'"
- (Project.get_name project);
- P.result "removed unused global declarations in new project '%s'" new_proj_name;
- Project.on project Globs.rm_unused_decl new_proj_name
-
-let journalized_rm_unused_globals =
- Journal.register
- "Sparecode.Register.rm_unused_globals"
- (Datatype.func2
- ~label1:("new_proj_name", None) Datatype.string
- ~label2:("project", Some Project.current) Project.ty
- Project.ty)
- unjournalized_rm_unused_globals
-
let rm_unused_globals ?new_proj_name ?(project=Project.current ()) () =
let new_proj_name =
match new_proj_name with
| Some name -> name
| None -> (Project.get_name project)^ " (without unused globals)"
in
- journalized_rm_unused_globals new_proj_name project
+ P.feedback "remove unused global declarations from project '%s'"
+ (Project.get_name project);
+ P.result "removed unused global declarations in new project '%s'" new_proj_name;
+ Project.on project Globs.rm_unused_decl new_proj_name
let run select_annot select_slice_pragma =
P.feedback "remove unused code...";
@@ -93,21 +81,10 @@ let run select_annot select_slice_pragma =
Project.copy ~selection:ctx new_prj;
new_prj
-let journalized_get =
- Journal.register
- "Sparecode.Register.get"
- (Datatype.func2
- ~label1:("select_annot", None) Datatype.bool
- ~label2:("select_slice_pragma", None) Datatype.bool
- Project.ty)
- (fun select_annot select_slice_pragma ->
- Result.memo
- (fun _ -> run select_annot select_slice_pragma)
- (select_annot, select_slice_pragma))
-
-(* add labels *)
let get ~select_annot ~select_slice_pragma =
- journalized_get select_annot select_slice_pragma
+ Result.memo
+ (fun _ -> run select_annot select_slice_pragma)
+ (select_annot, select_slice_pragma)
let main () =
if Sparecode_params.Analysis.get () then begin
diff --git a/src/plugins/users/users_register.ml b/src/plugins/users/users_register.ml
index 40f1eb7c2d98cca4f390ac3296444570ecbc268d..08352196ad61bedfaea29ad2190ac501cd69f6ba 100644
--- a/src/plugins/users/users_register.ml
+++ b/src/plugins/users/users_register.ml
@@ -93,12 +93,6 @@ let get kf =
find kf
end
-let get =
- Journal.register
- "Users.get"
- (Datatype.func Kernel_function.ty Kernel_function.Hptset.ty)
- get
-
let print () =
if ForceUsers.get () then
result "@[<v>====== DISPLAYING USERS ======@ %t\
diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml
index 11e429d42db8d613075e2221437624747db08395..2b63e58b9f02008b7c7a865bc8a44dc2e540140a 100644
--- a/src/plugins/value/engine/analysis.ml
+++ b/src/plugins/value/engine/analysis.ml
@@ -226,8 +226,7 @@ let compute () =
let compute =
let name = "Eva.Analysis.compute" in
- let f = Journal.register name Datatype.(func unit unit) compute in
- fst (State_builder.apply_once name [ Self.state ] f)
+ fst (State_builder.apply_once name [ Self.state ] compute)
(* Resets the Analyzer when the current project is changed. *)
let () =
diff --git a/src/plugins/value/gui_files/gui_callstacks_filters.ml b/src/plugins/value/gui_files/gui_callstacks_filters.ml
index 6c8486e8d674f3c033bfd079851c29d30addff7c..2da98a86a74e4e4591ccf43ac50cbd9df9ca3047 100644
--- a/src/plugins/value/gui_files/gui_callstacks_filters.ml
+++ b/src/plugins/value/gui_files/gui_callstacks_filters.ml
@@ -137,13 +137,13 @@ let () =
~comment:"Evaluation of a l-value on the callstacks focused in the GUI"
~plugin:"Value" "lval_to_zone_gui"
(Datatype.func2 Stmt.ty Lval.ty Locations.Zone.ty)
- ~journalize:false lval_to_zone_gui
+ lval_to_zone_gui
in
let _eval_tlv =
Dynamic.register
~comment:"Evaluation of a term, supposed to be a location, on the callstacks focused in the GUI"
~plugin:"Value" "tlval_to_zone_gui"
(Datatype.func2 Stmt.ty Term.ty Locations.Zone.ty)
- ~journalize:false tlval_to_zone_gui
+ tlval_to_zone_gui
in
()
diff --git a/src/plugins/value/partitioning/split_strategy.ml b/src/plugins/value/partitioning/split_strategy.ml
index 33b8e743fd5d16fa920731f70e1ad17d317a23be..7c3c134055a3c6764fedab223454580c58a04802 100644
--- a/src/plugins/value/partitioning/split_strategy.ml
+++ b/src/plugins/value/partitioning/split_strategy.ml
@@ -57,7 +57,6 @@ include
| SplitEqList l ->
List.fold_left (fun acc i -> acc * 13 + 57 * Int.hash i) 1 l
let copy = Datatype.identity
- let internal_pretty_code = Datatype.undefined
let pretty fmt = function
| NoSplit -> Format.pp_print_string fmt "no split"
| SplitAuto -> Format.pp_print_string fmt "auto split"
@@ -65,7 +64,6 @@ include
| SplitEqList l ->
Format.fprintf fmt "Split on \\result == %a"
(Pretty_utils.pp_list ~sep:",@ " Datatype.Integer.pretty) l
- let varname _ = "v"
let mem_project = Datatype.never_any_project
end)
diff --git a/src/plugins/value/values/offsm_value.ml b/src/plugins/value/values/offsm_value.ml
index 51399e2b4ac008502951e6f7ef380ed865846fab..556c2f74059fbd23cd95678c3ce0c285aa348d3a 100644
--- a/src/plugins/value/values/offsm_value.ml
+++ b/src/plugins/value/values/offsm_value.ml
@@ -372,11 +372,9 @@ module Datatype_Offsm_or_top = Datatype.Make_with_collections(struct
| Top -> 7895
| O o -> V_Offsetmap.hash o
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt = function
| Top -> Format.pp_print_string fmt "TopO"
| O o -> Format.fprintf fmt "O @[%a@]" V_Offsetmap.pretty o
- let varname _ = "o"
let mem_project = Datatype.never_any_project
end)
diff --git a/src/plugins/value_types/cvalue.ml b/src/plugins/value_types/cvalue.ml
index 61fc238db742832bc5ad2a2a42e13f2acd0cfbb8..81499fcb019d20eff6a1d509133411602f532993 100644
--- a/src/plugins/value_types/cvalue.ml
+++ b/src/plugins/value_types/cvalue.ml
@@ -857,8 +857,6 @@ module V_Or_Uninitialized = struct
let copy = Datatype.undefined
let rehash = Datatype.identity
let pretty = pretty
- let internal_pretty_code = Datatype.undefined
- let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
end)
: Datatype.S with type t := t)
diff --git a/src/plugins/value_types/function_Froms.ml b/src/plugins/value_types/function_Froms.ml
index dae6e569a3daee127b6787b0e120a77e630df317..f2399b16e49b2c03ed9cde711e01d1c173531187 100644
--- a/src/plugins/value_types/function_Froms.ml
+++ b/src/plugins/value_types/function_Froms.ml
@@ -57,9 +57,7 @@ struct
let rehash = Datatype.identity
let mem_project = Datatype.never_any_project
- let varname _ = "da"
- let internal_pretty_code = Datatype.undefined
let copy = Datatype.undefined
end)
@@ -178,9 +176,7 @@ module DepsOrUnassigned = struct
let rehash = Datatype.identity
let mem_project = Datatype.never_any_project
- let varname _ = "d"
- let internal_pretty_code = Datatype.undefined
let copy = Datatype.undefined
end)
@@ -625,10 +621,8 @@ include Datatype.Make
let compare = Datatype.undefined
let equal = equal
let pretty = pretty
- let internal_pretty_code = Datatype.undefined
let rehash = Datatype.identity
let copy = Datatype.undefined
- let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
end)
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 7869f466d863f94344ca26fb4337f80d7d76551e..da36a8c6b302de96b3695ce9f8473d2c74616e21 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -682,9 +682,7 @@ struct
let compare = Datatype.undefined
let hash = Datatype.undefined
let copy _old = QZERO.create ()
- let varname = Datatype.undefined
let pretty = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let mem_project _ _ = false
end)
diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index 8a6ede3e75a66dd8af63d1a1a707833f5b853c3c..8aca9f47467408d9c852a8a268ae2b120c872d07 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -582,10 +582,7 @@ module C_object = Datatype.Make(struct
let copy = Datatype.Undefined.copy
- let internal_pretty_code = Datatype.Undefined.internal_pretty_code
let mem_project = Datatype.Undefined.mem_project
-
- let varname _ = "co"
end)
let rec compare_ptr_conflated a b =
diff --git a/src/plugins/wp/tests/wp/wp_call_pre.c b/src/plugins/wp/tests/wp/wp_call_pre.c
index 857b5f629686bc3537b9b3eb40c6692caae44d76..be7bf59d67146f3d3d65471808eca4672969106a 100644
--- a/src/plugins/wp/tests/wp/wp_call_pre.c
+++ b/src/plugins/wp/tests/wp/wp_call_pre.c
@@ -6,7 +6,7 @@ OPT: -wp-model Hoare -wp-no-simpl -wp-fct double_call
*/
/* run.config_qualif
-OPT: -journal-disable -wp -wp-par 1
+OPT: -wp -wp-par 1
*/
int G = 3;
diff --git a/src/plugins/wp/tests/wp/wp_strategy.c b/src/plugins/wp/tests/wp/wp_strategy.c
index 258fd478c999f79a898eb2077da01abdc6ee063a..d7e6a4845b0fe23c8bfc8154f30b84e718bf7dcf 100644
--- a/src/plugins/wp/tests/wp/wp_strategy.c
+++ b/src/plugins/wp/tests/wp/wp_strategy.c
@@ -1,10 +1,10 @@
/* run.config
-OPT: -journal-disable -wp-model Hoare -wp-verbose 2
-OPT: -journal-disable -wp-model Typed -wp-verbose 2 -wp-prop @assigns
+OPT: -wp-model Hoare -wp-verbose 2
+OPT: -wp-model Typed -wp-verbose 2 -wp-prop @assigns
*/
/* run.config_qualif
-OPT: -journal-disable -rte -wp -wp-model Hoare -wp-par 1 -wp-msg-key shell
+OPT: -rte -wp -wp-model Hoare -wp-par 1 -wp-msg-key shell
*/
/*----------------------------------------------------------------------------*/
diff --git a/src/plugins/wp/tests/wp_acsl/struct_use_case.i b/src/plugins/wp/tests/wp_acsl/struct_use_case.i
index e9839c540db66f3c0f415e8d452163fbcbbee579..2707e0e0d25fd6cfac29632876df3613e6698d11 100644
--- a/src/plugins/wp/tests/wp_acsl/struct_use_case.i
+++ b/src/plugins/wp/tests/wp_acsl/struct_use_case.i
@@ -3,8 +3,8 @@
*/
/* run.config_qualif
-OPT: -journal-disable -wp -wp-model Caveat -wp-par 1 -wp-prop="-ko"
-OPT: -journal-disable -wp -wp-model Caveat -wp-par 1 -wp-prop ko -wp-steps 50
+OPT: -wp -wp-model Caveat -wp-par 1 -wp-prop="-ko"
+OPT: -wp -wp-model Caveat -wp-par 1 -wp-prop ko -wp-steps 50
*/
/* run.config_qed
@@ -18,7 +18,7 @@ struct {
/*@ ensures ko: var == { \old(var) \with .b[1] = x } ;
@ ensures ok: var == { \old(var) \with .b[1] = x, .b[0] = y } ;
- @*/
+ @*/
void f(unsigned int x, unsigned int y){
var.b[0] = y;
var.b[1] = x;
@@ -26,7 +26,7 @@ void f(unsigned int x, unsigned int y){
/*@ ensures ko: var == { \old(var) \with .b[1] = x } ;
@ ensures ok: var == { \old(var) \with .b[1] = x, .a = y } ;
- @*/
+ @*/
void g(unsigned int x, unsigned int y){
var.a = y;
var.b[1] = x;
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index b11a73f320de7ae2c6d42da2e0ea491449ab13d0..605913c9317af03cb1621fb32ea8176ab259f1f0 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -260,10 +260,8 @@ module PropIdRaw =
let copy = Datatype.undefined
let rehash = Datatype.identity
- let internal_pretty_code = Datatype.undefined
let pretty = Datatype.undefined
let mem_project = Datatype.never_any_project
- let varname = Datatype.undefined
end)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index fbc6df714458fb2357f53853a004f26b9a58f82c..9d50a7ad9f4a4d2982aea40ca6a65d596b1a2b55 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -490,13 +490,13 @@ let () = Type.set_ml_name ResultType.ty (Some "Wpo.result")
let get_gid =
Dynamic.register
- ~plugin:"Wp" "Wpo.get_gid" ~journalize:false
+ ~plugin:"Wp" "Wpo.get_gid"
(Datatype.func WpoType.ty Datatype.string)
(fun g -> g.po_gid)
let get_property =
Dynamic.register
- ~plugin:"Wp" "Wpo.get_property" ~journalize:false
+ ~plugin:"Wp" "Wpo.get_property"
(Datatype.func WpoType.ty Property.ty)
(fun g -> WpPropId.property_of_id g.po_pid)
@@ -827,12 +827,12 @@ let is_passed g =
is_proved g
let get_result =
- Dynamic.register ~plugin:"Wp" "Wpo.get_result" ~journalize:false
+ Dynamic.register ~plugin:"Wp" "Wpo.get_result"
(Datatype.func2 WpoType.ty ProverType.ty ResultType.ty)
get_result
let is_valid =
- Dynamic.register ~plugin:"Wp" "Wpo.is_valid" ~journalize:false
+ Dynamic.register ~plugin:"Wp" "Wpo.is_valid"
(Datatype.func ResultType.ty Datatype.bool) VCS.is_valid
(* -------------------------------------------------------------------------- *)
@@ -920,7 +920,6 @@ let iter ?ip ?index ?on_axiomatics ?on_behavior ?on_goal () =
let iter_on_goals =
Dynamic.register ~plugin:"Wp" "Wpo.iter_on_goals"
(Datatype.func (Datatype.func WpoType.ty Datatype.unit) Datatype.unit)
- ~journalize:true
(fun on_goal -> iter ~on_goal ())
let goals_of_property prop =
@@ -934,11 +933,10 @@ let goals_of_property prop =
let goals_of_property =
Dynamic.register ~plugin:"Wp" "Wpo.goals_of_property"
(Datatype.func Property.ty (Datatype.list WpoType.ty))
- ~journalize:false
goals_of_property
let prover_of_name =
- Dynamic.register ~plugin:"Wp" "Wpo.prover_of_name" ~journalize:false
+ Dynamic.register ~plugin:"Wp" "Wpo.prover_of_name"
(Datatype.func Datatype.string (Datatype.option ProverType.ty))
VCS.parse_prover
@@ -953,7 +951,7 @@ let get_logfile w prover result =
DISK.cache_log ~pid:w.po_pid ~model ~prover ~result
let _ignore =
- Dynamic.register ~plugin:"Wp" "Wpo.file_for_log_proof" ~journalize:false
+ Dynamic.register ~plugin:"Wp" "Wpo.file_for_log_proof"
(Datatype.func2
WpoType.ty ProverType.ty
(Datatype.pair Datatype.string Datatype.string))
diff --git a/tests/dynamic/abstract.ml b/tests/dynamic/abstract.ml
index 9d1b774785f80359788fd30cf123071c66ad49dd..54a14984bb33114aa4d2d04a2f500c3fc8ddb40a 100644
--- a/tests/dynamic/abstract.ml
+++ b/tests/dynamic/abstract.ml
@@ -8,7 +8,7 @@ module A : sig end = struct
let mk () = 1.05
let _ = B false
let f = function A n -> n | B false -> min_int | B true -> max_int
- module T =
+ module T =
Datatype.Make(struct
type t = tt
let name = "A.t"
@@ -16,7 +16,7 @@ module A : sig end = struct
include Datatype.Undefined
end)
let t = T.ty
- module U =
+ module U =
Datatype.Make(struct
type t = float
let name = "A.u"
@@ -25,42 +25,42 @@ module A : sig end = struct
end)
let u = U.ty
let mk =
- Dynamic.register ~plugin:"A" ~journalize:false "mk"
+ Dynamic.register ~plugin:"A" "mk"
(Datatype.func Datatype.unit u)
mk
let _ =
- Dynamic.register ~plugin:"A" ~journalize:false "f"
+ Dynamic.register ~plugin:"A" "f"
(Datatype.func t Datatype.int)
f
let _ =
- Dynamic.register ~plugin:"A" ~journalize:false "g"
+ Dynamic.register ~plugin:"A" "g"
(Datatype.func u Datatype.int)
(fun x -> Format.printf "%f@." x; int_of_float x)
- let v1 = Dynamic.register ~plugin:"A" ~journalize:false "v1" t (A 1)
- let _ = Dynamic.register ~plugin:"A" ~journalize:false "v2" t (A 2)
+ let v1 = Dynamic.register ~plugin:"A" "v1" t (A 1)
+ let _ = Dynamic.register ~plugin:"A" "v2" t (A 2)
let _ =
- Dynamic.register ~plugin:"A" ~journalize:false "h"
+ Dynamic.register ~plugin:"A" "h"
(Datatype.func t (Datatype.func u Datatype.bool))
(fun x y ->
match x with A x ->
Format.printf "params = %d %f@." x y;
x = int_of_float y | B _ -> false)
let _ =
- Dynamic.register ~plugin:"A" ~journalize:false "succ"
+ Dynamic.register ~plugin:"A" "succ"
(Datatype.func Datatype.int Datatype.int) succ
let _ =
- Dynamic.register ~journalize:false "ho" ~plugin:"A"
+ Dynamic.register "ho" ~plugin:"A"
(Datatype.func (Datatype.func Datatype.int Datatype.int) (Datatype.func t u))
(fun ff x -> float (ff (f x)))
let _ =
- Dynamic.register ~journalize:false ~plugin:"A" "ppu" (Datatype.func u Datatype.unit)
+ Dynamic.register ~plugin:"A" "ppu" (Datatype.func u Datatype.unit)
(fun f -> Format.printf "ppu %f@." f)
let ho2 =
- Dynamic.register ~plugin:"A" "ho2" ~journalize:false
+ Dynamic.register ~plugin:"A" "ho2"
(Datatype.func (Datatype.func t Datatype.int) (Datatype.func t u))
(fun f x -> float (f x))
- let _ =
+ let _ =
ignore (Dynamic.get ~plugin:"A" "mk" (Datatype.func Datatype.unit u) ())
module UA = Type.Abstract(struct let name = "A.u" end)
@@ -68,11 +68,11 @@ module A : sig end = struct
Dynamic.get ~plugin:"A" "mk" (Datatype.func Datatype.unit UA.ty) ()
let _ =
- Dynamic.register ~journalize:false ~plugin:"A" "poly"
+ Dynamic.register ~plugin:"A" "poly"
(Datatype.list u) [ 1.; 2.; 3. ]
let _ =
- Dynamic.register ~journalize:false ~plugin:"A" "poly2" (Datatype.list u)
+ Dynamic.register ~plugin:"A" "poly2" (Datatype.list u)
[ mk (); ho2 (function A n -> n | B _ -> min_int) v1; ho2 f v1 ]
end
@@ -132,4 +132,3 @@ module B = struct
(Dynamic.get ~plugin:"A" "ppu" (Datatype.func ty' Datatype.unit))
(Dynamic.get ~plugin:"A" "poly2" (Datatype.list ty'))
end
-
diff --git a/tests/dynamic/abstract2.ml b/tests/dynamic/abstract2.ml
index ac9898d9235f8c7bbdfb762d3c818f792c21c078..461f2dfbfc15096526e514857aafdddc475ee34a 100644
--- a/tests/dynamic/abstract2.ml
+++ b/tests/dynamic/abstract2.ml
@@ -4,7 +4,7 @@ module AA : sig end = struct
let ty =
Type.register ~name:"AA.t" ~ml_name:None Structural_descr.t_unknown [ "" ]
let _mk =
- Dynamic.register ~plugin:"AA" ~journalize:false "mk"
+ Dynamic.register ~plugin:"AA" "mk"
(Datatype.func Datatype.unit ty)
(fun () -> "a")
end
@@ -14,7 +14,7 @@ module BB : sig end = struct
let ty =
Type.register ~name:"BB.t" ~ml_name:None Structural_descr.t_unknown [ 1.0 ]
let _print =
- Dynamic.register ~plugin:"BB" ~journalize:false "print"
+ Dynamic.register ~plugin:"BB" "print"
(Datatype.func ty Datatype.unit)
print_float
end
@@ -25,9 +25,9 @@ let main () =
let module B = Type.Abstract(struct let name = "BB.t" end) in
let _b = B.ty in
let _s = Dynamic.get ~plugin:"AA" "mk" (Datatype.func Datatype.unit a) () in
- (* is now statically checked and no more dynamically *)
+ (* is now statically checked and no more dynamically *)
(* Dynamic.get ~plugin:"BB" "print" (Datatype.func b Datatype.unit) s;*)
()
-
+
let () = Db.Main.extend main
diff --git a/tests/journal/abstract_cpt.ml b/tests/journal/abstract_cpt.ml
deleted file mode 100644
index 5fa827630f94eaf5dbe1f35e9b81d3248fa3640f..0000000000000000000000000000000000000000
--- a/tests/journal/abstract_cpt.ml
+++ /dev/null
@@ -1,33 +0,0 @@
-let mk () = ref 0
-let incr c = incr c; !c
-
-include Datatype.Make(struct
- (* order of lines below does matter *)
- include Datatype.Serializable_undefined
- include Datatype.Ref(Datatype.Int)
- let varname _ = "cpt"
- let name = "Abstract_cpt.t"
-end)
-
-let mk =
- Dynamic.register
- ~journalize:true
- ~plugin:"Abstract_cpt"
- "mk"
- (Datatype.func Datatype.unit ty) mk
-
-let incr =
- Dynamic.register
- ~journalize:true
- ~plugin:"Abstract_cpt"
- "incr"
- (Datatype.func ty Datatype.int)
- incr
-
-let pretty =
- Dynamic.register
- ~journalize:true
- ~plugin:"Abstract_cpt"
- "pretty"
- (Datatype.func ty Datatype.unit)
- (fun n -> Format.printf "%d@." !n)
diff --git a/tests/journal/control.i b/tests/journal/control.i
deleted file mode 100644
index ec7902161dda42107bb8d9219dca2ccd293a1079..0000000000000000000000000000000000000000
--- a/tests/journal/control.i
+++ /dev/null
@@ -1,29 +0,0 @@
-/* run.config
- COMMENT: the following CMD redefinition omits adding @PTEST_FILE@ on purpose (due to -load)
- CMD: @frama-c@ @PTEST_OPTIONS@
- COMMENT: do not compare generated journals since they depend on current time
- PLUGIN: @EVA_PLUGINS@
- EXECNOW: BIN control_journal.ml @frama-c@ @PTEST_FILE@ -journal-enable -eva -deps -out @EVA_OPTIONS@ -main f -journal-name @PTEST_RESULT@/control_journal.ml > @DEV_NULL@ 2> @DEV_NULL@
- SCRIPT: @PTEST_RESULT@/control_journal.ml
- OPT:
- MODULE:
- SCRIPT: @PTEST_RESULT@/control_journal_bis.ml
- EXECNOW: BIN control_journal_bis.ml cp %{dep:@PTEST_RESULT@/control_journal.ml} @PTEST_RESULT@/control_journal_bis.ml > @DEV_NULL@ 2> @DEV_NULL@
- OPT: -calldeps
- MODULE: abstract_cpt use_cpt
- SCRIPT:
- EXECNOW: BIN abstract_cpt_journal.ml @frama-c@ -journal-enable -journal-name @PTEST_RESULT@/abstract_cpt_journal.ml > @DEV_NULL@ 2> @DEV_NULL@
- SCRIPT: @PTEST_RESULT@/abstract_cpt_journal.ml
- OPT:
-*/
-
-int x,y,c,d;
-
-void f() {
- int i;
- for(i=0; i<4 ; i++) {
- if (c) { if (d) {y++;} else {x++;}}
- else {};
- x=x+1;
- }
-}
diff --git a/tests/journal/control2.c b/tests/journal/control2.c
deleted file mode 100644
index 9570c6dd3afb3e59c787a9f04594244b196b4e0c..0000000000000000000000000000000000000000
--- a/tests/journal/control2.c
+++ /dev/null
@@ -1,19 +0,0 @@
-/* run.config
- COMMENT: the following CMD redefinition omits adding @PTEST_FILE@ on purpose (due to -load)
- CMD: @frama-c@ @PTEST_OPTIONS@
- PLUGIN: @EVA_PLUGINS@
- EXECNOW: BIN control_journal2.ml @frama-c@ -journal-enable -eva -deps -out -main f -journal-name @PTEST_RESULT@/control_journal2.ml @PTEST_FILE@ > @DEV_NULL@ 2> @DEV_NULL@
- SCRIPT: @PTEST_RESULT@/control_journal2.ml
- EXECNOW: LOG control2_sav.res LOG control2_sav.err BIN control_journal_next2.ml @frama-c@ -journal-enable -lib-entry -journal-name @PTEST_RESULT@/control_journal_next2.ml @PTEST_FILE@ > @PTEST_RESULT@/control2_sav.res 2> @PTEST_RESULT@/control2_sav.err
- SCRIPT: @PTEST_RESULT@/control_journal_next2.ml
- OPT:
-*/
-int x,y,c,d;
-void f() {
- int i;
- for(i=0; i<4 ; i++) {
- if (c) { if (d) {y++;} else {x++;}}
- else {};
- x=x+1;
- }
-}
diff --git a/tests/journal/intra.i b/tests/journal/intra.i
deleted file mode 100644
index 5ae163e21ff0267076ad57e04d8ddcfc17e1bc2e..0000000000000000000000000000000000000000
--- a/tests/journal/intra.i
+++ /dev/null
@@ -1,119 +0,0 @@
-/* run.config
- COMMENT: the following CMD redefinition omits adding @PTEST_FILE@ on purpose (due to -load)
- CMD: @frama-c@ @PTEST_OPTIONS@
- PLUGIN: @EVA_PLUGINS@ sparecode
- MODULE: @PTEST_NAME@
- EXECNOW: BIN intra_journal.ml @frama-c@ -eva-show-progress -journal-enable -journal-name @PTEST_RESULT@/intra_journal.ml @PTEST_FILE@ > @DEV_NULL@ 2> @DEV_NULL@
- SCRIPT: @PTEST_RESULT@/intra_journal.ml
- OPT:
-*/
-
-/* Waiting for results such as:
- * spare code analysis removes statements having variables with
- * prefix "spare_"
- *
- * slicing analysis removes statement having variables with
- * prefix "spare_" and "any_"
- */
-int G;
-
-int tmp (int a) {
- int x = a;
- //@ assert x == a ;
- int w = 1;
- //@ assert w == 1 ; // w is not spare or else
- // the assertion should be removed !
- int spare_z = 1;
- int spare_y = a+spare_z;
- return x;
-}
-
-int param (int a, int spare_b) {
- return a;
-}
-
-int spare_called_fct (int a) {
- return a;
-}
-
-int two_outputs (int a, int b) {
- G += b;
- return a;
-}
-
-int call_two_outputs (void) {
- int x, spare_y;
- int any_b = 1;
- int any_a = 2;
- int a = 1;
- int b = any_b;
- x = two_outputs (a, b);
- G = 1; /* don't use b = any_b; */
- b = 2;
- a = any_a;
- spare_y = two_outputs (a, b);
- /* don't use spare_y so don't use a = any_a */
- return x;
-}
-
-void assign (int *p, int *q) {
- *p = *q ;
-}
-
-int loop (int x, int y, int z) {
- int i = 0;
- //@ assert i < z ;
- //@ loop invariant i < y ;
- /* should keep y in sparecode analysis even if it is not used in the function */
- while (i < x) {
- i ++;
- }
- return i;
-}
-
-void stop(void) __attribute__ ((noreturn)) ;
-
-int main (int noreturn, int halt) {
- int res = 0;
- int spare_tmp = 3;
- int spare_param = 2 + spare_tmp;
- int spare_ref = 3;
- int x = 1;
- int y = 2;
- res += param (2, spare_param);
- res += tmp (4);
- spare_called_fct (5);
- res += call_two_outputs ();
- res += loop (10, 15, 20);
- assign (&x, &spare_ref) ; /* <- Here, best can be done for spare analysis */
- assign (&x, &y) ;
- if (noreturn) {
- if (halt)
- stop () ;
- else
- while (1);
- //@ assert \false ; // What should be done with
- // assertions related to dead code?
- }
-
- return res + G + x;
-}
-
-/*-------------------------------------*/
-struct { struct { int x; int y; } a; int b; } X10;
-int Y10;
-int f10 (int x) {
- //@ slice pragma expr X10;
- //@ slice pragma expr X10.a;
- //@ slice pragma expr X10.a.x;
- //@ slice pragma expr Y10;
- //@ assert X10.a.x >= 0;
- return x;
-}
-int main2 () {
- Y10 = 0;
- X10.b = 0;
- X10.a.y += f10 (3);
- return X10.a.x + X10.a.y;
-}
-/*-------------------------------------*/
diff --git a/tests/journal/intra.ml b/tests/journal/intra.ml
deleted file mode 100644
index 0962a71402273c161496fe0885c0c5879589ef9d..0000000000000000000000000000000000000000
--- a/tests/journal/intra.ml
+++ /dev/null
@@ -1,4 +0,0 @@
-let () =
- Db.Main.extend (fun _ ->
- ignore (Sparecode.Register.get ~select_annot:true
- ~select_slice_pragma:true))
diff --git a/tests/journal/oracle/control.0.res.oracle b/tests/journal/oracle/control.0.res.oracle
deleted file mode 100644
index 8191206632c5a2badf8b201659e3bc09e88640bc..0000000000000000000000000000000000000000
--- a/tests/journal/oracle/control.0.res.oracle
+++ /dev/null
@@ -1,38 +0,0 @@
-[kernel] Parsing control.i (no preprocessing)
-[eva] Analyzing a complete application starting at f
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- x ∈ {0}
- y ∈ {0}
- c ∈ {0}
- d ∈ {0}
-[eva] control.i:24: starting to merge loop iterations
-[eva:alarm] control.i:27: Warning: signed overflow. assert x + 1 ≤ 2147483647;
-[eva] Recording results for f
-[eva] done for function f
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function f:
- x ∈ [0..2147483647]
- i ∈ {4}
-[eva:summary] ====== ANALYSIS SUMMARY ======
- ----------------------------------------------------------------------------
- 1 function analyzed (out of 1): 100% coverage.
- In this function, 9 statements reached (out of 12): 75% coverage.
- ----------------------------------------------------------------------------
- No errors or warnings raised during the analysis.
- ----------------------------------------------------------------------------
- 1 alarm generated by the analysis:
- 1 integer overflow
- ----------------------------------------------------------------------------
- No logical properties have been reached by the analysis.
- ----------------------------------------------------------------------------
-[from] Computing for function f
-[from] Done for function f
-[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
-[from] Function f:
- x FROM x (and SELF)
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function f:
- x; i
diff --git a/tests/journal/oracle/control.1.res.oracle b/tests/journal/oracle/control.1.res.oracle
deleted file mode 100644
index ae023e8b8226ac8ac7a2e86a190dc09f5e2bcd72..0000000000000000000000000000000000000000
--- a/tests/journal/oracle/control.1.res.oracle
+++ /dev/null
@@ -1,71 +0,0 @@
-[kernel] Parsing control.i (no preprocessing)
-[eva] Analyzing a complete application starting at f
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- x ∈ {0}
- y ∈ {0}
- c ∈ {0}
- d ∈ {0}
-[eva] control.i:24: starting to merge loop iterations
-[eva:alarm] control.i:27: Warning: signed overflow. assert x + 1 ≤ 2147483647;
-[eva] Recording results for f
-[eva] done for function f
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function f:
- x ∈ [0..2147483647]
- i ∈ {4}
-[eva:summary] ====== ANALYSIS SUMMARY ======
- ----------------------------------------------------------------------------
- 1 function analyzed (out of 1): 100% coverage.
- In this function, 9 statements reached (out of 12): 75% coverage.
- ----------------------------------------------------------------------------
- No errors or warnings raised during the analysis.
- ----------------------------------------------------------------------------
- 1 alarm generated by the analysis:
- 1 integer overflow
- ----------------------------------------------------------------------------
- No logical properties have been reached by the analysis.
- ----------------------------------------------------------------------------
-[from] Computing for function f
-[from] Done for function f
-[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
-[from] Function f:
- x FROM x (and SELF)
-[from] ====== END OF DEPENDENCIES ======
-[eva] Analyzing a complete application starting at f
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- x ∈ {0}
- y ∈ {0}
- c ∈ {0}
- d ∈ {0}
-[eva:alarm] control.i:27: Warning: signed overflow. assert x + 1 ≤ 2147483647;
-[eva] Recording results for f
-[from] Computing for function f
-[from] Done for function f
-[eva] done for function f
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function f:
- x ∈ [0..2147483647]
- i ∈ {4}
-[eva:summary] ====== ANALYSIS SUMMARY ======
- ----------------------------------------------------------------------------
- 1 function analyzed (out of 1): 100% coverage.
- In this function, 9 statements reached (out of 12): 75% coverage.
- ----------------------------------------------------------------------------
- No errors or warnings raised during the analysis.
- ----------------------------------------------------------------------------
- 1 alarm generated by the analysis:
- 1 integer overflow
- ----------------------------------------------------------------------------
- No logical properties have been reached by the analysis.
- ----------------------------------------------------------------------------
-[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
-[from] entry point:
- x FROM x (and SELF)
-[from] ====== END OF CALLWISE DEPENDENCIES ======
-[inout] Out (internal) for function f:
- x; i
diff --git a/tests/journal/oracle/control.2.res.oracle b/tests/journal/oracle/control.2.res.oracle
deleted file mode 100644
index 2c9d316b3d61cb2542d43b9dcd9eea66d30c10b0..0000000000000000000000000000000000000000
--- a/tests/journal/oracle/control.2.res.oracle
+++ /dev/null
@@ -1,6 +0,0 @@
-1
-2
-3
-1
-2
-3
diff --git a/tests/journal/oracle/control2.res.oracle b/tests/journal/oracle/control2.res.oracle
deleted file mode 100644
index 97fb53bb8f67b370c1e94911f5b7ef2df89199fc..0000000000000000000000000000000000000000
--- a/tests/journal/oracle/control2.res.oracle
+++ /dev/null
@@ -1,73 +0,0 @@
-[kernel] Parsing control2.c (with preprocessing)
-[eva] Analyzing a complete application starting at f
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- x ∈ {0}
- y ∈ {0}
- c ∈ {0}
- d ∈ {0}
-[eva] control2.c:14: starting to merge loop iterations
-[eva:alarm] control2.c:17: Warning:
- signed overflow. assert x + 1 ≤ 2147483647;
-[eva] done for function f
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function f:
- x ∈ [0..2147483647]
- i ∈ {4}
-[eva:summary] ====== ANALYSIS SUMMARY ======
- ----------------------------------------------------------------------------
- 1 function analyzed (out of 1): 100% coverage.
- In this function, 9 statements reached (out of 12): 75% coverage.
- ----------------------------------------------------------------------------
- No errors or warnings raised during the analysis.
- ----------------------------------------------------------------------------
- 1 alarm generated by the analysis:
- 1 integer overflow
- ----------------------------------------------------------------------------
- No logical properties have been reached by the analysis.
- ----------------------------------------------------------------------------
-[from] Computing for function f
-[from] Done for function f
-[eva] Analyzing an incomplete application starting at f
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- x ∈ [--..--]
- y ∈ [--..--]
- c ∈ [--..--]
- d ∈ [--..--]
-[eva:alarm] control2.c:15: Warning:
- signed overflow. assert y + 1 ≤ 2147483647;
-[eva:alarm] control2.c:15: Warning:
- signed overflow. assert x + 1 ≤ 2147483647;
-[eva:alarm] control2.c:17: Warning:
- signed overflow. assert x + 1 ≤ 2147483647;
-[eva] done for function f
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function f:
- x ∈ [--..--]
- y ∈ [--..--]
- i ∈ {4}
-[eva:summary] ====== ANALYSIS SUMMARY ======
- ----------------------------------------------------------------------------
- 1 function analyzed (out of 1): 100% coverage.
- In this function, 12 statements reached (out of 12): 100% coverage.
- ----------------------------------------------------------------------------
- No errors or warnings raised during the analysis.
- ----------------------------------------------------------------------------
- 3 alarms generated by the analysis:
- 3 integer overflows
- ----------------------------------------------------------------------------
- No logical properties have been reached by the analysis.
- ----------------------------------------------------------------------------
-[from] Computing for function f
-[from] Done for function f
-[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
-[from] Function f:
- x FROM x; c; d (and SELF)
- y FROM y; c; d (and SELF)
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function f:
- x; y; i
diff --git a/tests/journal/oracle/control2_sav.err b/tests/journal/oracle/control2_sav.err
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/tests/journal/oracle/control2_sav.res b/tests/journal/oracle/control2_sav.res
deleted file mode 100644
index 1734f9bb5372539b42ca6899a554625e521d5272..0000000000000000000000000000000000000000
--- a/tests/journal/oracle/control2_sav.res
+++ /dev/null
@@ -1,77 +0,0 @@
-[kernel] Parsing control2.c (with preprocessing)
-[eva] Analyzing a complete application starting at f
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- x ∈ {0}
- y ∈ {0}
- c ∈ {0}
- d ∈ {0}
-[eva] control2.c:14: starting to merge loop iterations
-[eva:alarm] control2.c:17: Warning:
- signed overflow. assert x + 1 ≤ 2147483647;
-[eva] done for function f
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function f:
- x ∈ [0..2147483647]
- i ∈ {4}
-[eva:summary] ====== ANALYSIS SUMMARY ======
- ----------------------------------------------------------------------------
- 1 function analyzed (out of 1): 100% coverage.
- In this function, 9 statements reached (out of 12): 75% coverage.
- ----------------------------------------------------------------------------
- No errors or warnings raised during the analysis.
- ----------------------------------------------------------------------------
- 1 alarm generated by the analysis:
- 1 integer overflow
- ----------------------------------------------------------------------------
- No logical properties have been reached by the analysis.
- ----------------------------------------------------------------------------
-[from] Computing for function f
-[from] Done for function f
-[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
-[eva] Analyzing an incomplete application starting at f
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- x ∈ [--..--]
- y ∈ [--..--]
- c ∈ [--..--]
- d ∈ [--..--]
-[eva:alarm] control2.c:15: Warning:
- signed overflow. assert y + 1 ≤ 2147483647;
-[eva:alarm] control2.c:15: Warning:
- signed overflow. assert x + 1 ≤ 2147483647;
-[eva:alarm] control2.c:17: Warning:
- signed overflow. assert x + 1 ≤ 2147483647;
-[eva] done for function f
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function f:
- x ∈ [--..--]
- y ∈ [--..--]
- i ∈ {4}
-[eva:summary] ====== ANALYSIS SUMMARY ======
- ----------------------------------------------------------------------------
- 1 function analyzed (out of 1): 100% coverage.
- In this function, 12 statements reached (out of 12): 100% coverage.
- ----------------------------------------------------------------------------
- Some errors and warnings have been raised during the analysis:
- by the Eva analyzer: 0 errors 0 warnings
- by the Frama-C kernel: 0 errors 1 warning
- ----------------------------------------------------------------------------
- 3 alarms generated by the analysis:
- 3 integer overflows
- ----------------------------------------------------------------------------
- No logical properties have been reached by the analysis.
- ----------------------------------------------------------------------------
-[from] Computing for function f
-[from] Done for function f
-[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
-[from] Function f:
- x FROM x; c; d (and SELF)
- y FROM y; c; d (and SELF)
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function f:
- x; y; i
-[kernel] writing journal in file `control_journal_next2.ml'.
diff --git a/tests/journal/oracle/intra.res.oracle b/tests/journal/oracle/intra.res.oracle
deleted file mode 100644
index 052f7084beaf919d15fdb51263abd24d850c2459..0000000000000000000000000000000000000000
--- a/tests/journal/oracle/intra.res.oracle
+++ /dev/null
@@ -1,116 +0,0 @@
-[kernel] Parsing intra.i (no preprocessing)
-[sparecode] remove unused code...
-[eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- G ∈ {0}
- X10 ∈ {0}
- Y10 ∈ {0}
-[eva] computing for function param <- main.
- Called from intra.i:83.
-[eva] Recording results for param
-[eva] Done for function param
-[eva] computing for function tmp <- main.
- Called from intra.i:84.
-[eva] intra.i:22: assertion got status valid.
-[eva] intra.i:24: assertion got status valid.
-[eva] Recording results for tmp
-[eva] Done for function tmp
-[eva] computing for function spare_called_fct <- main.
- Called from intra.i:85.
-[eva] Recording results for spare_called_fct
-[eva] Done for function spare_called_fct
-[eva] computing for function call_two_outputs <- main.
- Called from intra.i:86.
-[eva] computing for function two_outputs <- call_two_outputs <- main.
- Called from intra.i:50.
-[eva] Recording results for two_outputs
-[eva] Done for function two_outputs
-[eva] computing for function two_outputs <- call_two_outputs <- main.
- Called from intra.i:54.
-[eva] Recording results for two_outputs
-[eva] Done for function two_outputs
-[eva] Recording results for call_two_outputs
-[eva] Done for function call_two_outputs
-[eva] computing for function loop <- main.
- Called from intra.i:87.
-[eva] intra.i:65: assertion got status valid.
-[eva] intra.i:66: loop invariant got status valid.
-[eva] intra.i:68: starting to merge loop iterations
-[eva] Recording results for loop
-[eva] Done for function loop
-[eva] computing for function assign <- main.
- Called from intra.i:88.
-[eva] Recording results for assign
-[eva] Done for function assign
-[eva] computing for function assign <- main.
- Called from intra.i:89.
-[eva] Recording results for assign
-[eva] Done for function assign
-[kernel:annot:missing-spec] intra.i:92: Warning:
- Neither code nor specification for function stop, generating default assigns from the prototype
-[eva] computing for function stop <- main.
- Called from intra.i:92.
-[eva] using specification for function stop
-[eva] Done for function stop
-[eva] Recording results for main
-[eva] done for function main
-[eva:summary] ====== ANALYSIS SUMMARY ======
- ----------------------------------------------------------------------------
- 8 functions analyzed (out of 10): 80% coverage.
- In these functions, 58 statements reached (out of 59): 98% coverage.
- ----------------------------------------------------------------------------
- Some errors and warnings have been raised during the analysis:
- by the Eva analyzer: 0 errors 0 warnings
- by the Frama-C kernel: 0 errors 1 warning
- ----------------------------------------------------------------------------
- 0 alarms generated by the analysis.
- ----------------------------------------------------------------------------
- Evaluation of the logical properties reached by the analysis:
- Assertions 4 valid 0 unknown 0 invalid 4 total
- Preconditions 0 valid 0 unknown 0 invalid 0 total
- 100% of the logical properties reached have been proven.
- ----------------------------------------------------------------------------
-[pdg] computing for function main
-[from] Computing for function param
-[from] Done for function param
-[from] Computing for function tmp
-[from] Done for function tmp
-[from] Computing for function spare_called_fct
-[from] Done for function spare_called_fct
-[from] Computing for function call_two_outputs
-[from] Computing for function two_outputs <-call_two_outputs
-[from] Done for function two_outputs
-[from] Done for function call_two_outputs
-[from] Computing for function loop
-[from] Done for function loop
-[from] Computing for function assign
-[from] Done for function assign
-[from] Computing for function stop
-[from] Done for function stop
-[pdg] done for function main
-[pdg] computing for function call_two_outputs
-[pdg] done for function call_two_outputs
-[pdg] computing for function assign
-[pdg] done for function assign
-[pdg] computing for function loop
-[pdg] done for function loop
-[pdg] computing for function tmp
-[pdg] done for function tmp
-[pdg] computing for function param
-[pdg] done for function param
-[pdg] computing for function two_outputs
-[pdg] done for function two_outputs
-[pdg] computing for function f10
-[pdg] Warning: unreachable entry point (sid:79, function f10)
-[pdg] Bottom for function f10
-[pdg] computing for function main2
-[pdg] Warning: unreachable entry point (sid:87, function main2)
-[pdg] Bottom for function main2
-[pdg] computing for function spare_called_fct
-[pdg] done for function spare_called_fct
-[pdg] computing for function stop
-[pdg] done for function stop
-[sparecode] remove unused global declarations...
-[sparecode] result in new project 'default without sparecode'.
diff --git a/tests/journal/test_config b/tests/journal/test_config
deleted file mode 100644
index 5b4e9a8bdd2b7dce5f1cd2d18923ecc5f7519b56..0000000000000000000000000000000000000000
--- a/tests/journal/test_config
+++ /dev/null
@@ -1,2 +0,0 @@
-PLUGIN:
-STDOPT:
diff --git a/tests/journal/use_cpt.ml b/tests/journal/use_cpt.ml
deleted file mode 100644
index f19b3e11a7f79e8c8981f2c3f73aff992e5fedd7..0000000000000000000000000000000000000000
--- a/tests/journal/use_cpt.ml
+++ /dev/null
@@ -1,20 +0,0 @@
-
-let main () =
- let module T = Type.Abstract(struct let name = "Abstract_cpt.t" end) in
- let c =
- Dynamic.get
- ~plugin:"Abstract_cpt" "mk" (Datatype.func Datatype.unit T.ty) ()
- in
- let incr =
- Dynamic.get
- ~plugin:"Abstract_cpt" "incr" (Datatype.func T.ty Datatype.int)
- in
- let pretty =
- Dynamic.get
- ~plugin:"Abstract_cpt" "pretty" (Datatype.func T.ty Datatype.unit)
- in
- let incr_and_pretty c = ignore (incr c); pretty c in
- for _i = 1 to 3 do incr_and_pretty c done
-
-let () = Db.Main.extend main
-
diff --git a/tests/slicing/combine.ml b/tests/slicing/combine.ml
index bbe23a110edfb1fe818977e138123364b920b55c..55fef497d923a4e9cba21e14e64d1b0174829bc4 100644
--- a/tests/slicing/combine.ml
+++ b/tests/slicing/combine.ml
@@ -6,15 +6,6 @@ let f_slice_names kf src_called fnum =
if (fname = "main") || (fnum = 1 && not src_called) then fname
else (fname ^ "_s_" ^ (string_of_int (fnum)))
-(* To be able to build framac-journal.ml *)
-let f_slice_names =
- Journal.register
- "Combine.f_slice_names"
- (Datatype.func Kernel_function.ty
- (Datatype.func Datatype.bool
- (Datatype.func Datatype.int Datatype.string)))
- f_slice_names
-
let main _ =
Slicing.Api.Project.reset_slicing ();
diff --git a/tests/sparecode/test_config b/tests/sparecode/test_config
index 40e3a32e1141194ae21aebe0470c76bca948bc06..f891b735a90856bbb735f6c53a50fef19542b9f6 100644
--- a/tests/sparecode/test_config
+++ b/tests/sparecode/test_config
@@ -1,3 +1,3 @@
MACRO: SPARECODE_PLUGINS @EVA_PLUGINS@ sparecode
PLUGIN: @SPARECODE_PLUGINS@
-OPT: -journal-disable @EVA_OPTIONS@ -sparecode-debug 1
+OPT: @EVA_OPTIONS@ -sparecode-debug 1
diff --git a/tests/spec/test_config b/tests/spec/test_config
index 6f16db895cb99190e93d744819de7c21e7358ebe..486cfa4b0f8caaaad2e1e03e663d2df6e32f5563 100644
--- a/tests/spec/test_config
+++ b/tests/spec/test_config
@@ -2,4 +2,4 @@ COMMENT: for now, this directory mainly tests the annotations syntax,
COMMENT: no analysis is performed.
COMMENT: we continue on annotation errors, as this allows to put
COMMENT: various variations of the same test in one file.
-OPT: -pp-annot -print -journal-disable -kernel-warn-key=annot-error=active -check -machdep x86_32
+OPT: -pp-annot -print -kernel-warn-key=annot-error=active -check -machdep x86_32