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/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 7bb60f13bd74e576c7e6f0eec94738a0bcbc9879..42bd47dd87081990a51d1cf9f77de7a0828f62eb 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -1894,24 +1894,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 +1906,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 +1921,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/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_state.ml b/src/kernel_services/cmdline_parameters/parameter_state.ml
index 8eb52c61979378a7ff7e22feb97b37b92219a047..3494bac4d7e0cd6b3b4e55021dcc8dc03a99da71 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,17 +216,13 @@ 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 *)
@@ -256,7 +236,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/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index aa88f10322091cd8ea4672057d06ec95299aa840..b3bde6f9030b362ea04ba152340a9b210e689f3b 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 =
@@ -236,26 +207,19 @@ module Value = struct
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 +283,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..694f2b80d0f996ee511811b822541326de75d86d 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -53,22 +53,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,7 +62,6 @@ val register_compute:
(unit -> unit) ref -> (unit -> unit) -> State.t
val register_guarded_compute:
- string ->
(unit -> bool) ->
(unit -> unit) ref -> (unit -> 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..97c81c930cba7434669f6fe5711fc24895668dea 100644
--- a/src/kernel_services/plugin_entry_points/dynamic.mli
+++ b/src/kernel_services/plugin_entry_points/dynamic.mli
@@ -30,7 +30,7 @@
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
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 3ef630f87377615d376089c541fcb003c681f604..914de159566b9d99712904833dbcc132b0f1811a 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -942,7 +942,6 @@ module Journal = struct
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
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index 493cea1aaf76821266d0ebe68c52c132dbc5a7a5..772f84b168d60d4dca4c86d5cd76a4e2498025c0 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
diff --git a/src/libraries/project/project.ml b/src/libraries/project/project.ml
index 846407b26e1ddf5773036e0fb42a7ba7a713575c..6038ec5acf3fa7150d43d61485fda483000263ac 100644
--- a/src/libraries/project/project.ml
+++ b/src/libraries/project/project.ml
@@ -249,8 +249,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 +281,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 +297,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 +308,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 +330,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 +339,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 +382,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 +402,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 +414,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 +426,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 +475,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 +570,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 +653,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 +695,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 +704,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} *)
(* ************************************************************************** *)
@@ -836,8 +718,6 @@ module Undo = struct
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;
@@ -851,8 +731,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/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/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/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..9ad0bf458faafded42cbba46ad152b4780b0a312 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 =
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/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/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/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/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..de79082709f3d342e78ddc6d5155a0f1f54584a9 100644
--- a/src/plugins/rte/register.ml
+++ b/src/plugins/rte/register.ml
@@ -61,15 +61,15 @@ let compute () =
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;
+ Db.register fctref fct;
if is_dyn then
let _ignore =
- Dynamic.register ?comment ~plugin:"RteGen" name ty ~journalize:true fct
+ Dynamic.register ?comment ~plugin:"RteGen" name ty fct
in
()
let nojournal_register fctref fct =
- Db.register Db.Journalization_not_required fctref (fun () -> fct)
+ Db.register fctref (fun () -> fct)
let () =
journal_register false
@@ -109,7 +109,6 @@ let _ =
~plugin:"RteGen"
"emitter"
Emitter.ty
- ~journalize:false
Generator.emitter
(* retrieve list of generated rte annotations for a given stmt *)
@@ -122,7 +121,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 +131,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 +141,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 +149,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..ac09384aaa16afe7708c1551247fafeb86233abf 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)
diff --git a/src/plugins/slicing/api.ml b/src/plugins/slicing/api.ml
index 4f188601176098412d2a35e81ffbae854fbc8c2e..949abeffd58fe44ee27aedd13dd4f972e7c789c0 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 *)
@@ -52,17 +51,7 @@ let set_modes calls callers sliceUndef keepAnnotations () =
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 +67,18 @@ 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 +120,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
@@ -384,19 +162,13 @@ module Slice = struct
(** {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} *)
@@ -458,104 +230,48 @@ module Request = struct
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/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/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/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 ();