diff --git a/dev/size_states.ml b/dev/size_states.ml index ad62726e2b8427127497eea54cc0526c00ae650b..020f68ab4c2b4c7abe1cd1f60821069c1f91f7d8 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 9038698de7d93433908feafd913dbcf4e54507cc..3c6830100175cb5c8113e2731e20c9d196b6b9dc 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 604d1885603bcdec9502f303603e75d2be66b608..7d84275fba2ef2f6bb137ee5f8177f79066be563 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 e256faa8a32f45946288a775ea6dbcc6e25253d0..4ee00dad2e55f438854ed90ba1329ad26ceba80a 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 4cc340bc30d2c07a6417f012e124d30c0d533825..e4bd3f11a35681cd93890902c785e4568dfe897d 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 e5c74452edddbeadc9391e782b657e1b4b963dcf..5f3817778ebd052192b21669882fa288893007fb 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 3d9a51c9c604652a63f21c9a4074b6f38ff0fe5a..988275d9d341ffa6fa8695e2c56ad40c29808341 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 382621862ec580be5c3723396d727593b07e4161..cc433a923fd2668f12619f4b68c42b7459de7511 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 e688748981644b66e97171f44f68a7506821fcd4..3a289ed851cb41b7a0f6945b7218e110b0581db7 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 e01bf492151dd13574dc8b7abde0e992a417769d..23af83d0008e0a7aa763ffa46d3a70d674fb80b6 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 e46b2fe6fc2f72585dccc7fbe40618eb4ab1be43..6c15467ee648a43199b14bd1413d632392b46446 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 b498fdb3da4511bc0a74c731c6e0c88046886d00..eb80f881da9479b14529a5810dbdfe7d2f30f102 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 122d1ffdc531791aca5aa71de75a6db779882fa9..f6cfe1692742bcca7a98251eb68a66d5059ac017 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 0841af991e943fae2d37d9daf1498dc608d73ed7..7a695885327a51392c578d3d85a694179090ef98 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 8fa8244e8d460ef4f3f26ec30b6d7918b47ca0ca..fdf6111c94e02ceca8fe8e9d939a90c5919f82b7 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 1eefd2a6aafa696dbdfc11045a2169bb73eef85b..d4efc8e180a17821395a7476d9ae56fbbd7d656f 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 adc46ac9afe5f9e8de4429f4f89fef630fb99f85..77310af6265b1dc720b369cb676a8b9ae56a7736 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 adc46ac9afe5f9e8de4429f4f89fef630fb99f85..77310af6265b1dc720b369cb676a8b9ae56a7736 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 adc46ac9afe5f9e8de4429f4f89fef630fb99f85..77310af6265b1dc720b369cb676a8b9ae56a7736 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 2f5e58acc1635df6a8b03b80d2d92bc6607f00f7..843e8bfd9d228db5e290a16d877b5eb6a2ae0b3c 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 3b40425c8b0d144c33af69e31bc4f36d1497e134..e93f37b85bd6d346e81e0bf14eaf2c7460b8b218 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 23fdd74a8e17fa6daf460ff9df12a26643ccbf2d..e5f1df0f5192cf827e8e70d41c88d63317c7366a 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 017f5d7e289ec4a07bc67b936e47a9863853bfe4..94925cd99057fe55726972e3f287e1f22b9d4136 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 08f85896583e1fd650d0a0a860d5aee11dfbf5f4..e119a4018c2255402579c623632b9339b2b21078 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 fe144bb2b96ff10ef8b8f29240892e52c4dd1390..fa71e931f156b8dad9bd99cae34fab8fe65e6df2 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 67739a849f82ed036730165d3406b0b8cb91ec0d..cc589bf59371c62ef0ca4131cf413a582d155060 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 95ce1b8feb867bdd15cc0a9c7ee44ab341c5a3b0..8a58db24333455c0a4985a0cbac47e8c4e732db9 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 67792829ccc13bd7c1f32ba40da461af3555459a..d1a29f66bc4f1898ff14f15fafdd80781a075526 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 13c1a758514b42aedfc5e71c3cd884654cbfd8b7..b81b894199c01d393eda516848b3e0532d9f43b7 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 6c81b013f84c8a11d4aea07b9852af7cc1ca04f4..33f036663ac343318c2ca7e2e208eaa1a39f63eb 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 5c61595d99b3af283f52eeb3bdbad942a2f28334..bca0d3708ad9c754898d14f3b2c44edfc8bc5ef7 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 850ebb7fe74df3a1ce5164f9f724cd5d0d8e16f8..a4e5e85d31f4fcf406c56278beb2757a7f0e9eb1 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 aee5de68bf0f43530d7fad97ae8be115ad7c227a..de72e68303aecbedcf173f33f8fa3c3dcc470063 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 003c0d78fcf236517599ece74cf28a5978abb668..df9beea20f8bd31766c25136d413db7fb06a2b9f 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 26fc68df230d6d2aaac763921a1e6df2e4553232..56e64e53e6ade951ef9d5412d74de1c729815ca4 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 3e5ff2aeb18c4aa3965443546fdeeb96014b4ec9..84f9e678d825fb51539fa4cd8e315d30d0b35049 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 f93bf609e17efc98cf19d17c94995d7a188692d7..f7a1db558c624007a7d82ccc7b1cf2d61bfcb9ec 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 b643f5e21c331646a38be17b5c09630bcf0e6cd9..cc4d6ba366686a4f6dc473ffeb6f5c08b4028aeb 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 c459ac2c91b4394d82c728606ca11450aaa67cfa..24e4880f4565fafdbceaf1ffb39362c6b785a4d7 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 618b539d408c879d9008f0538ce5f1ea24119c3a..a307a06e68aab06c7783b10303ddac970d8ee536 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 176678b5e498016794add8061f174db1042246fd..9f01ac05a016a02c824b9ff66af216f565138df6 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 22b3e698f5ef07a053b2b626ec33fcebe58927d7..43e491e743369265dab22b83a593ca0db5be9728 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 84e2056534967d964bd941612b2a9f9c70add25c..2f8ae1cc9d5924c0e150e4f5ed0159e57c3c3646 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 b065d1184b534cd5020fd3365a0d50030ca940ca..ad9c1cd40ad09cb28026fe7989fdd01b3332e20d 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 d9273a0790d5e53a0f199245b637d219c8acdfc4..a182c3e78447f00fabd1964aaa995dc243975f53 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 4595aacd8a2e12f73a352451095a39c1fc055818..8c2c574f6b5bfcaed5c8bbdfd8c1a8a402c93483 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 5e7ef8e3bc1159857218f3e3e3213d97a7ee9177..8a6cf8b9e4decffdd36e809510c3ebafe2969a29 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 df3464b57135b9a7a6327735639a4232b64949e2..6b0e644de4e98c55cd9d141c0cca34318b27fa5b 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 7bb30f7433978bffd79585946e69db15bfcdbf6a..d19dc67fd9c8d531ddb7d2eb8ce2769472d273dc 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 9680545a9181782f63276fbecd1d738d3c498784..b8411106ae8e8b0a4a9b939b007b82940968129d 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 ecc7d9b45051bd034248a154eec671e6dcf52fd7..8c5bd1a2951cfa3ef9782322e59f4715491b330a 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 178682c5981788be687fbc5881856b6eda2fc160..48f2de3ef19731d8b3395f2397e273b2d5a953b1 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 643fbd6057e6cd512bce729b09b029f65113d122..8e361649e87b3e0bac19a96d240aca37b5af61ab 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 929820d1c99edbf9534a97a8b7e3f64f622ceb9d..c1413df81d4ac7039fbfbbc26cac79db2dee2694 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 27abdbadafe39fdb947327983cf2674cc6b21b2d..2019f62b4db49ceeccc28bb8f930d5def0d183b5 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 5f1039342c9246c5c2243d0b8e70a32dc5cfa17b..855dbe38cfd397c89b10a1516bf7d3195d73100a 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 52eb8613929beaab64f7de7c011f12b6a546f873..7a6617155ee3f52357b04063a1a9992e344f6003 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 2337dbdb92dda2b2c435be532a16d344557f0667..74394943bb2f274858574210d3d09ac18c8d42cc 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 04bf6496e9f681b54439603ffddf3b5dc5088272..340aec48868f73b4dc44e0ab1c994676692d07f6 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 42bcad35768e1b6f33a2f02a58d253fd36fb65f5..716d0e00e99ceaff9a1e4f7665ae73fd123c1d3d 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 b413b26e45126b3d60f2e70442d5a8a019e99351..9cfc87fef111b9a9d01dec19534ffa4ed8eea314 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 25fd111322f8f8abfc1fc2e866dc0fd388b8e707..9cb63d7e0d9696da87f1086abcbb54771e8e5313 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 4aa4ac68015e0d5c4aa32f616f850e0f41f3456a..24b8ad9579f09e0fda4f78e2437bc99392102693 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 d476d72a07963e1cdc3355c0c63857a238f92513..50bc432573eac4fecacf885f01ec8c541c11f3cd 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 eca897451ea5a8d0498ad46dc1526b67ada578f2..1823763111f162e7261f4cba82782fac30b490f9 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 db4668d7326f8d28db6b399a1ffb5d17fda5c679..4ab9acd47ce62ac91057617cf0fe1578d02c0aa6 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 3e167f78bf94d7e2e68dfd7ce6c25f60653a1ed1..369d710cdd7fdf82a6d78fc37a061e96c2e195e5 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 dd8183d8e506894079b751a435730d199ae22a04..3654187155ecb9e02f8d730dfc78bcaa4af9df44 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 c2b8ca966bd971e147c8f49ee8aeb94f7af9e0ff..168be205dbb456f3eeabff4c9990fed028d18424 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 f224e4bcfca28421dbd9967f5624a0e485d8cccb..fe51268692588c39cf096254d141c2672d8710fa 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 04d2679952d844a376299eb5e32449b829314e9a..85f19109e0f142708efddda38da2ef5813fffb8b 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 a4796d9b33bb2fdf068980b0230a25f860cba669..311f8c041013ab8b03207ae341bcaf946a947fac 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 7ef013171d3ffcb3393faadca7654fcbb964c638..e07f3b60ab1e197091d8b5bce1575e49dc8d8bd7 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 f8a486d3fe77663beff1fa0c8e18168a44c1bf7d..78dfc0eeb16cf32a9301bbb1cc595975da5b9c08 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 2d20a43cb00819d2370fd19c4a2e2db7e2b4f880..425a359bd354165fc4e26b06d8e5050f6304d030 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 453fa5f48395e14b1a3f3adcadca1228a9d2e434..1b8ed9cb196e9088339e739812e246b5d54226a8 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 a3c06d6424eeda5e5c4268f5af98c0af9fbc74ae..b72ff4783dac1d229a8a18577676f652427f6358 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 73293f6f62db4ff66140644d78c423ab6c181980..f3f0f72b3e4a76c0c8dd1369a12c864672381771 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 6ce0dc57be049a58c3884d46b551637628452564..edf9e20adaee3abddd7e38a5302f496695f26c2b 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 d9163defa210d991acf8362bd59ac34d9f9c57ac..b5eceabbdf7f201d47c6db5334cf566e3ef0675e 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 7a13be06edfa6eefa75872796092c46e78abe1f7..e75f6dac805235d5831fcb4fc83bc33c6aa3cad9 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 9be7b2b2cf3ab2debf77a764ef0d4fe04f02eecc..6996d5ed0326d36527c4ac9f2521463a66dc03b6 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 c57db98104c49e29b04fa97b48f459248f6b4fd9..8e59f646a944c1c3a4464672beced4ff5349350b 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 b4f0bdbd1988e9dee39c410f4e17810aab53f5d8..bb8b128d2960a1baded2d1a0b9fd84d5db0b14ce 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 8c18407a7c3570bca2d96930ab0f6c28d5e85865..3f9c35918acef2fdf3f119c27689c2d6d7f5fd3d 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 c3ab6699cdcf5d62e36ddf353bf4201f736b5f77..01515996ec887e0b04587bb5712cdf435c66b4d6 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 d129f05a877ac00f90d79bc0ba48f6a62591dfa1..fdcf2b0c5d8a47c3135d2f6f528f6acb034706b5 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 079fb42f5e3a8c26cb4d5b0a231a582e08ba8e61..8c1b1578e44040204b9e91c008b6e1aeb694f346 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 224c74f4289c413958bf7e141380d34e00949465..cb02f561c1223b0876d439044040e5db8240fc06 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 8cb421763f5dc9c46a3c61679a6413b458875578..9358eb15ac52523d94d9c705b142142f512702a2 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 ea417ba7710a999aa54681cf88770f622473b46f..b89b9009d34d9dc3f4a9b9fbecf6593eb6a3aca6 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 b46478f7925e914d25506a3200d3d9e87b55885f..88601d0e0687b81c0e55a8ab30421c6cd01fae49 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 c906a333c79cdbc7b004e95ccfe1496de65f0cf6..4e839e8c33766d6e92832de24c7380754ad9c3bc 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 ac7fba803c66a0b3a6d79d93cdda3118cb3d19db..cfc236e625f9057be89c97065706c7f2096c55f3 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 571edd890e7d77048cac3fd1376645a59e2eab64..3f3bdb9afceb8a130ab76fd704f4d1057cf8d08c 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 e8f5b806e8358fdc021fe1977576213b1b93f109..32771550a04aaa8a069987a52b8357872be20888 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 84eef5538f096ec0107928b835f597a9c662520d..b06b24d64dbf3c3213af4927f553fe358a0f162f 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 9843d085b1e85bbb4cca3d1c49fdb0e15fcda88b..63d674cf07ba768f453d41eb778b371ff9ba7979 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 61dfa1768fa4a977aab7240a422d22f1d46e8314..ca6ed24e40feabcb1e89b30899a15e9f04f6cfc3 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 bf97a89df6479fba8dcfeb7cb317fba07fb3f6cc..fe869a1f1bef88f9d0cb0e3d89ac24c9a7282f85 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 afe0d309b5e8b570901a9fad9eaa53b264a969ee..6e51a976ceae8728fd025e6275f8bc3ffff9fdd3 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 b64d3776a9de481781db197742c069a77e68d120..8f1c10e8d02f20232e08f2e487b89ab56b5c4771 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 43e96ba1a24aa9b14808047fb4b9f26b6b73f360..dce5e8cfc2b03a89b957de3e4c16fe25a09e3071 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 6470ee925904435745bd9ead0d9d7a33cf929d00..97678ef9abb1e9e2e6c4d626c5600abf3ac13d53 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 290543f644af55ef65b3fca95563f627c4f17f59..cf379082ec0a407dca4e3670b79adc3348741148 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 297c7fed4a45df97b8970a4a78a31a0a6d8cf6f4..9597d33f3c7dde54c9eb2d3fdac7c14f53dbbab5 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 73238757c077b193a9a5ea1cfd9be83778134585..67bb3b984883dad3a98ecfd1278272e9479da2c0 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 832c2104127e461c46e5e120a9e9868262897194..c2248a4ebc119d082c215d70662ce313ab5fe2d4 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 2fd3673ffa30e0005f7e38f8b3663104e5dce937..5c31565debc4da05f38968f730c72ef8e835f9ad 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 81908f382636d5494b21425fc938182ab0d00d38..ac6d9836317842aba5b37ac9087a2ae546aa5d5d 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 c382ddaaabc0f7b7ba73f904d9ef5b7dbbbcea1a..be52ee29bff92683bab71ee573da183e602739be 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 0c9dea658b023a88f7be802b18c95c7de552edab..cfd3e993581eef73247ed9ff74fd7172f8e33df8 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 7b6f77aa5f8f1d7d362de123ec827c53e052bd70..36c84526fddb1f700c1b64111bdd721dc93055e5 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 4787ec1dbbb58ed4ef196814ab780ea26df0b2d8..04a8eeca0ea3fe4b7cfe4b80107f238026c6e1f4 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 c51486acaecd1ccf588f1180f59d1728c5a81768..cddd787c76c38aff5d5b9bb450744645c79045fd 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 eef216849e864ac5b972d0b401683ffecbd5e7f1..6b4473fae3dfb11f25f6a96b1034d3b4f12510df 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 d8d0b2b0373de8cdb41233441db0c85f0099395b..b1f013cf8a5df9af901e113ddb89e93501582aab 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 44d7b7cae636a1d6aa880f2ff6c65c01bd1914a0..ad70dd8cd73f3a148b9de2fadff5578d38f1a1de 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 6c792a3d3ee8155beb6f9ba3c44e698f5d196a33..e9a1d1ba3467bbc39ac705f514d0133f71afa9b6 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 b9c45d54b4c46abc1b0e634ec17b6879414a0c78..47e5c94e5b2cddf1e473683678f87c99bdc50ee5 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 a7a36476e7bd7baf11e9e893971bb13722ca783b..f1e33d6a26ec54a33718c5da4afabbd862fd2f2e 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 5bf2774757d4402519d82ae1590fef2b179ca7ea..70498a8b9d7df4c2567f3f99134c210ae884c16d 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 23c627b3a5bb207fb6a40a3d1ec5fcd793dfbe3e..c19687a8e02f102cf506b5c9e39b3cbbadfdf10d 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 7ef362bb5864a62627fc589a2ee7e243e68b9e62..213681f5ea014d82deed4ebab5efbd95489efbab 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 cd22de24d55aeb20304ac0c9c47cac5a00854a52..544cedc524d73d676d906c3b45a7d20ff9296209 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 c1549b692964c6eb2732665b2848d4cb38f28a61..7a845bfc81448f019c3ee2c703902fee2aa8e709 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 c360664de0dccaa55c8c903489869ccae5dba7d7..0ffabb44622aeb623304cfb67b9fe370d316a99b 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 1e5347ab012160175d918845265e2438e3ea3532..a0a766521b2afba0e386ed2f7e13da7d93e82f9f 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 12d0bb16cd9ea6f58270a01a2cb71ed3d5042f34..02186193baa7df0b46834af0aeb7af26164b4939 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 4a7bd87831f8f3dff90580f39dff13bb9b039ad3..ba7f105b8e6435c1be4f6215f0a8b918caf8a2bd 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 5337381c38f61d7ebd21bfe3dd76abd77f937f0b..1203f653da673aa02b8e30ade126e5ed44a2a880 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 308f4e84faac142bf859f27f65f499b5d4aa70fc..2f42807031bdccf95eeb08e69fc0774381810d31 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 44c8841ce20ff11081d17df4ce27678a661ef8a5..2cdc9f2b99108fa1448c43793ada568d86a66a2f 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 ff6515dce26737dc4355e611a7eaeca836bd31d8..bea1c788a8db4d25ed8d4337915b2a808a6289a3 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 50e23891052592eb8f602c19bb18a5990e8c8740..d80f6eaded10b3c578372359d019b0219dc4f72c 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 55fef497d923a4e9cba21e14e64d1b0174829bc4..363a52744674203eb654ba925d0ddcd543241187 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 f378201635ea019df2276d1c0ec0c8bea7ed1952..749bf33a9cd6b05cbd4389a7c1f10fb8cfa64fb0 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 f8034d2bb8bfe58794f7aee9d97fa09214159c64..59d8909fec7affa744ce0427e937dbcd6bf08266 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 368ca32111e0e6c146a934c0a1ad3c7f3bf02b98..eecfabb85f5754b981b19e5b9a74d37fecbfb142 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 779736380bbeacedb289bdd76ba997d4da072c04..59c3c7850452178fea83a2e65f9d7878a12b75ec 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 80fbe7ad12575a7cf978e0441508b3fec992676d..20d9cf894b4313e8de955b113d1856183320df45 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 39e3e6d67a0bbda7190384523b629ca7b7ba20b9..f6c24675639034770580bd80540ddadde8624ba1 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 3f4f91a882baf5854948d5ae40233726b28d64ec..620101c3c7112425f8722af6cb47975778dcc1a3 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 e60a1638a7c80ed04c83d6de012bcb1146ace84e..44324761620faf36c046e3895eb3710b00e0b2dc 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 3987c2dbb5549f1e1cb5a3f78a8f52bbbf2f909c..1ac5530d7cf37a47366539cc2bca97124630a18b 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 3ca361344c91d376826f603ced718685d0c257ac..34757642a6d327507f33b708517a67ae9b8dbb33 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 db2b0600fb056e3493e2567ff559ebaf3b460813..86330eb14674168bdf7439fa582fbdd6d7b0353d 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 49ebe8a4369d0367afcecc959f034e61381861d1..e2e583cb32bc19ed1e21ae061cc3983296b2c2b1 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 3bc2da1b356c7916b579cc72d42623b0409a4f5b..00856164ca3523766c133b6b89918d6ad4055323 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 30350f7bc83682ce293385dccfec0cbbb1015729..2ea168c2e08b9f3f21fb2a041d1d69bf10cc60cb 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 20497076ec3e57581978dddbee179f5355356a45..1bef94312b3bc740c7a8912c2ac415329b49fef6 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 0b2db1c2597924a3f4fd195103ad2ad8c2927047..67e0a71a3574101028de48cc2540f7b24aaaec63 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 a2071303368c92bef6b1bcec891ca5ca807a365e..1f592aa1cdc112703551aa5da04e17868a0eaf4b 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 594d3b71e4b03b506173990f569c70b3ae21ddcf..00edf14ec350c23d5eea437c613119917a2df405 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 6137de01c4f3443ed4e811608d4a18ca94de7a6f..515c000abbb03468a37d8053daf74328951a6dd1 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 b04cbf629387bf88dfc337863dfbed17b492e2bb..c0983cdcb65cb77e13f02aee58e6add4245c564c 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 5c2cd6c0ccbc488e12917a4b33ba866d09b1d65a..df156a1b321f7feedff45c526870173b42af5b6c 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 964e4bd7e1546e51f9b1d0424ecc7e2fdec5d000..e804e3f5c1573dd4803d79cafbee2b0f16952fc6 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 1ebbd226e9059736d7af1124fb3f44f65f4925b2..c72a69092d8540bddd292d152a0a05669fbe2737 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 ab45132edef74fda692787fbfbbb8eb75acf6832..981677af4b9157cbaf129644343cbec9bc1386a9 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 e5c2f208daa0da69b050079e2917b19e417fc40d..4bc0b994098b02e948cb1d2a4e3d9e19f6d23bfd 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 59768fd96d6e2f7a79f844c3eb7514e5b84a7b57..49357073c1e86bb4f2a7e09de2bc0e6d52f912ac 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 f4b2847fec3e10ff5d3b6fd673406b363e403ffd..567806c7f75335fa50180b7624b8e1cc0d195021 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 00739577e3d845c29c86de1d3c6658fa34b6365f..c009bfc5e6ac4bf85dff53210803700de65c5375 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 0199a1377741054724df687749950ae71605b6dd..7ece88634f085734c53e16ef24f9843a72f2c333 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 220c1774a2c1ca3265ff87578f56edb13604456f..699515474771c8e719f14761632ef752c05cdccb 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 9088cf306802455e82893b4042ccd39921790e5c..e7e19684b7d1b7b4e3bb696186b2d92aea2a34ac 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 374e927700b937885f27c029f3d1744110d9ea39..78684161af938b737b54fd6b718cc7eb2cfb86bb 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 91848fca46bde9e68c9fa474f0419c94aa6d9ddf..ff32f386106f7cd0cd33a7ffc18ea3906bd533b2 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 3346cb44b0cf42d98bf275a8489e244f30513bf6..d94c9bb1f232e49dcf6c57f807b83c1f19646711 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 b5473e4babc253445b1cdc78594f3b683f93830d..1b56638f8397f1b0f0a0e00166a077318899bc8c 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 b570e86889e229bf1528d4ef585196420363f2fd..1880115f52bfa921012297675a888f31d9c08b6f 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 9cf6b01c5d5a3c04b1e180846e05ad48883ebc5b..1a85f02e29488f26c4e06a1b0359cbc4a2307f6c 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 f0e57935a236f696af9949647edb7ec78d06fb81..5d8f7ebcf6bde4c0fe0a7d1547807ee631af983a 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 f1d044e360ca5c10d475483b4dbee281e77758cf..f89efcb734e8e2c7a140bffe411ab5c2492be129 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 65cfeb144d9e11ed0dff43387c254d8ff4088af3..7a1bfb7d7bb59e2bcac99a3d28155ca89f05c12e 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 7f6abc845200d0eceff40365c3c812cd702b3632..bf6940f3d0c048aaf94c70102fad611d99921108 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 ad61b6e9d03a365784d31010f6c2f3aae5a09eec..346158605bf084d856b40e9a985df3d5d141fd96 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 e28f0429b68ca220b12e37f15c4417edc32179c6..3c0d0a77a1bd9f39dfe5df3ef39a6cc3acd7236e 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 e842f7e046d687f023eca1e6c8563c03d6d33ccf..405d52240d1ae4ed4f237f8bb9d5f0c095cde338 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 a4715ea3d0a87386c4ab6add6fb877e37c9bf7fe..c278d32a902345b7364575590f67e3b9fcdd3c9f 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 792d21a8f44538b02c681ebff028fc22208362c8..8ed3ae99011d09628bbcc9fc3412c3312970f26d 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 6598804b5dabf33d46bd35e748643f5f99661364..7d171a9b2a4f9e9001615ed475f36b72c7a8fac8 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 a3c06d6424eeda5e5c4268f5af98c0af9fbc74ae..b72ff4783dac1d229a8a18577676f652427f6358 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 9a527c7a9a2d98e168b6a14ec29b3d449ff65dcc..6848afacc1c2a89a43e0aa9069a217f0d6d5aeaa 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 0f09f3308a6ece20e90940de47f88beb9e0c89a0..66bc8a7fe8e4b3b30b89ebb6cb8506f82d04e902 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 79a9fc9d24574aa3c8154e3e0e57aeda1f7360d4..6cde00d6b77403522c495807ceff448292603451 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 2401972bb518c95055702f302615bf86e0814697..02d7c09feb1a5838b0a4a873c699b25efd257e77 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 8d9bfb9491f63f97f6b8d852dc4f8e6e6f46b072..42d12a82dc52596779d95c5794c5708da7caed8f 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 8a82d9d421339f8c89731d786fd60bc2d32dd017..43d34b1446e424d49725c174d632129fe6e03a3b 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 48e3b3405bcb13af995b3a50f15aebaa64b09b54..16b578adda73105011b362ed629cff2ffbb6a9c2 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