From 342358fd654b35460ceb729e0b535d7934bb733f Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 31 Jul 2009 08:18:01 +0000
Subject: [PATCH] fixed bug occuring with 'frama-c -verbose'
---
src/kernel/boot.ml | 44 +++++-----------------
src/kernel/cmdline.ml | 84 ++++++++++++++++++++++++++++++++----------
src/kernel/cmdline.mli | 2 +
src/lib/extlib.ml | 5 ++-
4 files changed, 78 insertions(+), 57 deletions(-)
diff --git a/src/kernel/boot.ml b/src/kernel/boot.ml
index 933131d50d9..7be2822b8b3 100644
--- a/src/kernel/boot.ml
+++ b/src/kernel/boot.ml
@@ -73,41 +73,15 @@ let () =
Kind.version := Config.version;
boot_cil ();
Sys.catch_break true;
- try
- Journal.set_name (Parameters.Journal.Name.get ());
- ignore (Project.create "default");
- Cmdline.parse_and_boot (fun () -> !Db.Toplevel.run) run_plugins;
- Plugin.run_normal_exit_hook ();
- exit 0 (* ensure that nothing occurs after booting: no other file can be
- linked after boot.ml *)
- with
- | Cmdline.Exit ->
- Plugin.run_normal_exit_hook ();
- exit 0
- | Log.AbortError s ->
- Parameters.error
- "%s failed to complete because of an invalid user input"
- s;
- exit 1
- | Log.AbortFatal s when Parameters.Debug.get () = 0 ->
- (* do it only in non-debugging mode:
- get a backtrace if you are debugging. *)
- Parameters.error
- "%s failed to complete because of an unexpected internal error.
-please report at http://bts.frama-c.com"
- s;
- exit 2
- | Sys.Break when Parameters.Debug.get () = 0 -> (* User interuption *)
- Parameters.error "stopped on user request";
- exit 3
- | e when Parameters.Debug.get () = 0 ->
- (* do it only in non-debugging mode:
- get a backtrace if you are debugging. *)
- Parameters.error
- "unexpected error %s
-please report as `crash' at http://bts.frama-c.com"
- (Printexc.to_string e);
- exit 4
+ Cmdline.catch_toplevel_run
+ (fun () ->
+ Journal.set_name (Parameters.Journal.Name.get ());
+ ignore (Project.create "default");
+ Cmdline.parse_and_boot (fun () -> !Db.Toplevel.run) run_plugins)
+ (fun () ->
+ Plugin.run_normal_exit_hook ();
+ exit 0 (* ensure that nothing occurs after booting: no other file can be
+ linked after boot.ml *))
(*
Local Variables:
diff --git a/src/kernel/cmdline.ml b/src/kernel/cmdline.ml
index 54d3c64aad0..6c666438baa 100644
--- a/src/kernel/cmdline.ml
+++ b/src/kernel/cmdline.ml
@@ -58,6 +58,44 @@ module L =
end)
include L
+(** {2 Exiting Frama-C} *)
+
+type exit = unit
+exception Exit
+let nop = ()
+
+let catch_toplevel_run f at_normal_exit =
+ try
+ f ();
+ at_normal_exit ()
+ with
+ | Exit ->
+ at_normal_exit ()
+ | Log.AbortError s ->
+ L.error
+ "%s failed to complete because of an invalid user input"
+ s;
+ exit 1
+ | Log.AbortFatal s when !debug_level_ref = 0 ->
+ (* do it only in non-debugging mode:
+ get a backtrace if you are debugging. *)
+ L.error
+ "%s failed to complete because of an unexpected internal error.
+please report at http://bts.frama-c.com"
+ s;
+ exit 2
+ | Sys.Break when !debug_level_ref = 0 -> (* User interuption *)
+ L.error "stopped on user request";
+ exit 3
+ | e when !debug_level_ref = 0 ->
+ (* do it only in non-debugging mode:
+ get a backtrace if you are debugging. *)
+ L.error
+ "unexpected error %s
+please report as `crash' at http://bts.frama-c.com"
+ (Printexc.to_string e);
+ exit 4
+
(** {2 Generic parsing way} *)
type option_setting =
@@ -71,8 +109,9 @@ let raise_error name because = raise (Cannot_parse(name, because))
let error name msg =
let bin_name = Sys.argv.(0) in
- L.abort "option `%s' %s.@\nuse `%s -help' for more information." name msg bin_name
-
+ L.abort
+ "option `%s' %s.@\nuse `%s -help' for more information."
+ name msg bin_name
let all_options = match Array.to_list Sys.argv with
| [] -> assert false
@@ -148,20 +187,29 @@ let parse known_options_list options_list =
(** {2 First parsing stage at the very beginning of the initialization step} *)
-let non_initial_options =
- fst
- (parse
- [ "-debug",
- Int (fun n -> debug_level_ref := n; debug_isset_ref := true);
- "-quiet", Unit (fun () -> quiet_ref := true);
- "-journal-enable", Unit (fun () -> journal_enable_ref := true);
- "-journal-disable", Unit (fun () -> journal_enable_ref := false);
- "-journal-name", String (fun s -> journal_name_ref := s);
- "-no-obj", Unit (fun () -> use_obj_ref := false);
- "-no-type", Unit (fun () -> use_type_ref := false);
- "-verbose",
- Int (fun n -> verbose_level_ref := n; verbose_isset_ref := true) ]
- all_options)
+let non_initial_options_ref = ref []
+
+let () =
+ let first_parsing_stage () =
+ fst
+ (parse
+ [ "-debug",
+ Int (fun n -> debug_level_ref := n; debug_isset_ref := true);
+ "-quiet", Unit (fun () -> quiet_ref := true);
+ "-journal-enable", Unit (fun () -> journal_enable_ref := true);
+ "-journal-disable", Unit (fun () -> journal_enable_ref := false);
+ "-journal-name", String (fun s -> journal_name_ref := s);
+ "-no-obj", Unit (fun () -> use_obj_ref := false);
+ "-no-type", Unit (fun () -> use_type_ref := false);
+ "-verbose",
+ Int (fun n -> verbose_level_ref := n; verbose_isset_ref := true) ]
+ all_options)
+ in
+ catch_toplevel_run
+ (fun () -> non_initial_options_ref := first_parsing_stage ())
+ (fun () -> ())
+
+let non_initial_options = !non_initial_options_ref
let () =
if not !use_obj_ref then use_type_ref := false;
@@ -280,10 +328,6 @@ end
let add_plugin = Plugin.add
-type exit = unit
-exception Exit
-let nop = ()
-
module Make_Stage(S: sig val exclusive: bool val name: string end) = struct
let nb_actions = ref 0
diff --git a/src/kernel/cmdline.mli b/src/kernel/cmdline.mli
index 56c06f58d0f..65a64c8ada0 100644
--- a/src/kernel/cmdline.mli
+++ b/src/kernel/cmdline.mli
@@ -79,6 +79,8 @@ val run_after_configuring_stage: (unit -> unit) -> unit
@plugin development guide
@since Beryllium-20090601-beta1 *)
+val catch_toplevel_run: (unit -> unit) -> (unit -> unit) -> unit
+
(** {2 Special functions}
These functions should not be used by a standard plug-in developer. *)
diff --git a/src/lib/extlib.ml b/src/lib/extlib.ml
index 34a5d3a678c..6c039d4a174 100644
--- a/src/lib/extlib.ml
+++ b/src/lib/extlib.ml
@@ -110,13 +110,14 @@ external getperfcount1024: unit -> int = "getperfcount1024"
external address_of_value: 'a -> int = "address_of_value"
-
let try_finally ~finally f x =
try
let r = f x in
finally ();
r
- with e -> finally () ; raise e
+ with e ->
+ finally ();
+ raise e
let full_command cmd args ~stdin ~stdout ~stderr =
let pid = Unix.create_process cmd args stdin stdout stderr in
--
GitLab