From 365dcde62a9ad30b07ccd2ae2c73516891723a42 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 25 Jan 2024 14:09:52 +0100
Subject: [PATCH] [kernel] Deprecates Db.Main
---
dev/size_states.ml | 2 +-
doc/developer/examples/populate_spec/populate.ml | 2 +-
.../examples/syntactic_check/syntactic_check.ml | 2 +-
doc/developer/tutorial/hello/src/extend_run.ml | 2 +-
.../tutorial/hello/v1-simple/hello_world.ml | 2 +-
.../tutorial/hello/v2-register/hello_world.ml | 2 +-
doc/developer/tutorial/hello/v3-log/hello_world.ml | 2 +-
.../tutorial/hello/v4-options/hello_world.ml | 2 +-
.../tutorial/hello/v5-multiple/hello_run.ml | 2 +-
.../tutorial/hello/v6-test-with-bug/hello_run.ml | 2 +-
doc/developer/tutorial/hello/v7-doc/hello_run.ml | 2 +-
.../viewcfg/src/extend_with_run_with_options.ml | 2 +-
.../tutorial/viewcfg/src/extend_with_simple_run.ml | 2 +-
.../tutorial/viewcfg/v1-simple/view_cfg.ml | 2 +-
.../tutorial/viewcfg/v2-options/view_cfg.ml | 2 +-
doc/developer/tutorial/viewcfg/v3-eva/view_cfg.ml | 2 +-
doc/developer/tutorial/viewcfg/v4-bogue/run.ml | 2 +-
doc/developer/tutorial/viewcfg/v5-state/run.ml | 2 +-
.../tutorial/viewcfg/v6-state-clear/run.ml | 2 +-
share/analysis-scripts/list_functions.ml | 2 +-
src/kernel_internals/runtime/boot.ml | 4 +++-
src/kernel_internals/runtime/boot.mli | 9 +++++++++
src/kernel_services/plugin_entry_points/db.ml | 2 +-
src/kernel_services/plugin_entry_points/db.mli | 14 ++++----------
src/plugins/alias/Alias.ml | 2 +-
src/plugins/aorai/aorai_register.ml | 2 +-
src/plugins/api-generator/api_generator.ml | 2 +-
src/plugins/callgraph/register.ml | 2 +-
src/plugins/constant_propagation/api.ml | 2 +-
src/plugins/dive/main.ml | 2 +-
src/plugins/e-acsl/examples/demo/script.ml | 2 +-
src/plugins/e-acsl/src/main.ml | 2 +-
src/plugins/eva/engine/analysis.ml | 2 +-
src/plugins/from/from_register.ml | 2 +-
src/plugins/gui/menu_manager.ml | 2 +-
src/plugins/impact/register.ml | 2 +-
src/plugins/inout/register.ml | 2 +-
src/plugins/loop_analysis/register.ml | 2 +-
src/plugins/markdown-report/mdr_register.ml | 2 +-
src/plugins/metrics/register.ml | 2 +-
src/plugins/nonterm/nonterm_run.ml | 2 +-
src/plugins/obfuscator/obfuscator_register.ml | 2 +-
src/plugins/occurrence/register.ml | 2 +-
src/plugins/pdg/register.ml | 2 +-
src/plugins/postdominators/postdominators.ml | 2 +-
src/plugins/reduc/register.ml | 2 +-
src/plugins/report/classify.ml | 2 +-
src/plugins/report/csv.ml | 2 +-
src/plugins/report/register.ml | 2 +-
src/plugins/report/tests/report/multi_emitters.ml | 2 +-
src/plugins/report/tests/report/no_hyp.ml | 2 +-
src/plugins/report/tests/report/one_hyp.ml | 2 +-
.../report/tests/report/projectified_status.ml | 2 +-
src/plugins/report/tests/report/several_hyps.ml | 2 +-
src/plugins/rte/register.ml | 2 +-
src/plugins/server/server_batch.ml | 2 +-
src/plugins/server/server_doc.ml | 2 +-
src/plugins/server/server_socket.ml | 2 +-
src/plugins/server/server_zmq.ok.ml | 2 +-
src/plugins/slicing/register.ml | 2 +-
src/plugins/sparecode/register.ml | 2 +-
src/plugins/users/users_register.ml | 2 +-
.../variadic/tests/declared/called_in_ghost.ml | 2 +-
src/plugins/wp/RegionAnalysis.ml | 2 +-
src/plugins/wp/register.ml | 2 +-
src/plugins/wp/tests/wp/stmtcompiler_test.ml | 2 +-
src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml | 2 +-
tests/builtins/big_local_array_script.ml | 2 +-
tests/callgraph/function_pointer.ml | 2 +-
tests/cil/Change_formals.ml | 2 +-
tests/cil/change_to_instr.ml | 2 +-
tests/cil/insert_formal.ml | 2 +-
tests/cil/mkBinOp.ml | 2 +-
tests/cil/queue_ghost_instr.ml | 2 +-
.../introduction_of_non_explicit_cast.ml | 2 +-
tests/crowbar/mutable_const_fail.ml | 2 +-
tests/crowbar/mutable_mutable_fail.ml | 2 +-
tests/dynamic/abstract2.ml | 2 +-
tests/float/fval_test.ml | 2 +-
tests/jcdb/jcdb.ml | 2 +-
tests/libc/check_compliance.ml | 2 +-
tests/libc/check_const.ml | 2 +-
tests/libc/check_libc_anonymous_tags.ml | 2 +-
tests/libc/check_libc_naming_conventions.ml | 2 +-
tests/libc/check_parsing_individual_headers.ml | 2 +-
tests/misc/Debug_category.ml | 2 +-
tests/misc/add_assigns.ml | 2 +-
tests/misc/behavior_names.ml | 2 +-
tests/misc/bts0489.ml | 2 +-
tests/misc/bts1201.ml | 2 +-
tests/misc/bts1347.ml | 2 +-
tests/misc/bug_0209.ml | 2 +-
tests/misc/callsite.ml | 2 +-
tests/misc/change_main.ml | 2 +-
tests/misc/cil_builder.ml | 2 +-
tests/misc/cli_string_multiple_map.ml | 2 +-
tests/misc/copy_kf.ml | 2 +-
tests/misc/copy_machdep.ml | 2 +-
tests/misc/ensures.ml | 2 +-
tests/misc/find_enclosing_loop.ml | 2 +-
tests/misc/global_decl_loc.ml | 2 +-
tests/misc/init_from_cil.ml | 2 +-
.../misc/interpreted_automata_dataflow_backward.ml | 2 +-
.../misc/interpreted_automata_dataflow_forward.ml | 2 +-
tests/misc/issue109.ml | 2 +-
tests/misc/justcopy.ml | 2 +-
tests/misc/log_twice.ml | 2 +-
tests/misc/my_visitor.ml | 4 ++--
tests/misc/orphan_emitter.ml | 2 +-
tests/misc/plugin_log.ml | 2 +-
tests/misc/remove_status_hyps.ml | 2 +-
tests/misc/save_comments.ml | 2 +-
tests/misc/static.ml | 2 +-
tests/misc/test_datatype.ml | 2 +-
tests/misc/version.ml | 2 +-
tests/misc/vis_queueInstr.ml | 2 +-
tests/misc/vis_spec.ml | 2 +-
tests/misc/visitor_creates_func_bts_1349.ml | 2 +-
tests/misc/well_typed_alarm.ml | 2 +-
tests/misc/with space/module.ml | 2 +-
tests/misc/wstring_phase6.ml | 2 +-
tests/pdg/dyn_dpds.ml | 2 +-
tests/pdg/sets.ml | 2 +-
tests/rte/compute_annot.ml | 2 +-
tests/rte/my_annot_proxy.ml | 2 +-
tests/rte/my_annotation.ml | 2 +-
tests/rte/rte_get_annot.ml | 2 +-
tests/saveload/deps_E.ml | 2 +-
tests/saveload/load_one.ml | 4 ++--
tests/saveload/multi_project.ml | 2 +-
tests/saveload/status.ml | 2 +-
tests/scope/bts971.ml | 2 +-
tests/scope/zones.ml | 2 +-
tests/slicing/adpcm.ml | 2 +-
tests/slicing/anim.ml | 2 +-
tests/slicing/combine.ml | 2 +-
tests/slicing/ex_spec_interproc.ml | 2 +-
tests/slicing/horwitz.ml | 2 +-
tests/slicing/mark_all_slices.ml | 2 +-
tests/slicing/merge.ml | 2 +-
tests/slicing/min_call.ml | 2 +-
tests/slicing/select_by_annot.ml | 2 +-
tests/slicing/select_simple.ml | 2 +-
tests/slicing/simple_intra_slice.ml | 2 +-
tests/slicing/slice_no_body.ml | 2 +-
tests/slicing/switch.ml | 2 +-
tests/spec/Extend.ml | 2 +-
tests/spec/Extend_recursive_preprocess.ml | 2 +-
tests/spec/Extend_short_print.ml | 2 +-
tests/spec/Type_of_term.ml | 2 +-
tests/spec/add_global.ml | 2 +-
tests/spec/assigns_from_kf.ml | 2 +-
tests/spec/boolean_conversion.ml | 2 +-
tests/spec/bts0578.ml | 2 +-
tests/spec/bts0655.ml | 2 +-
tests/spec/comparison.ml | 2 +-
tests/spec/default_spec_combine.ml | 2 +-
tests/spec/default_spec_custom.ml | 2 +-
tests/spec/default_spec_mode.ml | 2 +-
tests/spec/expr_to_term.ml | 2 +-
tests/spec/extend_extern.ml | 2 +-
tests/spec/location_char.ml | 2 +-
tests/spec/logic_functions_sets.ml | 2 +-
tests/spec/loop_assigns_generated.ml | 2 +-
tests/spec/model.ml | 2 +-
tests/spec/pp_empty_spec.ml | 2 +-
tests/spec/property_test.ml | 2 +-
tests/spec/status_by_call_issue_890.ml | 2 +-
tests/spec/type_constructors_in_env.ml | 2 +-
tests/syntax/Enum_repr.ml | 2 +-
tests/syntax/Refresh_visitor.ml | 2 +-
tests/syntax/add_allocates.ml | 2 +-
tests/syntax/ast_diff_1.ml | 2 +-
tests/syntax/ast_init.ml | 2 +-
tests/syntax/clone_test.ml | 2 +-
tests/syntax/copy_visitor_bts_1073.ml | 2 +-
tests/syntax/copy_visitor_bts_1073_bis.ml | 2 +-
tests/syntax/formals_decl_leak.ml | 2 +-
tests/syntax/func_locs.ml | 2 +-
tests/syntax/get_astinfo_bts1136.ml | 2 +-
tests/syntax/ghost_cv_var_decl.ml | 2 +-
tests/syntax/ghost_parameters_formals_status.ml | 2 +-
tests/syntax/logic_env_script.ml | 2 +-
tests/syntax/mutable_test.ml | 2 +-
tests/syntax/reorder.ml | 2 +-
tests/syntax/temporary_location.ml | 2 +-
tests/syntax/transient_block.ml | 2 +-
tests/syntax/typedef_multi.ml | 2 +-
tests/syntax/vdescr_bts1387.ml | 2 +-
tests/syntax/visit_create_local.ml | 2 +-
tests/value/unit_tests.ml | 2 +-
191 files changed, 206 insertions(+), 201 deletions(-)
diff --git a/dev/size_states.ml b/dev/size_states.ml
index ad62726e2b8..020f68ab4c2 100644
--- a/dev/size_states.ml
+++ b/dev/size_states.ml
@@ -109,4 +109,4 @@ let all_sizes () =
Kernel.result "## Sizes ##@.%a"
(Pretty_utils.pp_list ~pre:"@[<v>" ~suf:"@]" ~sep:"@ " pp) res
-let () = Db.Main.extend all_sizes
+let () = Boot.Main.extend all_sizes
diff --git a/doc/developer/examples/populate_spec/populate.ml b/doc/developer/examples/populate_spec/populate.ml
index 9038698de7d..3c683010017 100644
--- a/doc/developer/examples/populate_spec/populate.ml
+++ b/doc/developer/examples/populate_spec/populate.ml
@@ -72,4 +72,4 @@ let create_mode () =
frama-c. *)
let () = Cmdline.run_after_configuring_stage create_mode
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/examples/syntactic_check/syntactic_check.ml b/doc/developer/examples/syntactic_check/syntactic_check.ml
index 604d1885603..7d84275fba2 100644
--- a/doc/developer/examples/syntactic_check/syntactic_check.ml
+++ b/doc/developer/examples/syntactic_check/syntactic_check.ml
@@ -64,4 +64,4 @@ let create_syntactic_check_project () =
ignore
(File.create_project_from_visitor "syntactic check" (new non_zero_divisor))
-let () = Db.Main.extend create_syntactic_check_project
+let () = Boot.Main.extend create_syntactic_check_project
diff --git a/doc/developer/tutorial/hello/src/extend_run.ml b/doc/developer/tutorial/hello/src/extend_run.ml
index e256faa8a32..4ee00dad2e5 100644
--- a/doc/developer/tutorial/hello/src/extend_run.ml
+++ b/doc/developer/tutorial/hello/src/extend_run.ml
@@ -1 +1 @@
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/hello/v1-simple/hello_world.ml b/doc/developer/tutorial/hello/v1-simple/hello_world.ml
index 4cc340bc30d..e4bd3f11a35 100644
--- a/doc/developer/tutorial/hello/v1-simple/hello_world.ml
+++ b/doc/developer/tutorial/hello/v1-simple/hello_world.ml
@@ -8,4 +8,4 @@ let run () =
let msg = Printexc.to_string exc in
Printf.eprintf "There was an error: %s\n" msg
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/hello/v2-register/hello_world.ml b/doc/developer/tutorial/hello/v2-register/hello_world.ml
index e5c74452edd..5f3817778eb 100644
--- a/doc/developer/tutorial/hello/v2-register/hello_world.ml
+++ b/doc/developer/tutorial/hello/v2-register/hello_world.ml
@@ -17,4 +17,4 @@ let run () =
let msg = Printexc.to_string exc in
Printf.eprintf "There was an error: %s\n" msg
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/hello/v3-log/hello_world.ml b/doc/developer/tutorial/hello/v3-log/hello_world.ml
index 3d9a51c9c60..988275d9d34 100644
--- a/doc/developer/tutorial/hello/v3-log/hello_world.ml
+++ b/doc/developer/tutorial/hello/v3-log/hello_world.ml
@@ -15,4 +15,4 @@ let run () =
in
Self.result "11 * 5 = %d" product
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/hello/v4-options/hello_world.ml b/doc/developer/tutorial/hello/v4-options/hello_world.ml
index 382621862ec..cc433a923fd 100644
--- a/doc/developer/tutorial/hello/v4-options/hello_world.ml
+++ b/doc/developer/tutorial/hello/v4-options/hello_world.ml
@@ -40,4 +40,4 @@ let run () =
let msg = Printexc.to_string exc in
Printf.eprintf "There was an error: %s\n" msg
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/hello/v5-multiple/hello_run.ml b/doc/developer/tutorial/hello/v5-multiple/hello_run.ml
index e6887489816..3a289ed851c 100644
--- a/doc/developer/tutorial/hello/v5-multiple/hello_run.ml
+++ b/doc/developer/tutorial/hello/v5-multiple/hello_run.ml
@@ -2,4 +2,4 @@ let run () =
if Hello_options.Enabled.get() then
Hello_print.output "Hello, world!"
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/hello/v6-test-with-bug/hello_run.ml b/doc/developer/tutorial/hello/v6-test-with-bug/hello_run.ml
index e01bf492151..23af83d0008 100644
--- a/doc/developer/tutorial/hello/v6-test-with-bug/hello_run.ml
+++ b/doc/developer/tutorial/hello/v6-test-with-bug/hello_run.ml
@@ -2,4 +2,4 @@ let run () =
if Hello_options.Enabled.get() then
Hello_print.output "Hello world!" (* removed comma *)
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/hello/v7-doc/hello_run.ml b/doc/developer/tutorial/hello/v7-doc/hello_run.ml
index e46b2fe6fc2..6c15467ee64 100644
--- a/doc/developer/tutorial/hello/v7-doc/hello_run.ml
+++ b/doc/developer/tutorial/hello/v7-doc/hello_run.ml
@@ -13,4 +13,4 @@ let run () =
Hello_print.output "Hello, world!"
(** Definition of the entry point of the hello plug-in. *)
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/viewcfg/src/extend_with_run_with_options.ml b/doc/developer/tutorial/viewcfg/src/extend_with_run_with_options.ml
index b498fdb3da4..eb80f881da9 100644
--- a/doc/developer/tutorial/viewcfg/src/extend_with_run_with_options.ml
+++ b/doc/developer/tutorial/viewcfg/src/extend_with_run_with_options.ml
@@ -6,4 +6,4 @@ let run () =
Visitor.visitFramacFileSameGlobals (new print_cfg fmt) (Ast.get ());
close_out chan
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/viewcfg/src/extend_with_simple_run.ml b/doc/developer/tutorial/viewcfg/src/extend_with_simple_run.ml
index 122d1ffdc53..f6cfe169274 100644
--- a/doc/developer/tutorial/viewcfg/src/extend_with_simple_run.ml
+++ b/doc/developer/tutorial/viewcfg/src/extend_with_simple_run.ml
@@ -4,4 +4,4 @@ let run () =
Visitor.visitFramacFileSameGlobals (new print_cfg fmt) (Ast.get ());
close_out chan
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/viewcfg/v1-simple/view_cfg.ml b/doc/developer/tutorial/viewcfg/v1-simple/view_cfg.ml
index 0841af991e9..7a695885327 100644
--- a/doc/developer/tutorial/viewcfg/v1-simple/view_cfg.ml
+++ b/doc/developer/tutorial/viewcfg/v1-simple/view_cfg.ml
@@ -50,4 +50,4 @@ let run () =
Visitor.visitFramacFileSameGlobals (new print_cfg fmt) (Ast.get ());
close_out chan
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/viewcfg/v2-options/view_cfg.ml b/doc/developer/tutorial/viewcfg/v2-options/view_cfg.ml
index 8fa8244e8d4..fdf6111c94e 100644
--- a/doc/developer/tutorial/viewcfg/v2-options/view_cfg.ml
+++ b/doc/developer/tutorial/viewcfg/v2-options/view_cfg.ml
@@ -71,4 +71,4 @@ let run () =
Visitor.visitFramacFileSameGlobals (new print_cfg fmt) (Ast.get ());
close_out chan
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/viewcfg/v3-eva/view_cfg.ml b/doc/developer/tutorial/viewcfg/v3-eva/view_cfg.ml
index 1eefd2a6aaf..d4efc8e180a 100644
--- a/doc/developer/tutorial/viewcfg/v3-eva/view_cfg.ml
+++ b/doc/developer/tutorial/viewcfg/v3-eva/view_cfg.ml
@@ -79,4 +79,4 @@ let run () =
Visitor.visitFramacFileSameGlobals (new print_cfg fmt) (Ast.get ());
close_out chan
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/viewcfg/v4-bogue/run.ml b/doc/developer/tutorial/viewcfg/v4-bogue/run.ml
index adc46ac9afe..77310af6265 100644
--- a/doc/developer/tutorial/viewcfg/v4-bogue/run.ml
+++ b/doc/developer/tutorial/viewcfg/v4-bogue/run.ml
@@ -2,4 +2,4 @@ let run () =
if Options.Gui.get() then
Gui.show ()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/viewcfg/v5-state/run.ml b/doc/developer/tutorial/viewcfg/v5-state/run.ml
index adc46ac9afe..77310af6265 100644
--- a/doc/developer/tutorial/viewcfg/v5-state/run.ml
+++ b/doc/developer/tutorial/viewcfg/v5-state/run.ml
@@ -2,4 +2,4 @@ let run () =
if Options.Gui.get() then
Gui.show ()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/doc/developer/tutorial/viewcfg/v6-state-clear/run.ml b/doc/developer/tutorial/viewcfg/v6-state-clear/run.ml
index adc46ac9afe..77310af6265 100644
--- a/doc/developer/tutorial/viewcfg/v6-state-clear/run.ml
+++ b/doc/developer/tutorial/viewcfg/v6-state-clear/run.ml
@@ -2,4 +2,4 @@ let run () =
if Options.Gui.get() then
Gui.show ()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/share/analysis-scripts/list_functions.ml b/share/analysis-scripts/list_functions.ml
index 2f5e58acc16..843e8bfd9d2 100644
--- a/share/analysis-scripts/list_functions.ml
+++ b/share/analysis-scripts/list_functions.ml
@@ -300,4 +300,4 @@ let run () =
in
print_json outfp funinfos_json
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/src/kernel_internals/runtime/boot.ml b/src/kernel_internals/runtime/boot.ml
index 3b40425c8b0..e93f37b85bd 100644
--- a/src/kernel_internals/runtime/boot.ml
+++ b/src/kernel_internals/runtime/boot.ml
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+module Main = Hook.Make ()
+
let toplevel = ref (fun f -> f ())
let set_toplevel run = toplevel := run
@@ -33,7 +35,7 @@ let play_analysis () =
end
end;
try
- Db.Main.apply ();
+ Main.apply ();
Log.treat_deferred_error ();
(* Printing code, if required, have to be done at end. *)
if Kernel.PrintCode.get () then File.pretty_ast ();
diff --git a/src/kernel_internals/runtime/boot.mli b/src/kernel_internals/runtime/boot.mli
index 23fdd74a8e1..e5f1df0f519 100644
--- a/src/kernel_internals/runtime/boot.mli
+++ b/src/kernel_internals/runtime/boot.mli
@@ -20,6 +20,15 @@
(* *)
(**************************************************************************)
+(** Frama-C main interface.
+ @since Lithium-20081201
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
+module Main : sig
+ val extend : (unit -> unit) -> unit
+ (** Register a function to be called by the Frama-C main entry point.
+ @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
+end
+
val play_analysis : unit -> unit
(** Run all the Frama-C analyses. This function should be called only by
toplevels.
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 017f5d7e289..94925cd9905 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -21,7 +21,7 @@
(**************************************************************************)
module Main = struct
- include Hook.Make()
+ let extend = Boot.Main.extend
end
(* ************************************************************************* *)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 08f85896583..e119a4018c2 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -45,20 +45,14 @@
line)
*)
-(** Frama-C main interface.
+(** DEPRECATED Frama-C main interface.
@since Lithium-20081201
- @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
+ @deprecated Frama-C+dev Use module {!Boot.Main} *)
module Main: sig
-
val extend : (unit -> unit) -> unit
+ [@@ deprecated "Use module Boot.Main"]
(** Register a function to be called by the Frama-C main entry point.
- @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
-
- (**/**)
- val apply: unit -> unit
- (** Not for casual user. *)
- (**/**)
-
+ @deprecated Frama-C+dev Use module {!Boot.Main} *)
end
(** {3 GUI} *)
diff --git a/src/plugins/alias/Alias.ml b/src/plugins/alias/Alias.ml
index fe144bb2b96..fa71e931f15 100644
--- a/src/plugins/alias/Alias.ml
+++ b/src/plugins/alias/Alias.ml
@@ -33,4 +33,4 @@ let main () =
end
let () =
- Db.Main.extend main
+ Boot.Main.extend main
diff --git a/src/plugins/aorai/aorai_register.ml b/src/plugins/aorai/aorai_register.ml
index 67739a849f8..cc589bf5937 100644
--- a/src/plugins/aorai/aorai_register.ml
+++ b/src/plugins/aorai/aorai_register.ml
@@ -200,7 +200,7 @@ let run, _ =
run
let main () = if Aorai_option.is_on () then run ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(*
Local Variables:
diff --git a/src/plugins/api-generator/api_generator.ml b/src/plugins/api-generator/api_generator.ml
index 95ce1b8feb8..8a58db24333 100644
--- a/src/plugins/api-generator/api_generator.ml
+++ b/src/plugins/api-generator/api_generator.ml
@@ -581,6 +581,6 @@ let generate () =
end
let () =
- Db.Main.extend generate
+ Boot.Main.extend generate
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/callgraph/register.ml b/src/plugins/callgraph/register.ml
index 67792829ccc..d1a29f66bc4 100644
--- a/src/plugins/callgraph/register.ml
+++ b/src/plugins/callgraph/register.ml
@@ -27,7 +27,7 @@ let main () =
end else
if not (Cg.is_computed ()) then Cg.dump ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(*
Local Variables:
diff --git a/src/plugins/constant_propagation/api.ml b/src/plugins/constant_propagation/api.ml
index 13c1a758514..b81b894199c 100644
--- a/src/plugins/constant_propagation/api.ml
+++ b/src/plugins/constant_propagation/api.ml
@@ -398,7 +398,7 @@ let main () =
if force_semantic_folding then compute ()
let () =
- Db.Main.extend main
+ Boot.Main.extend main
(*
Local Variables:
diff --git a/src/plugins/dive/main.ml b/src/plugins/dive/main.ml
index 6c81b013f84..33f036663ac 100644
--- a/src/plugins/dive/main.ml
+++ b/src/plugins/dive/main.ml
@@ -66,4 +66,4 @@ let main () =
end
let () =
- Db.Main.extend main
+ Boot.Main.extend main
diff --git a/src/plugins/e-acsl/examples/demo/script.ml b/src/plugins/e-acsl/examples/demo/script.ml
index 5c61595d99b..bca0d3708ad 100644
--- a/src/plugins/e-acsl/examples/demo/script.ml
+++ b/src/plugins/e-acsl/examples/demo/script.ml
@@ -113,4 +113,4 @@ let main () =
let ppt, line = search kf in
emit ppt line
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/src/plugins/e-acsl/src/main.ml b/src/plugins/e-acsl/src/main.ml
index 850ebb7fe74..a4e5e85d31f 100644
--- a/src/plugins/e-acsl/src/main.ml
+++ b/src/plugins/e-acsl/src/main.ml
@@ -162,7 +162,7 @@ let main () =
ignore (generate_code (Options.Project_name.get ()));
end
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(*
Local Variables:
diff --git a/src/plugins/eva/engine/analysis.ml b/src/plugins/eva/engine/analysis.ml
index aee5de68bf0..de72e68303a 100644
--- a/src/plugins/eva/engine/analysis.ml
+++ b/src/plugins/eva/engine/analysis.ml
@@ -236,4 +236,4 @@ let main () =
if Parameters.ForceValues.get () then compute ();
if is_computed () then Red_statuses.report ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/src/plugins/from/from_register.ml b/src/plugins/from/from_register.ml
index 003c0d78fcf..df9beea20f8 100644
--- a/src/plugins/from/from_register.ml
+++ b/src/plugins/from/from_register.ml
@@ -158,7 +158,7 @@ let main () =
if not_quiet then print_calldeps ();
)
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(*
Local Variables:
diff --git a/src/plugins/gui/menu_manager.ml b/src/plugins/gui/menu_manager.ml
index 26fc68df230..56e64e53e6a 100644
--- a/src/plugins/gui/menu_manager.ml
+++ b/src/plugins/gui/menu_manager.ml
@@ -339,7 +339,7 @@ class menu_manager ?packing (_:Gtk_helper.host) =
else debug_item#misc#hide ()
in
reset ();
- Db.Main.extend reset
+ Boot.Main.extend reset
end
diff --git a/src/plugins/impact/register.ml b/src/plugins/impact/register.ml
index 3e5ff2aeb18..84f9e678d82 100644
--- a/src/plugins/impact/register.ml
+++ b/src/plugins/impact/register.ml
@@ -161,7 +161,7 @@ let main () =
ignore (compute_pragmas ());
Options.feedback "analysis done"
end
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(*
Local Variables:
diff --git a/src/plugins/inout/register.ml b/src/plugins/inout/register.ml
index f93bf609e17..f7a1db558c6 100644
--- a/src/plugins/inout/register.ml
+++ b/src/plugins/inout/register.ml
@@ -77,7 +77,7 @@ let main () =
end)
end
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(*
diff --git a/src/plugins/loop_analysis/register.ml b/src/plugins/loop_analysis/register.ml
index b643f5e21c3..cc4d6ba3666 100644
--- a/src/plugins/loop_analysis/register.ml
+++ b/src/plugins/loop_analysis/register.ml
@@ -38,4 +38,4 @@ let main () =
end
;;
-Db.Main.extend main;;
+Boot.Main.extend main;;
diff --git a/src/plugins/markdown-report/mdr_register.ml b/src/plugins/markdown-report/mdr_register.ml
index c459ac2c91b..24e4880f456 100644
--- a/src/plugins/markdown-report/mdr_register.ml
+++ b/src/plugins/markdown-report/mdr_register.ml
@@ -31,4 +31,4 @@ let main () =
Mdr_params.Generate.option_name s
let () =
- Db.Main.extend main
+ Boot.Main.extend main
diff --git a/src/plugins/metrics/register.ml b/src/plugins/metrics/register.ml
index 618b539d408..a307a06e68a 100644
--- a/src/plugins/metrics/register.ml
+++ b/src/plugins/metrics/register.ml
@@ -76,7 +76,7 @@ let main () =
;;
(* Register main entry points *)
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(*
diff --git a/src/plugins/nonterm/nonterm_run.ml b/src/plugins/nonterm/nonterm_run.ml
index 176678b5e49..9f01ac05a01 100644
--- a/src/plugins/nonterm/nonterm_run.ml
+++ b/src/plugins/nonterm/nonterm_run.ml
@@ -348,4 +348,4 @@ let main () =
if Enabled.get () then run_once ()
let () =
- Db.Main.extend main
+ Boot.Main.extend main
diff --git a/src/plugins/obfuscator/obfuscator_register.ml b/src/plugins/obfuscator/obfuscator_register.ml
index 22b3e698f5e..43e491e7433 100644
--- a/src/plugins/obfuscator/obfuscator_register.ml
+++ b/src/plugins/obfuscator/obfuscator_register.ml
@@ -71,7 +71,7 @@ let run () =
and by the discussion in Gitlab issue #491 *)
end
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
(*
Local Variables:
diff --git a/src/plugins/occurrence/register.ml b/src/plugins/occurrence/register.ml
index 84e20565349..2f8ae1cc9d5 100644
--- a/src/plugins/occurrence/register.ml
+++ b/src/plugins/occurrence/register.ml
@@ -249,7 +249,7 @@ let print_all = print_all
(* ************************************************************************** *)
let main _fmt = if Print.get () then print_all ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(*
Local Variables:
diff --git a/src/plugins/pdg/register.ml b/src/plugins/pdg/register.ml
index b065d1184b5..ad9c1cd40ad 100644
--- a/src/plugins/pdg/register.ml
+++ b/src/plugins/pdg/register.ml
@@ -84,7 +84,7 @@ let main () =
(compute_once ();
Pdg_parameters.BuildAll.output output)
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(* {2 Overview}
diff --git a/src/plugins/postdominators/postdominators.ml b/src/plugins/postdominators/postdominators.ml
index d9273a0790d..a182c3e7844 100644
--- a/src/plugins/postdominators/postdominators.ml
+++ b/src/plugins/postdominators/postdominators.ml
@@ -39,4 +39,4 @@ let output () =
let output, _ = State_builder.apply_once "Postdominators.Compute.output"
[Compute.self] output
-let () = Db.Main.extend output
+let () = Boot.Main.extend output
diff --git a/src/plugins/reduc/register.ml b/src/plugins/reduc/register.ml
index 4595aacd8a2..8c2c574f6b5 100644
--- a/src/plugins/reduc/register.ml
+++ b/src/plugins/reduc/register.ml
@@ -38,4 +38,4 @@ let main () =
()
end
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/src/plugins/report/classify.ml b/src/plugins/report/classify.ml
index 5e7ef8e3bc1..8a6cf8b9e4d 100644
--- a/src/plugins/report/classify.ml
+++ b/src/plugins/report/classify.ml
@@ -574,7 +574,7 @@ let main () =
let () =
begin
Cmdline.run_after_configuring_stage register ;
- Db.Main.extend main ;
+ Boot.Main.extend main ;
end
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/report/csv.ml b/src/plugins/report/csv.ml
index df3464b5713..6b0e644de4e 100644
--- a/src/plugins/report/csv.ml
+++ b/src/plugins/report/csv.ml
@@ -110,7 +110,7 @@ let print_csv, _ =
let main () =
if not (Report_parameters.CSVFile.is_empty ()) then print_csv ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(*
diff --git a/src/plugins/report/register.ml b/src/plugins/report/register.ml
index 7bb30f74339..d19dc67fd9c 100644
--- a/src/plugins/report/register.ml
+++ b/src/plugins/report/register.ml
@@ -47,7 +47,7 @@ let print, _ =
let main () = if Report_parameters.Print.get () then print ()
let () =
- Db.Main.extend main;
+ Boot.Main.extend main;
(*
Local Variables:
diff --git a/src/plugins/report/tests/report/multi_emitters.ml b/src/plugins/report/tests/report/multi_emitters.ml
index 9680545a918..b8411106ae8 100644
--- a/src/plugins/report/tests/report/multi_emitters.ml
+++ b/src/plugins/report/tests/report/multi_emitters.ml
@@ -59,4 +59,4 @@ let main () =
set_status emitter1 Property_status.False_and_reachable;
print_status ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/src/plugins/report/tests/report/no_hyp.ml b/src/plugins/report/tests/report/no_hyp.ml
index ecc7d9b4505..8c5bd1a2951 100644
--- a/src/plugins/report/tests/report/no_hyp.ml
+++ b/src/plugins/report/tests/report/no_hyp.ml
@@ -52,4 +52,4 @@ let main () =
*)
end
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/src/plugins/report/tests/report/one_hyp.ml b/src/plugins/report/tests/report/one_hyp.ml
index 178682c5981..48f2de3ef19 100644
--- a/src/plugins/report/tests/report/one_hyp.ml
+++ b/src/plugins/report/tests/report/one_hyp.ml
@@ -223,4 +223,4 @@ let main () =
(* *********************************************************************** *)
()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/src/plugins/report/tests/report/projectified_status.ml b/src/plugins/report/tests/report/projectified_status.ml
index 643fbd6057e..8e361649e87 100644
--- a/src/plugins/report/tests/report/projectified_status.ml
+++ b/src/plugins/report/tests/report/projectified_status.ml
@@ -55,4 +55,4 @@ let main () =
set_status Property_status.Dont_know;
print_status ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/src/plugins/report/tests/report/several_hyps.ml b/src/plugins/report/tests/report/several_hyps.ml
index 929820d1c99..c1413df81d4 100644
--- a/src/plugins/report/tests/report/several_hyps.ml
+++ b/src/plugins/report/tests/report/several_hyps.ml
@@ -205,4 +205,4 @@ let main () =
(***************************************************************************)
test "INCONSISTENT + INCONSISTENT" (set inconsistent inconsistent)
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/src/plugins/rte/register.ml b/src/plugins/rte/register.ml
index 27abdbadafe..2019f62b4db 100644
--- a/src/plugins/rte/register.ml
+++ b/src/plugins/rte/register.ml
@@ -86,7 +86,7 @@ let main () =
"annotations computed"
end
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(*
Local Variables:
diff --git a/src/plugins/server/server_batch.ml b/src/plugins/server/server_batch.ml
index 5f1039342c9..855dbe38cfd 100644
--- a/src/plugins/server/server_batch.ml
+++ b/src/plugins/server/server_batch.ml
@@ -126,6 +126,6 @@ let execute () =
(* --- Run the Server from the Command line --- *)
(* -------------------------------------------------------------------------- *)
-let () = Db.Main.extend execute
+let () = Boot.Main.extend execute
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/server_doc.ml b/src/plugins/server/server_doc.ml
index 52eb8613929..7a6617155ee 100644
--- a/src/plugins/server/server_doc.ml
+++ b/src/plugins/server/server_doc.ml
@@ -383,7 +383,7 @@ let dump ~root ?(meta=true) () =
end
let () =
- Db.Main.extend begin
+ Boot.Main.extend begin
fun () ->
if not (Senv.Doc.is_empty ()) then
let root = Senv.Doc.get () in
diff --git a/src/plugins/server/server_socket.ml b/src/plugins/server/server_socket.ml
index 2337dbdb92d..74394943bb2 100644
--- a/src/plugins/server/server_socket.ml
+++ b/src/plugins/server/server_socket.ml
@@ -336,6 +336,6 @@ let cmdline () =
(Printexc.to_string exn)
end
-let () = Db.Main.extend cmdline
+let () = Boot.Main.extend cmdline
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/server_zmq.ok.ml b/src/plugins/server/server_zmq.ok.ml
index 04bf6496e9f..340aec48868 100644
--- a/src/plugins/server/server_zmq.ok.ml
+++ b/src/plugins/server/server_zmq.ok.ml
@@ -212,6 +212,6 @@ let cmdline () =
if cmd <> "" then launch_client cmd ;
end
-let () = Db.Main.extend cmdline
+let () = Boot.Main.extend cmdline
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/slicing/register.ml b/src/plugins/slicing/register.ml
index 42bcad35768..716d0e00e99 100644
--- a/src/plugins/slicing/register.ml
+++ b/src/plugins/slicing/register.ml
@@ -60,7 +60,7 @@ let main () =
end
(** Register the function [main] as a main entry point. *)
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(* {2 Overview}
diff --git a/src/plugins/sparecode/register.ml b/src/plugins/sparecode/register.ml
index b413b26e451..9cfc87fef11 100644
--- a/src/plugins/sparecode/register.ml
+++ b/src/plugins/sparecode/register.ml
@@ -98,7 +98,7 @@ let main () =
File.pretty_ast ~prj:new_proj ()
end
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(*
Local Variables:
diff --git a/src/plugins/users/users_register.ml b/src/plugins/users/users_register.ml
index 25fd111322f..9cb63d7e0d9 100644
--- a/src/plugins/users/users_register.ml
+++ b/src/plugins/users/users_register.ml
@@ -110,7 +110,7 @@ let print () =
let print_once, _self_print =
State_builder.apply_once "Users_register.print" [ Users.self ] print
-let () = Db.Main.extend print_once
+let () = Boot.Main.extend print_once
(*
Local Variables:
diff --git a/src/plugins/variadic/tests/declared/called_in_ghost.ml b/src/plugins/variadic/tests/declared/called_in_ghost.ml
index 4aa4ac68015..24b8ad9579f 100644
--- a/src/plugins/variadic/tests/declared/called_in_ghost.ml
+++ b/src/plugins/variadic/tests/declared/called_in_ghost.ml
@@ -37,4 +37,4 @@ class print =
let run () = Visitor.visitFramacFileSameGlobals (new print) (Ast.get())
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/src/plugins/wp/RegionAnalysis.ml b/src/plugins/wp/RegionAnalysis.ml
index d476d72a079..50bc432573e 100644
--- a/src/plugins/wp/RegionAnalysis.ml
+++ b/src/plugins/wp/RegionAnalysis.ml
@@ -111,6 +111,6 @@ let main () =
) ;
end
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(* ---------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index eca897451ea..1823763111f 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -1031,6 +1031,6 @@ let main =
]
let () = Cmdline.at_normal_exit do_cache_cleanup
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(* ------------------------------------------------------------------------ *)
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test.ml b/src/plugins/wp/tests/wp/stmtcompiler_test.ml
index db4668d7326..4ab9acd47ce 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test.ml
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test.ml
@@ -149,4 +149,4 @@ let turn_off_populate () =
let () = Cmdline.run_after_configuring_stage turn_off_populate
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
index 3e167f78bf9..369d710cdd7 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
@@ -162,4 +162,4 @@ let run () =
ordered_kf
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/builtins/big_local_array_script.ml b/tests/builtins/big_local_array_script.ml
index dd8183d8e50..3654187155e 100644
--- a/tests/builtins/big_local_array_script.ml
+++ b/tests/builtins/big_local_array_script.ml
@@ -6,4 +6,4 @@ let foo () =
File.init_from_c_files [File.from_filename f]
end
-let () = Db.Main.extend foo
+let () = Boot.Main.extend foo
diff --git a/tests/callgraph/function_pointer.ml b/tests/callgraph/function_pointer.ml
index c2b8ca966bd..168be205dbb 100644
--- a/tests/callgraph/function_pointer.ml
+++ b/tests/callgraph/function_pointer.ml
@@ -1,4 +1,4 @@
let main () =
Format.printf "number of calls = %d@." (Callgraph.Uses.nb_calls ())
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/cil/Change_formals.ml b/tests/cil/Change_formals.ml
index f224e4bcfca..fe512686925 100644
--- a/tests/cil/Change_formals.ml
+++ b/tests/cil/Change_formals.ml
@@ -88,7 +88,7 @@ let main () =
if Project.get_name (Project.current()) <> "test" then
ignore (generate_code "test")
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(*
Local Variables:
diff --git a/tests/cil/change_to_instr.ml b/tests/cil/change_to_instr.ml
index 04d2679952d..85f19109e0f 100644
--- a/tests/cil/change_to_instr.ml
+++ b/tests/cil/change_to_instr.ml
@@ -14,4 +14,4 @@ let run () =
Visitor.visitFramacFileSameGlobals (new add_skip) (Ast.get())
let () =
- Db.Main.extend run
+ Boot.Main.extend run
diff --git a/tests/cil/insert_formal.ml b/tests/cil/insert_formal.ml
index a4796d9b33b..311f8c04101 100644
--- a/tests/cil/insert_formal.ml
+++ b/tests/cil/insert_formal.ml
@@ -57,4 +57,4 @@ let update_func f =
let run () =
Globals.Functions.iter_on_fundecs update_func
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/cil/mkBinOp.ml b/tests/cil/mkBinOp.ml
index 7ef013171d3..e07f3b60ab1 100644
--- a/tests/cil/mkBinOp.ml
+++ b/tests/cil/mkBinOp.ml
@@ -40,4 +40,4 @@ let main () =
test cone ione;
test ione cone
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/cil/queue_ghost_instr.ml b/tests/cil/queue_ghost_instr.ml
index f8a486d3fe7..78dfc0eeb16 100644
--- a/tests/cil/queue_ghost_instr.ml
+++ b/tests/cil/queue_ghost_instr.ml
@@ -24,4 +24,4 @@ let run () =
Visitor.visitFramacFileSameGlobals (new add_skip) (Ast.get())
let () =
- Db.Main.extend run
+ Boot.Main.extend run
diff --git a/tests/constant_propagation/introduction_of_non_explicit_cast.ml b/tests/constant_propagation/introduction_of_non_explicit_cast.ml
index 2d20a43cb00..425a359bd35 100644
--- a/tests/constant_propagation/introduction_of_non_explicit_cast.ml
+++ b/tests/constant_propagation/introduction_of_non_explicit_cast.ml
@@ -10,4 +10,4 @@ let main _ =
();
File.pretty_ast ~prj:new_proj ();;
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/crowbar/mutable_const_fail.ml b/tests/crowbar/mutable_const_fail.ml
index 453fa5f4839..1b8ed9cb196 100644
--- a/tests/crowbar/mutable_const_fail.ml
+++ b/tests/crowbar/mutable_const_fail.ml
@@ -15,4 +15,4 @@ let main () =
(Cil.typeHasAttribute "const" (Cil.typeOffset x.vtype offset))
| _ -> assert false
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/crowbar/mutable_mutable_fail.ml b/tests/crowbar/mutable_mutable_fail.ml
index a3c06d6424e..b72ff4783da 100644
--- a/tests/crowbar/mutable_mutable_fail.ml
+++ b/tests/crowbar/mutable_mutable_fail.ml
@@ -15,4 +15,4 @@ let main () =
(not (Cil.typeHasAttribute "const" (Cil.typeOffset x.vtype offset)))
| _ -> assert false
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/dynamic/abstract2.ml b/tests/dynamic/abstract2.ml
index 73293f6f62d..f3f0f72b3e4 100644
--- a/tests/dynamic/abstract2.ml
+++ b/tests/dynamic/abstract2.ml
@@ -30,4 +30,4 @@ let main () =
()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/float/fval_test.ml b/tests/float/fval_test.ml
index 6ce0dc57be0..edf9e20adae 100644
--- a/tests/float/fval_test.ml
+++ b/tests/float/fval_test.ml
@@ -277,4 +277,4 @@ let main _ =
test_forward_comp ();
;;
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/jcdb/jcdb.ml b/tests/jcdb/jcdb.ml
index d9163defa21..b5eceabbdf7 100644
--- a/tests/jcdb/jcdb.ml
+++ b/tests/jcdb/jcdb.ml
@@ -10,4 +10,4 @@ let run () =
let prj = Project.create_by_copy ~last:true "copy" in
Project.on prj print_json ()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/libc/check_compliance.ml b/tests/libc/check_compliance.ml
index 7a13be06edf..e75f6dac805 100644
--- a/tests/libc/check_compliance.ml
+++ b/tests/libc/check_compliance.ml
@@ -124,7 +124,7 @@ let check_ident c11 posix glibc nonstandard c11_headers id headers =
end
let () =
- Db.Main.extend (fun () ->
+ Boot.Main.extend (fun () ->
if not !run_once then begin
run_once := true;
let vis = new stdlib_visitor in
diff --git a/tests/libc/check_const.ml b/tests/libc/check_const.ml
index 9be7b2b2cf3..6996d5ed032 100644
--- a/tests/libc/check_const.ml
+++ b/tests/libc/check_const.ml
@@ -68,4 +68,4 @@ let check () =
in
Globals.Functions.iter check_kf
-let () = Db.Main.extend check
+let () = Boot.Main.extend check
diff --git a/tests/libc/check_libc_anonymous_tags.ml b/tests/libc/check_libc_anonymous_tags.ml
index c57db98104c..8e59f646a94 100644
--- a/tests/libc/check_libc_anonymous_tags.ml
+++ b/tests/libc/check_libc_anonymous_tags.ml
@@ -50,7 +50,7 @@ end
let run_once = ref false
let () =
- Db.Main.extend (fun () ->
+ Boot.Main.extend (fun () ->
if not !run_once then begin
run_once := true;
Visitor.visitFramacFile (new tags_visitor) (Ast.get ())
diff --git a/tests/libc/check_libc_naming_conventions.ml b/tests/libc/check_libc_naming_conventions.ml
index b4f0bdbd198..bb8b128d296 100644
--- a/tests/libc/check_libc_naming_conventions.ml
+++ b/tests/libc/check_libc_naming_conventions.ml
@@ -46,7 +46,7 @@ let check_separated =
let run_once = ref false
let () =
- Db.Main.extend (fun () ->
+ Boot.Main.extend (fun () ->
if not !run_once then begin
run_once := true;
Globals.Functions.fold (fun kf () ->
diff --git a/tests/libc/check_parsing_individual_headers.ml b/tests/libc/check_parsing_individual_headers.ml
index 8c18407a7c3..3f9c35918ac 100644
--- a/tests/libc/check_parsing_individual_headers.ml
+++ b/tests/libc/check_parsing_individual_headers.ml
@@ -45,4 +45,4 @@ let collect_headers () =
) all_headers
let () =
- Db.Main.extend collect_headers
+ Boot.Main.extend collect_headers
diff --git a/tests/misc/Debug_category.ml b/tests/misc/Debug_category.ml
index c3ab6699cdc..01515996ec8 100644
--- a/tests/misc/Debug_category.ml
+++ b/tests/misc/Debug_category.ml
@@ -43,4 +43,4 @@ let run () =
feedback ~dkey "D is enabled";
warning ~wkey "Another Warning A"
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/misc/add_assigns.ml b/tests/misc/add_assigns.ml
index d129f05a877..fdcf2b0c5d8 100644
--- a/tests/misc/add_assigns.ml
+++ b/tests/misc/add_assigns.ml
@@ -33,4 +33,4 @@ let main () =
Property_status.(emit emitter ~hyps:[] ip True)
end
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/misc/behavior_names.ml b/tests/misc/behavior_names.ml
index 079fb42f5e3..8c1b1578e44 100644
--- a/tests/misc/behavior_names.ml
+++ b/tests/misc/behavior_names.ml
@@ -10,4 +10,4 @@ let run () =
(Annotations.fresh_behavior_name kf "foo")
(Annotations.fresh_behavior_name kf "bla")
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/misc/bts0489.ml b/tests/misc/bts0489.ml
index 224c74f4289..cb02f561c12 100644
--- a/tests/misc/bts0489.ml
+++ b/tests/misc/bts0489.ml
@@ -17,4 +17,4 @@ let run () =
let file = Ast.get () in
Visitor.visitFramacFile (new visitor) file
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/misc/bts1201.ml b/tests/misc/bts1201.ml
index 8cb421763f5..9358eb15ac5 100644
--- a/tests/misc/bts1201.ml
+++ b/tests/misc/bts1201.ml
@@ -4,4 +4,4 @@ let main () =
Eva.Analysis.compute ();
;;
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/misc/bts1347.ml b/tests/misc/bts1347.ml
index ea417ba7710..b89b9009d34 100644
--- a/tests/misc/bts1347.ml
+++ b/tests/misc/bts1347.ml
@@ -25,4 +25,4 @@ let run () =
end)
let () =
- Db.Main.extend run
+ Boot.Main.extend run
diff --git a/tests/misc/bug_0209.ml b/tests/misc/bug_0209.ml
index b46478f7925..88601d0e068 100644
--- a/tests/misc/bug_0209.ml
+++ b/tests/misc/bug_0209.ml
@@ -13,4 +13,4 @@ let main () =
Logic_env.Builtins is not projectified) *)
Project.on p Ast.compute ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/misc/callsite.ml b/tests/misc/callsite.ml
index c906a333c79..4e839e8c337 100644
--- a/tests/misc/callsite.ml
+++ b/tests/misc/callsite.ml
@@ -16,4 +16,4 @@ let main () =
Ast.compute () ;
List.iter dump ["f";"g";"h";"k"]
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/misc/change_main.ml b/tests/misc/change_main.ml
index ac7fba803c6..cfc236e625f 100644
--- a/tests/misc/change_main.ml
+++ b/tests/misc/change_main.ml
@@ -11,4 +11,4 @@ let run () =
(File.create_project_from_visitor
"change_main" (fun prj -> new visitor prj))
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/misc/cil_builder.ml b/tests/misc/cil_builder.ml
index 571edd890e7..3f3bdb9afce 100644
--- a/tests/misc/cil_builder.ml
+++ b/tests/misc/cil_builder.ml
@@ -18,4 +18,4 @@ let run () =
let () =
- Db.Main.extend run
+ Boot.Main.extend run
diff --git a/tests/misc/cli_string_multiple_map.ml b/tests/misc/cli_string_multiple_map.ml
index e8f5b806e83..32771550a04 100644
--- a/tests/misc/cli_string_multiple_map.ml
+++ b/tests/misc/cli_string_multiple_map.ml
@@ -32,4 +32,4 @@ let main () =
in
Datatype.String.Map.iter print (M.get ())
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/misc/copy_kf.ml b/tests/misc/copy_kf.ml
index 84eef5538f0..b06b24d64db 100644
--- a/tests/misc/copy_kf.ml
+++ b/tests/misc/copy_kf.ml
@@ -53,4 +53,4 @@ let main () =
Kernel.feedback "After replacement:@\n%t"
(fun fmt -> File.pretty_ast ~fmt ())
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/misc/copy_machdep.ml b/tests/misc/copy_machdep.ml
index 9843d085b1e..63d674cf07b 100644
--- a/tests/misc/copy_machdep.ml
+++ b/tests/misc/copy_machdep.ml
@@ -13,4 +13,4 @@ let run () =
(if Kernel.Unicode.get () = Project.on proj Kernel.Unicode.get () then
"" else "not ")
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/misc/ensures.ml b/tests/misc/ensures.ml
index 61dfa1768fa..ca6ed24e40f 100644
--- a/tests/misc/ensures.ml
+++ b/tests/misc/ensures.ml
@@ -21,4 +21,4 @@ let run () =
function_name Property_status.pretty status)
ip)
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/misc/find_enclosing_loop.ml b/tests/misc/find_enclosing_loop.ml
index bf97a89df64..fe869a1f1be 100644
--- a/tests/misc/find_enclosing_loop.ml
+++ b/tests/misc/find_enclosing_loop.ml
@@ -30,4 +30,4 @@ let run () =
Visitor.visitFramacFileSameGlobals (new check) (Ast.get());
Kernel.result "Script done"
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/misc/global_decl_loc.ml b/tests/misc/global_decl_loc.ml
index afe0d309b5e..6e51a976cea 100644
--- a/tests/misc/global_decl_loc.ml
+++ b/tests/misc/global_decl_loc.ml
@@ -8,4 +8,4 @@ let run () =
Printer.pp_location vi.vdecl
)
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/misc/init_from_cil.ml b/tests/misc/init_from_cil.ml
index b64d3776a9d..8f1c10e8d02 100644
--- a/tests/misc/init_from_cil.ml
+++ b/tests/misc/init_from_cil.ml
@@ -5,4 +5,4 @@ let run () =
Project.set_current prj;
Printer.pp_file Format.std_formatter (Ast.get())
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/misc/interpreted_automata_dataflow_backward.ml b/tests/misc/interpreted_automata_dataflow_backward.ml
index 43e96ba1a24..dce5e8cfc2b 100644
--- a/tests/misc/interpreted_automata_dataflow_backward.ml
+++ b/tests/misc/interpreted_automata_dataflow_backward.ml
@@ -70,4 +70,4 @@ let run () =
Dataflow.Result.to_dot_file LivenessDomain.pretty results filepath
let () =
- Db.Main.extend run
+ Boot.Main.extend run
diff --git a/tests/misc/interpreted_automata_dataflow_forward.ml b/tests/misc/interpreted_automata_dataflow_forward.ml
index 6470ee92590..97678ef9abb 100644
--- a/tests/misc/interpreted_automata_dataflow_forward.ml
+++ b/tests/misc/interpreted_automata_dataflow_forward.ml
@@ -120,4 +120,4 @@ let run () =
ConstantsDomain.pretty result
let () =
- Db.Main.extend run
+ Boot.Main.extend run
diff --git a/tests/misc/issue109.ml b/tests/misc/issue109.ml
index 290543f644a..cf379082ec0 100644
--- a/tests/misc/issue109.ml
+++ b/tests/misc/issue109.ml
@@ -5,4 +5,4 @@ let main () =
File.init_from_cmdline ();
Eva.Analysis.compute ()
-let main = Db.Main.extend main
+let main = Boot.Main.extend main
diff --git a/tests/misc/justcopy.ml b/tests/misc/justcopy.ml
index 297c7fed4a4..9597d33f3c7 100644
--- a/tests/misc/justcopy.ml
+++ b/tests/misc/justcopy.ml
@@ -7,4 +7,4 @@ let main () =
in
ignore (File.create_project_from_visitor "justcopy" o)
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/misc/log_twice.ml b/tests/misc/log_twice.ml
index 73238757c07..67bb3b98488 100644
--- a/tests/misc/log_twice.ml
+++ b/tests/misc/log_twice.ml
@@ -13,4 +13,4 @@ let run () =
Eva.Analysis.compute ();
()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/misc/my_visitor.ml b/tests/misc/my_visitor.ml
index 832c2104127..c2248a4ebc1 100644
--- a/tests/misc/my_visitor.ml
+++ b/tests/misc/my_visitor.ml
@@ -81,7 +81,7 @@ let main () =
print ()
end
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(* This other main is a simple test for deep copy. *)
@@ -95,4 +95,4 @@ let main () =
assert (Project.on p ~selection (fun () -> not (Kernel.LibEntry.get ())) ())
end
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/misc/orphan_emitter.ml b/tests/misc/orphan_emitter.ml
index 2fd3673ffa3..5c31565debc 100644
--- a/tests/misc/orphan_emitter.ml
+++ b/tests/misc/orphan_emitter.ml
@@ -18,4 +18,4 @@ let main () =
let stmt = Kernel_function.find_first_stmt kf in
Annotations.add_assert emitter1 stmt Logic_const.ptrue
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/misc/plugin_log.ml b/tests/misc/plugin_log.ml
index 81908f38263..ac6d9836317 100644
--- a/tests/misc/plugin_log.ml
+++ b/tests/misc/plugin_log.ml
@@ -17,4 +17,4 @@ let main () =
failure "failure";*)
()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/misc/remove_status_hyps.ml b/tests/misc/remove_status_hyps.ml
index c382ddaaabc..be52ee29bff 100644
--- a/tests/misc/remove_status_hyps.ml
+++ b/tests/misc/remove_status_hyps.ml
@@ -58,4 +58,4 @@ let main () =
report "removing P1" l'
| _ -> assert false
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/misc/save_comments.ml b/tests/misc/save_comments.ml
index 0c9dea658b0..cfd3e993581 100644
--- a/tests/misc/save_comments.ml
+++ b/tests/misc/save_comments.ml
@@ -40,4 +40,4 @@ let run () =
Format.printf "Printing saved project:@.";
File.pretty_ast ~prj ~fmt ()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/misc/static.ml b/tests/misc/static.ml
index 7b6f77aa5f8..36c84526fdd 100644
--- a/tests/misc/static.ml
+++ b/tests/misc/static.ml
@@ -23,4 +23,4 @@ let run () =
Kernel.fatal "mixing local variables from f and g";
File.pretty_ast ()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/misc/test_datatype.ml b/tests/misc/test_datatype.ml
index 4787ec1dbbb..04a8eeca0ea 100644
--- a/tests/misc/test_datatype.ml
+++ b/tests/misc/test_datatype.ml
@@ -26,4 +26,4 @@ let main () =
(* no equality in Hashtbls. *)
Test.Hashtbl.iter (fun _ _ -> assert false) (H.copy h)
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/misc/version.ml b/tests/misc/version.ml
index c51486acaec..cddd787c76c 100644
--- a/tests/misc/version.ml
+++ b/tests/misc/version.ml
@@ -17,4 +17,4 @@ let run () =
Kernel.abort
"could not parse Fc_config.version"
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/misc/vis_queueInstr.ml b/tests/misc/vis_queueInstr.ml
index eef216849e8..6b4473fae3d 100644
--- a/tests/misc/vis_queueInstr.ml
+++ b/tests/misc/vis_queueInstr.ml
@@ -4,5 +4,5 @@ class vis prj = object(this)
end
let () =
- Db.Main.extend (fun () ->
+ Boot.Main.extend (fun () ->
ignore (File.create_project_from_visitor "A" (new vis)))
diff --git a/tests/misc/vis_spec.ml b/tests/misc/vis_spec.ml
index d8d0b2b0373..b1f013cf8a5 100644
--- a/tests/misc/vis_spec.ml
+++ b/tests/misc/vis_spec.ml
@@ -48,4 +48,4 @@ let startup () =
Project.set_current prj;
;;
-let () = Db.Main.extend startup
+let () = Boot.Main.extend startup
diff --git a/tests/misc/visitor_creates_func_bts_1349.ml b/tests/misc/visitor_creates_func_bts_1349.ml
index 44d7b7cae63..ad70dd8cd73 100644
--- a/tests/misc/visitor_creates_func_bts_1349.ml
+++ b/tests/misc/visitor_creates_func_bts_1349.ml
@@ -44,4 +44,4 @@ let run () =
let vis prj = new test prj in
ignore (File.create_project_from_visitor "test" vis)
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/misc/well_typed_alarm.ml b/tests/misc/well_typed_alarm.ml
index 6c792a3d3ee..e9a1d1ba346 100644
--- a/tests/misc/well_typed_alarm.ml
+++ b/tests/misc/well_typed_alarm.ml
@@ -3,4 +3,4 @@ let main () =
Filecheck.check_ast "Check alarm";
File.pretty_ast ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/misc/with space/module.ml b/tests/misc/with space/module.ml
index b9c45d54b4c..47e5c94e5b2 100644
--- a/tests/misc/with space/module.ml
+++ b/tests/misc/with space/module.ml
@@ -1,3 +1,3 @@
-let () = Db.Main.extend (fun () ->
+let () = Boot.Main.extend (fun () ->
Kernel.feedback "module successfully loaded"
)
diff --git a/tests/misc/wstring_phase6.ml b/tests/misc/wstring_phase6.ml
index a7a36476e7b..f1e33d6a26e 100644
--- a/tests/misc/wstring_phase6.ml
+++ b/tests/misc/wstring_phase6.ml
@@ -19,4 +19,4 @@ class vis =
let do_it () = Visitor.visitFramacFileSameGlobals (new vis) (Ast.get())
-let () = Db.Main.extend do_it
+let () = Boot.Main.extend do_it
diff --git a/tests/pdg/dyn_dpds.ml b/tests/pdg/dyn_dpds.ml
index 5bf2774757d..70498a8b9d7 100644
--- a/tests/pdg/dyn_dpds.ml
+++ b/tests/pdg/dyn_dpds.ml
@@ -42,4 +42,4 @@ let main _ =
Format.printf "%a@." (Pdg.Api.pretty ~bw:false) pdg;
Pdg.Api.extract pdg "dyn_dpds_1.dot"
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/pdg/sets.ml b/tests/pdg/sets.ml
index 23c627b3a5b..c19687a8e02 100644
--- a/tests/pdg/sets.ml
+++ b/tests/pdg/sets.ml
@@ -54,4 +54,4 @@ let main _ =
pp_nodes "Test [all_related_nodes] y@11" nodes
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/rte/compute_annot.ml b/tests/rte/compute_annot.ml
index 7ef362bb586..213681f5ea0 100644
--- a/tests/rte/compute_annot.ml
+++ b/tests/rte/compute_annot.ml
@@ -38,4 +38,4 @@ let main () =
print ();
print_status ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/rte/my_annot_proxy.ml b/tests/rte/my_annot_proxy.ml
index cd22de24d55..544cedc524d 100644
--- a/tests/rte/my_annot_proxy.ml
+++ b/tests/rte/my_annot_proxy.ml
@@ -36,4 +36,4 @@ let main () =
print ();
print_status ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/rte/my_annotation.ml b/tests/rte/my_annotation.ml
index c1549b69296..7a845bfc814 100644
--- a/tests/rte/my_annotation.ml
+++ b/tests/rte/my_annotation.ml
@@ -49,4 +49,4 @@ let main () =
print () ;
print_status ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/rte/rte_get_annot.ml b/tests/rte/rte_get_annot.ml
index c360664de0d..0ffabb44622 100644
--- a/tests/rte/rte_get_annot.ml
+++ b/tests/rte/rte_get_annot.ml
@@ -53,4 +53,4 @@ let main () =
print () ;
Globals.Functions.iter show_rte_of_kf
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/saveload/deps_E.ml b/tests/saveload/deps_E.ml
index 1e5347ab012..a0a766521b2 100644
--- a/tests/saveload/deps_E.ml
+++ b/tests/saveload/deps_E.ml
@@ -37,4 +37,4 @@ let main () =
assert (StateB.get_option () = None); (* reset to default *)
assert (StateC.get_option () = None) (* reset because of dependency of B *)
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/saveload/load_one.ml b/tests/saveload/load_one.ml
index 12d0bb16cd9..02186193baa 100644
--- a/tests/saveload/load_one.ml
+++ b/tests/saveload/load_one.ml
@@ -13,7 +13,7 @@ let main () =
let p = Project.load fp in
Project.on p (fun () -> Eva.Analysis.compute (); ignore (sparecode ())) ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(* testing Project.create_by_copy *)
let main2 () =
@@ -24,4 +24,4 @@ let main2 () =
Format.printf "COPY AST@.";
File.pretty_ast ~prj ()
-let () = Db.Main.extend main2
+let () = Boot.Main.extend main2
diff --git a/tests/saveload/multi_project.ml b/tests/saveload/multi_project.ml
index 4a7bd87831f..ba7f105b8e6 100644
--- a/tests/saveload/multi_project.ml
+++ b/tests/saveload/multi_project.ml
@@ -23,4 +23,4 @@ let main () =
check "default" (<>);
check "bar" (<>)
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/saveload/status.ml b/tests/saveload/status.ml
index 5337381c38f..1203f653da6 100644
--- a/tests/saveload/status.ml
+++ b/tests/saveload/status.ml
@@ -39,4 +39,4 @@ let main () =
end in
Visitor.visitFramacFileSameGlobals o (Ast.get ())
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/scope/bts971.ml b/tests/scope/bts971.ml
index 308f4e84faa..2f42807031b 100644
--- a/tests/scope/bts971.ml
+++ b/tests/scope/bts971.ml
@@ -63,4 +63,4 @@ let main _ =
tests ()
;;
-let _ = Db.Main.extend main
+let _ = Boot.Main.extend main
diff --git a/tests/scope/zones.ml b/tests/scope/zones.ml
index 44c8841ce20..2cdc9f2b991 100644
--- a/tests/scope/zones.ml
+++ b/tests/scope/zones.ml
@@ -64,4 +64,4 @@ let main _ =
let pp = find_ret "caller" in
compute_and_print pp "Yf"
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/slicing/adpcm.ml b/tests/slicing/adpcm.ml
index ff6515dce26..bea1c788a8d 100644
--- a/tests/slicing/adpcm.ml
+++ b/tests/slicing/adpcm.ml
@@ -12,5 +12,5 @@ let resname = "tests/slicing/adpcm.sliced" in
ignore (test "uppol2" ~do_prop_to_callers:true ~resname (select_retres));;
*)
let () =
- Db.Main.extend
+ Boot.Main.extend
(fun _ -> ignore (test "uppol2" ~do_prop_to_callers:true (select_retres)))
diff --git a/tests/slicing/anim.ml b/tests/slicing/anim.ml
index 50e23891052..d80f6eaded1 100644
--- a/tests/slicing/anim.ml
+++ b/tests/slicing/anim.ml
@@ -47,4 +47,4 @@ let main _ =
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/slicing/combine.ml b/tests/slicing/combine.ml
index 55fef497d92..363a5274467 100644
--- a/tests/slicing/combine.ml
+++ b/tests/slicing/combine.ml
@@ -66,4 +66,4 @@ let main _ =
Format.printf "After Sparecode :@.";
File.pretty_ast ~prj:proj4 ();;
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/slicing/ex_spec_interproc.ml b/tests/slicing/ex_spec_interproc.ml
index f378201635e..749bf33a9cd 100644
--- a/tests/slicing/ex_spec_interproc.ml
+++ b/tests/slicing/ex_spec_interproc.ml
@@ -107,4 +107,4 @@ let main _ =
print_project ();;
(*=========================================================================*)
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/slicing/horwitz.ml b/tests/slicing/horwitz.ml
index f8034d2bb8b..59d8909fec7 100644
--- a/tests/slicing/horwitz.ml
+++ b/tests/slicing/horwitz.ml
@@ -8,6 +8,6 @@ tests/slicing/horwitz.byte -deps tests/slicing/horwitz.c
include LibSelect;;
let () =
- Db.Main.extend
+ Boot.Main.extend
(fun _ ->
ignore (test_select_data ~do_prop_to_callers:true "incr" "*pi"));;
diff --git a/tests/slicing/mark_all_slices.ml b/tests/slicing/mark_all_slices.ml
index 368ca32111e..eecfabb85f5 100644
--- a/tests/slicing/mark_all_slices.ml
+++ b/tests/slicing/mark_all_slices.ml
@@ -70,4 +70,4 @@ let main _ =
Slicing.Api.Request.apply_all_internal ();
extract_and_print ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/slicing/merge.ml b/tests/slicing/merge.ml
index 779736380bb..59c3c785045 100644
--- a/tests/slicing/merge.ml
+++ b/tests/slicing/merge.ml
@@ -95,4 +95,4 @@ let main _ =
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/slicing/min_call.ml b/tests/slicing/min_call.ml
index 80fbe7ad125..20d9cf894b4 100644
--- a/tests/slicing/min_call.ml
+++ b/tests/slicing/min_call.ml
@@ -129,4 +129,4 @@ extract_and_print project;;
*)
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/slicing/select_by_annot.ml b/tests/slicing/select_by_annot.ml
index 39e3e6d67a0..f6c24675639 100644
--- a/tests/slicing/select_by_annot.ml
+++ b/tests/slicing/select_by_annot.ml
@@ -45,4 +45,4 @@ let main _ =
Slicing.Api.Project.pretty Format.std_formatter;
extract_and_print ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/slicing/select_simple.ml b/tests/slicing/select_simple.ml
index 3f4f91a882b..620101c3c71 100644
--- a/tests/slicing/select_simple.ml
+++ b/tests/slicing/select_simple.ml
@@ -21,4 +21,4 @@ let main _ =
ignore (test_select_data "f8" "ps->c");
ignore (test_select_data "f8" "*ps")
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/slicing/simple_intra_slice.ml b/tests/slicing/simple_intra_slice.ml
index e60a1638a7c..44324761620 100644
--- a/tests/slicing/simple_intra_slice.ml
+++ b/tests/slicing/simple_intra_slice.ml
@@ -108,4 +108,4 @@ let main _ =
Slicing.Api.Project.pretty Format.std_formatter
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/slicing/slice_no_body.ml b/tests/slicing/slice_no_body.ml
index 3987c2dbb55..1ac5530d7cf 100644
--- a/tests/slicing/slice_no_body.ml
+++ b/tests/slicing/slice_no_body.ml
@@ -58,4 +58,4 @@ let main _ =
print_project ();
extract_and_print ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/slicing/switch.ml b/tests/slicing/switch.ml
index 3ca361344c9..34757642a6d 100644
--- a/tests/slicing/switch.ml
+++ b/tests/slicing/switch.ml
@@ -7,4 +7,4 @@ let main _ =
test_select_data "main" "x";
test_select_data "main" "y";
test_select_data "main" "z"
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/spec/Extend.ml b/tests/spec/Extend.ml
index db2b0600fb0..86330eb1467 100644
--- a/tests/spec/Extend.ml
+++ b/tests/spec/Extend.ml
@@ -136,4 +136,4 @@ let run () =
Project.on prj Ast.compute ();
File.pretty_ast ~prj ()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/spec/Extend_recursive_preprocess.ml b/tests/spec/Extend_recursive_preprocess.ml
index 49ebe8a4369..e2e583cb32b 100644
--- a/tests/spec/Extend_recursive_preprocess.ml
+++ b/tests/spec/Extend_recursive_preprocess.ml
@@ -80,4 +80,4 @@ let run () =
Filecheck.check_ast "Test";
Project.set_current old
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/spec/Extend_short_print.ml b/tests/spec/Extend_short_print.ml
index 3bc2da1b356..00856164ca3 100644
--- a/tests/spec/Extend_short_print.ml
+++ b/tests/spec/Extend_short_print.ml
@@ -11,4 +11,4 @@ let process_global _ = function
| Dextended(e, _, _) -> Kernel.feedback "%a" Cil_printer.pp_short_extended e
| _ -> ()
-let () = Db.Main.extend (fun () -> Annotations.iter_global process_global)
+let () = Boot.Main.extend (fun () -> Annotations.iter_global process_global)
diff --git a/tests/spec/Type_of_term.ml b/tests/spec/Type_of_term.ml
index 30350f7bc83..2ea168c2e08 100644
--- a/tests/spec/Type_of_term.ml
+++ b/tests/spec/Type_of_term.ml
@@ -33,4 +33,4 @@ let run () =
Visitor.visitFramacFileSameGlobals (new visitor) ast
;;
-Db.Main.extend run
+Boot.Main.extend run
diff --git a/tests/spec/add_global.ml b/tests/spec/add_global.ml
index 20497076ec3..1bef94312b3 100644
--- a/tests/spec/add_global.ml
+++ b/tests/spec/add_global.ml
@@ -33,4 +33,4 @@ let transform () =
Project.on prj Filecheck.check_ast "prj";
File.pretty_ast ~prj ()
-let () = Db.Main.extend transform
+let () = Boot.Main.extend transform
diff --git a/tests/spec/assigns_from_kf.ml b/tests/spec/assigns_from_kf.ml
index 0b2db1c2597..67e0a71a357 100644
--- a/tests/spec/assigns_from_kf.ml
+++ b/tests/spec/assigns_from_kf.ml
@@ -4,4 +4,4 @@ let run () =
ignore (Annotations.funspec kf)
)
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/spec/boolean_conversion.ml b/tests/spec/boolean_conversion.ml
index a2071303368..1f592aa1cdc 100644
--- a/tests/spec/boolean_conversion.ml
+++ b/tests/spec/boolean_conversion.ml
@@ -19,4 +19,4 @@ let run () =
Visitor.visitFramacFileSameGlobals vis (Ast.get());
Filecheck.check_ast "Test"
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/spec/bts0578.ml b/tests/spec/bts0578.ml
index 594d3b71e4b..00edf14ec35 100644
--- a/tests/spec/bts0578.ml
+++ b/tests/spec/bts0578.ml
@@ -42,4 +42,4 @@ let main () =
Annotations.add_ensures Emitter.end_user kf ~stmt:!s3 post_cond;
Filecheck.check_ast "after merging code_annot and ensures"
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/spec/bts0655.ml b/tests/spec/bts0655.ml
index 6137de01c4f..515c000abbb 100644
--- a/tests/spec/bts0655.ml
+++ b/tests/spec/bts0655.ml
@@ -20,4 +20,4 @@ let run () =
let f = Ast.get () in
Visitor.visitFramacFileSameGlobals (new check_float) f
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/spec/comparison.ml b/tests/spec/comparison.ml
index b04cbf62938..c0983cdcb65 100644
--- a/tests/spec/comparison.ml
+++ b/tests/spec/comparison.ml
@@ -28,4 +28,4 @@ let run () =
Visitor.visitFramacFileSameGlobals vis (Ast.get())
;;
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/spec/default_spec_combine.ml b/tests/spec/default_spec_combine.ml
index 5c2cd6c0ccb..df156a1b321 100644
--- a/tests/spec/default_spec_combine.ml
+++ b/tests/spec/default_spec_combine.ml
@@ -28,4 +28,4 @@ let populate () =
let () = Cmdline.run_after_configuring_stage populate
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/spec/default_spec_custom.ml b/tests/spec/default_spec_custom.ml
index 964e4bd7e15..e804e3f5c15 100644
--- a/tests/spec/default_spec_custom.ml
+++ b/tests/spec/default_spec_custom.ml
@@ -48,4 +48,4 @@ let populate () =
let () = Cmdline.run_after_configuring_stage populate
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/spec/default_spec_mode.ml b/tests/spec/default_spec_mode.ml
index 1ebbd226e90..c72a69092d8 100644
--- a/tests/spec/default_spec_mode.ml
+++ b/tests/spec/default_spec_mode.ml
@@ -16,4 +16,4 @@ let run () =
Globals.Functions.iter generate_spec
[@@ warning "-3"]
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/spec/expr_to_term.ml b/tests/spec/expr_to_term.ml
index ab45132edef..981677af4b9 100644
--- a/tests/spec/expr_to_term.ml
+++ b/tests/spec/expr_to_term.ml
@@ -92,4 +92,4 @@ let compute () =
treat_fct_pred i;
end
-let () = Db.Main.extend compute
+let () = Boot.Main.extend compute
diff --git a/tests/spec/extend_extern.ml b/tests/spec/extend_extern.ml
index e5c2f208daa..4bc0b994098 100644
--- a/tests/spec/extend_extern.ml
+++ b/tests/spec/extend_extern.ml
@@ -33,4 +33,4 @@ let () = Kernel.TypeCheck.set false
let () = Kernel.Debug.set 1
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/spec/location_char.ml b/tests/spec/location_char.ml
index 59768fd96d6..49357073c1e 100644
--- a/tests/spec/location_char.ml
+++ b/tests/spec/location_char.ml
@@ -37,4 +37,4 @@ end
let main () =
Visitor.visitFramacFileSameGlobals (new print_term) (Ast.get())
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/spec/logic_functions_sets.ml b/tests/spec/logic_functions_sets.ml
index f4b2847fec3..567806c7f75 100644
--- a/tests/spec/logic_functions_sets.ml
+++ b/tests/spec/logic_functions_sets.ml
@@ -13,4 +13,4 @@ let check = function
| _ -> ()
let () =
- Db.Main.extend (fun () -> Annotations.iter_global (fun _ g -> check g))
+ Boot.Main.extend (fun () -> Annotations.iter_global (fun _ g -> check g))
diff --git a/tests/spec/loop_assigns_generated.ml b/tests/spec/loop_assigns_generated.ml
index 00739577e3d..c009bfc5e6a 100644
--- a/tests/spec/loop_assigns_generated.ml
+++ b/tests/spec/loop_assigns_generated.ml
@@ -92,4 +92,4 @@ let main () =
(Property.ip_of_code_annot_single kf s (List.hd lalloc)));
File.pretty_ast ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/spec/model.ml b/tests/spec/model.ml
index 0199a137774..7ece88634f0 100644
--- a/tests/spec/model.ml
+++ b/tests/spec/model.ml
@@ -46,4 +46,4 @@ let main () =
print_models typ;
Format.print_flush ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/spec/pp_empty_spec.ml b/tests/spec/pp_empty_spec.ml
index 220c1774a2c..69951547477 100644
--- a/tests/spec/pp_empty_spec.ml
+++ b/tests/spec/pp_empty_spec.ml
@@ -32,4 +32,4 @@ let run () =
(List.hd (Annotations.behaviors ~emitter main));
File.pretty_ast()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/spec/property_test.ml b/tests/spec/property_test.ml
index 9088cf30680..e7e19684b7d 100644
--- a/tests/spec/property_test.ml
+++ b/tests/spec/property_test.ml
@@ -74,4 +74,4 @@ let run () =
show_properties ();
Project.on prj show_properties ()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/spec/status_by_call_issue_890.ml b/tests/spec/status_by_call_issue_890.ml
index 374e927700b..78684161af9 100644
--- a/tests/spec/status_by_call_issue_890.ml
+++ b/tests/spec/status_by_call_issue_890.ml
@@ -1,3 +1,3 @@
let () =
- Db.Main.extend
+ Boot.Main.extend
(fun () -> Globals.Functions.iter Statuses_by_call.setup_all_preconditions_proxies)
diff --git a/tests/spec/type_constructors_in_env.ml b/tests/spec/type_constructors_in_env.ml
index 91848fca46b..ff32f386106 100644
--- a/tests/spec/type_constructors_in_env.ml
+++ b/tests/spec/type_constructors_in_env.ml
@@ -8,4 +8,4 @@ let run () =
with Not_found -> Kernel.fatal "A should be in the environment");
File.pretty_ast ()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/syntax/Enum_repr.ml b/tests/syntax/Enum_repr.ml
index 3346cb44b0c..d94c9bb1f23 100644
--- a/tests/syntax/Enum_repr.ml
+++ b/tests/syntax/Enum_repr.ml
@@ -18,4 +18,4 @@ let run () =
| _ -> ()
in
List.iter output f.globals
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/syntax/Refresh_visitor.ml b/tests/syntax/Refresh_visitor.ml
index b5473e4babc..1b56638f839 100644
--- a/tests/syntax/Refresh_visitor.ml
+++ b/tests/syntax/Refresh_visitor.ml
@@ -76,4 +76,4 @@ let main () =
) ();
File.pretty_ast ~prj:p ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/syntax/add_allocates.ml b/tests/syntax/add_allocates.ml
index b570e86889e..1880115f52b 100644
--- a/tests/syntax/add_allocates.ml
+++ b/tests/syntax/add_allocates.ml
@@ -1,2 +1,2 @@
let () =
- Db.Main.extend Allocates.add_allocates_nothing
+ Boot.Main.extend Allocates.add_allocates_nothing
diff --git a/tests/syntax/ast_diff_1.ml b/tests/syntax/ast_diff_1.ml
index 9cf6b01c5d5..1a85f02e294 100644
--- a/tests/syntax/ast_diff_1.ml
+++ b/tests/syntax/ast_diff_1.ml
@@ -24,4 +24,4 @@ let show_correspondances () =
Ast_diff.Kernel_function.iter show_fun;
end
-let () = Db.Main.extend show_correspondances
+let () = Boot.Main.extend show_correspondances
diff --git a/tests/syntax/ast_init.ml b/tests/syntax/ast_init.ml
index f0e57935a23..5d8f7ebcf6b 100644
--- a/tests/syntax/ast_init.ml
+++ b/tests/syntax/ast_init.ml
@@ -17,4 +17,4 @@ let run () =
Ast.compute ();
File.pretty_ast ()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/syntax/clone_test.ml b/tests/syntax/clone_test.ml
index f1d044e360c..f89efcb734e 100644
--- a/tests/syntax/clone_test.ml
+++ b/tests/syntax/clone_test.ml
@@ -5,4 +5,4 @@ let run () =
File.pretty_ast();
Filecheck.check_ast "clone"
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/syntax/copy_visitor_bts_1073.ml b/tests/syntax/copy_visitor_bts_1073.ml
index 65cfeb144d9..7a1bfb7d7bb 100644
--- a/tests/syntax/copy_visitor_bts_1073.ml
+++ b/tests/syntax/copy_visitor_bts_1073.ml
@@ -30,4 +30,4 @@ let run () =
in
File.pretty_ast ~prj ()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/syntax/copy_visitor_bts_1073_bis.ml b/tests/syntax/copy_visitor_bts_1073_bis.ml
index 7f6abc84520..bf6940f3d0c 100644
--- a/tests/syntax/copy_visitor_bts_1073_bis.ml
+++ b/tests/syntax/copy_visitor_bts_1073_bis.ml
@@ -51,5 +51,5 @@ let main () =
P.feedback "exported in new project : %s" new_proj_name
end
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
(*============================================================================*)
diff --git a/tests/syntax/formals_decl_leak.ml b/tests/syntax/formals_decl_leak.ml
index ad61b6e9d03..346158605bf 100644
--- a/tests/syntax/formals_decl_leak.ml
+++ b/tests/syntax/formals_decl_leak.ml
@@ -11,4 +11,4 @@ let check_vi_exists vi _ =
let run () =
let _ = Ast.get () in Cil.iterFormalsDecl check_vi_exists
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/syntax/func_locs.ml b/tests/syntax/func_locs.ml
index e28f0429b68..3c0d0a77a1b 100644
--- a/tests/syntax/func_locs.ml
+++ b/tests/syntax/func_locs.ml
@@ -6,4 +6,4 @@ let run () =
fname
) (Cabs2cil.func_locs ())
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/syntax/get_astinfo_bts1136.ml b/tests/syntax/get_astinfo_bts1136.ml
index e842f7e046d..405d52240d1 100644
--- a/tests/syntax/get_astinfo_bts1136.ml
+++ b/tests/syntax/get_astinfo_bts1136.ml
@@ -36,4 +36,4 @@ let main () =
Cil_datatype.Syntactic_scope.pretty kind
in List.iter do_v vars; List.iter do_v vars'
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/syntax/ghost_cv_var_decl.ml b/tests/syntax/ghost_cv_var_decl.ml
index a4715ea3d0a..c278d32a902 100644
--- a/tests/syntax/ghost_cv_var_decl.ml
+++ b/tests/syntax/ghost_cv_var_decl.ml
@@ -45,4 +45,4 @@ class visitor = object(_)
end
let () =
- Db.Main.extend (fun () -> Visitor.visitFramacFileSameGlobals (new visitor) (Ast.get ()))
+ Boot.Main.extend (fun () -> Visitor.visitFramacFileSameGlobals (new visitor) (Ast.get ()))
diff --git a/tests/syntax/ghost_parameters_formals_status.ml b/tests/syntax/ghost_parameters_formals_status.ml
index 792d21a8f44..8ed3ae99011 100644
--- a/tests/syntax/ghost_parameters_formals_status.ml
+++ b/tests/syntax/ghost_parameters_formals_status.ml
@@ -25,4 +25,4 @@ let run () =
in
Globals.Functions.iter print_info
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/syntax/logic_env_script.ml b/tests/syntax/logic_env_script.ml
index 6598804b5da..7d171a9b2a4 100644
--- a/tests/syntax/logic_env_script.ml
+++ b/tests/syntax/logic_env_script.ml
@@ -28,4 +28,4 @@ let run () =
in
Project.on prj check ()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/syntax/mutable_test.ml b/tests/syntax/mutable_test.ml
index a3c06d6424e..b72ff4783da 100644
--- a/tests/syntax/mutable_test.ml
+++ b/tests/syntax/mutable_test.ml
@@ -15,4 +15,4 @@ let main () =
(not (Cil.typeHasAttribute "const" (Cil.typeOffset x.vtype offset)))
| _ -> assert false
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/syntax/reorder.ml b/tests/syntax/reorder.ml
index 9a527c7a9a2..6848afacc1c 100644
--- a/tests/syntax/reorder.ml
+++ b/tests/syntax/reorder.ml
@@ -54,4 +54,4 @@ let run () =
File.pretty_ast ();
Filecheck.check_ast "reordered"
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/syntax/temporary_location.ml b/tests/syntax/temporary_location.ml
index 0f09f3308a6..66bc8a7fe8e 100644
--- a/tests/syntax/temporary_location.ml
+++ b/tests/syntax/temporary_location.ml
@@ -14,4 +14,4 @@ let main () =
Cil.visitCilFile (new vis :> Cil.cilVisitor) (Ast.get ())
let () =
- Db.Main.extend main
+ Boot.Main.extend main
diff --git a/tests/syntax/transient_block.ml b/tests/syntax/transient_block.ml
index 79a9fc9d245..6cde00d6b77 100644
--- a/tests/syntax/transient_block.ml
+++ b/tests/syntax/transient_block.ml
@@ -50,4 +50,4 @@ let main () =
let prj = File.create_project_from_visitor "test" (fun prj -> new vis prj) in
File.pretty_ast ~prj ()
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/syntax/typedef_multi.ml b/tests/syntax/typedef_multi.ml
index 2401972bb51..02d7c09feb1 100644
--- a/tests/syntax/typedef_multi.ml
+++ b/tests/syntax/typedef_multi.ml
@@ -2,4 +2,4 @@ let run () =
File.reorder_ast ();
File.pretty_ast ()
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/syntax/vdescr_bts1387.ml b/tests/syntax/vdescr_bts1387.ml
index 8d9bfb9491f..42d12a82dc5 100644
--- a/tests/syntax/vdescr_bts1387.ml
+++ b/tests/syntax/vdescr_bts1387.ml
@@ -12,4 +12,4 @@ class print_vdescr =
let run () = Visitor.visitFramacFileSameGlobals (new print_vdescr) (Ast.get())
-let () = Db.Main.extend run
+let () = Boot.Main.extend run
diff --git a/tests/syntax/visit_create_local.ml b/tests/syntax/visit_create_local.ml
index 8a82d9d4213..43d34b1446e 100644
--- a/tests/syntax/visit_create_local.ml
+++ b/tests/syntax/visit_create_local.ml
@@ -34,4 +34,4 @@ let main () =
Project.on prj run ();
end
-let () = Db.Main.extend main
+let () = Boot.Main.extend main
diff --git a/tests/value/unit_tests.ml b/tests/value/unit_tests.ml
index 48e3b3405bc..16b578adda7 100644
--- a/tests/value/unit_tests.ml
+++ b/tests/value/unit_tests.ml
@@ -1,3 +1,3 @@
(* Programmatic tests of Eva, run by unit_tests.i. *)
-let () = Db.Main.extend Eva.Unit_tests.run
+let () = Boot.Main.extend Eva.Unit_tests.run
--
GitLab