fixed bug occuring with 'frama-c -verbose'

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:

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

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. *)

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