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/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_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 3494bac4d7e0cd6b3b4e55021dcc8dc03a99da71..1b7b59d67f06eb6aaac438a4d54c5c1f1d4512c6 100644
--- a/src/kernel_services/cmdline_parameters/parameter_state.ml
+++ b/src/kernel_services/cmdline_parameters/parameter_state.ml
@@ -225,7 +225,6 @@ struct
     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
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index b3bde6f9030b362ea04ba152340a9b210e689f3b..64e5c108ab5c3840e18f335d49f175bf582864d0 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -206,7 +206,6 @@ module Value = struct
         let dependencies = [Ast.self]
       end)
 
-  (* This function is *not* journalized *)
   let globals_set_initial_state state =
     if not (Option.equal Cvalue.Model.equal
               (Some state)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 694f2b80d0f996ee511811b822541326de75d86d..2af2d50cac7072e389760abd198f66268c9c6263 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}.
@@ -172,8 +171,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
@@ -196,8 +194,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/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 914de159566b9d99712904833dbcc132b0f1811a..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,44 +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)
-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 772f84b168d60d4dca4c86d5cd76a4e2498025c0..c7ff75869fc85686e3b5c56cd5a6a3c2a6ad9306 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -508,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/plugins/constant_propagation/api.ml b/src/plugins/constant_propagation/api.ml
index 9ad0bf458faafded42cbba46ad152b4780b0a312..b493138ca518026cddf832ade9121294518784d2 100644
--- a/src/plugins/constant_propagation/api.ml
+++ b/src/plugins/constant_propagation/api.ml
@@ -395,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/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/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/security_slicing/components.ml b/src/plugins/security_slicing/components.ml
index ac09384aaa16afe7708c1551247fafeb86233abf..629fa05f3835588deac0848a4d24514a7f93b89f 100644
--- a/src/plugins/security_slicing/components.ml
+++ b/src/plugins/security_slicing/components.ml
@@ -839,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)
@@ -878,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
index 3b17ef709fdb50f3f6dc147f12c5f42151d6542f..1751112ca3dacd3a63e01d2f1598308c41fdc705 100644
--- 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 949abeffd58fe44ee27aedd13dd4f972e7c789c0..bdc35b91066fc7c4fca741519f497a7dfdd21702 100644
--- a/src/plugins/slicing/api.ml
+++ b/src/plugins/slicing/api.ml
@@ -44,8 +44,6 @@ 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 ;
@@ -68,8 +66,6 @@ module Project = struct
 
   let default_slice_names = SlicingTransform.default_slice_names
 
-  (** {2 Functions with journalized side effects } *)
-
   let reset_slicing = SlicingState.reset_slicing
 
   let extract ?(f_slice_names=default_slice_names) new_proj_name =
@@ -159,8 +155,6 @@ 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 =
     SlicingProject.create_slice
 
@@ -226,8 +220,6 @@ 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 ~propagate_to_callers =
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 74a31d69012701e846df5255bd61c40a36ef231a..5391e63fc7871e53ab98f03aad91be8b6e3ae4a5 100644
--- a/src/plugins/slicing/slicingTypes.ml
+++ b/src/plugins/slicing/slicingTypes.ml
@@ -74,8 +74,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
diff --git a/src/plugins/slicing/slicingTypes.mli b/src/plugins/slicing/slicingTypes.mli
index fdf1db12067f758f993a76fb8e6d2a52f47e2879..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