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/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-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.