diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index 09d04639e829e0f8edd3baad947cdddf0af58241..a932d0eebdcf98c0dc1a21575316dd7a9cb5208b 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -113,20 +113,25 @@ let post_analysis () =
(* Remove redundant alarms *)
if Value_parameters.RmAssert.get () then !Db.Value.rm_asserts ()
-(* Register a signal handler for SIGUSR1, that will be used to abort Value *)
-let () =
- let prev = ref (fun _ -> ()) in
- let handler (_signal: int) =
- !prev Sys.sigusr1; (* Call previous signal handler *)
- Value_parameters.warning "Stopping analysis at user request@.";
- Iterator.signal_abort ()
+(* Registers signal handlers for SIGUSR1 and SIGINT to cleanly abort the Eva
+ analysis. Returns a function that restores previous signal behaviors after
+ the analysis. *)
+let register_signal_handler () =
+ let warn () =
+ Value_parameters.warning ~once:true "Stopping analysis at user request@."
in
- try
- match Sys.signal Sys.sigusr1 (Sys.Signal_handle handler) with
- | Sys.Signal_default | Sys.Signal_ignore -> ()
- | Sys.Signal_handle f -> prev := f
- with Invalid_argument _ -> () (* Ignore: SIGURSR1 is not available on Windows,
- and possibly on other platforms. *)
+ let stop _ = warn (); Iterator.signal_abort () in
+ let interrupt _ = warn (); raise Sys.Break in
+ let register_handler signal handler =
+ match Sys.signal signal (Sys.Signal_handle handler) with
+ | previous_behavior -> fun () -> Sys.set_signal signal previous_behavior
+ | exception Invalid_argument _ -> fun () -> ()
+ (* Ignore: SIGURSR1 is not available on Windows,
+ and possibly on other platforms. *)
+ in
+ let restore_sigusr1 = register_handler Sys.sigusr1 stop in
+ let restore_sigint = register_handler Sys.sigint interrupt in
+ fun () -> restore_sigusr1 (); restore_sigint ()
module Make (Abstract: Abstractions.Eva) = struct
@@ -327,7 +332,8 @@ module Make (Abstract: Abstractions.Eva) = struct
Db.Value.Call_Value_Callbacks.apply (cvalue_state, [kf, Kglobal])
let compute kf init_state =
- try
+ let restore_signals = register_signal_handler () in
+ let compute () =
Value_util.push_call_stack kf Kglobal;
store_initial_state kf init_state;
let call =
@@ -344,10 +350,13 @@ module Make (Abstract: Abstractions.Eva) = struct
post_analysis ();
Abstract.Dom.post_analysis final_state;
Value_results.print_summary ();
- with Log.AbortError _ | Log.AbortFatal _ | Log.FeatureRequest _ as e ->
+ restore_signals ()
+ in
+ let cleanup () =
Abstract.Dom.Store.mark_as_computed ();
- post_analysis_cleanup ~aborted:true;
- raise e
+ post_analysis_cleanup ~aborted:true
+ in
+ Value_util.protect compute ~cleanup
let compute_from_entry_point kf ~lib_entry =
pre_analysis ();
@@ -355,10 +364,9 @@ module Make (Abstract: Abstractions.Eva) = struct
(if lib_entry then "n in" else " ")
Kernel_function.pretty kf;
let initial_state =
- try Init.initial_state_with_formals ~lib_entry kf
- with Log.AbortError _ | Log.AbortFatal _ | Log.FeatureRequest _ as e ->
- post_analysis_cleanup ~aborted:true;
- raise e
+ Value_util.protect
+ (fun () -> Init.initial_state_with_formals ~lib_entry kf)
+ ~cleanup:(fun () -> post_analysis_cleanup ~aborted:true)
in
match initial_state with
| `Bottom ->
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index 6f1f546680aa2eb4d61cbe7716d2911c0f21dc3a..933035419a65831bb45ff24fc2c41ae84fd27181 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -29,7 +29,7 @@ let check_signals, signal_abort =
(fun () ->
if !signal_emitted then begin
signal_emitted := false;
- raise (Log.AbortError "eva")
+ raise Sys.Break
end),
(fun () -> signal_emitted := true)
@@ -765,7 +765,7 @@ module Computer
end)
()
in
- try
+ let compute () =
let results = Dataflow.compute () in
if Value_parameters.ValShowProgress.get () then
Value_parameters.feedback "Recording results for %a"
@@ -779,11 +779,12 @@ module Computer
Kernel_function.pretty kf;
| _ -> ());
results, !Dataflow.cacheable
- with Log.AbortError _ | Log.AbortFatal _ | Log.FeatureRequest _ as e ->
- (* analysis was aborted: pop the call stack and inform the caller *)
+ in
+ let cleanup () =
Dataflow.mark_degeneration ();
- Dataflow.merge_results ();
- raise e
+ Dataflow.merge_results ()
+ in
+ Value_util.protect compute ~cleanup
end
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 874b2b65af01462ba3bfc492638d958e221e30be..f18e4c385e8a192ee184d3e37392c7b49b15844c 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -319,7 +319,7 @@ module Make (Abstract: Abstractions.Eva) = struct
(* Changed by compute_call_ref, called from process_call *)
Cil.CurrentLoc.set (Cil_datatype.Stmt.loc stmt);
in
- try
+ let process () =
let domain_valuation = Eval.to_domain_valuation valuation in
let res =
(* Process the call according to the domain decision. *)
@@ -332,10 +332,9 @@ module Make (Abstract: Abstractions.Eva) = struct
in
cleanup ();
res
- with Log.AbortError _ | Log.AbortFatal _ | Log.FeatureRequest _ as e ->
- InOutCallback.clear ();
- cleanup ();
- raise e
+ in
+ Value_util.protect process
+ ~cleanup:(fun () -> InOutCallback.clear (); cleanup ())
(* ------------------- Retro propagation on formals ----------------------- *)
diff --git a/src/plugins/value/utils/value_util.ml b/src/plugins/value/utils/value_util.ml
index 13a005dd2afb149c347bfdd8ed45f51fd90b3262..9f7ddc3f46156c55e8a3159cd15db1058b988464 100644
--- a/src/plugins/value/utils/value_util.ml
+++ b/src/plugins/value/utils/value_util.ml
@@ -107,6 +107,22 @@ module DegenerationPoints =
let dependencies = [ Db.Value.self ]
end)
+let protect_only_once = ref true
+
+let protect f ~cleanup =
+ let catch () = !protect_only_once && not (Kernel.SaveState.is_empty ()) in
+ try f ();
+ with
+ | Log.AbortError _ | Log.AbortFatal _ | Log.FeatureRequest _
+ | Sys.Break as e when catch () ->
+ try
+ Value_parameters.feedback ~once:true "Clean up and save partial results.";
+ cleanup ();
+ raise e;
+ with e ->
+ protect_only_once := false;
+ raise e
+
let register_new_var v typ =
if Cil.isFunctionType typ then
Globals.Functions.replace_by_declaration (Cil.empty_funspec()) v v.vdecl
diff --git a/src/plugins/value/utils/value_util.mli b/src/plugins/value/utils/value_util.mli
index 0bfe89cbe916816878319417b0dc123ad79bea1c..c99393d8885d66b5e1e11023582e3b7b797f05c7 100644
--- a/src/plugins/value/utils/value_util.mli
+++ b/src/plugins/value/utils/value_util.mli
@@ -51,6 +51,11 @@ val warning_once_current : ('a, Format.formatter, unit) format -> 'a
status associated to {!Value_parameters.wkey_alarm} *)
val alarm_report: 'a Log.pretty_printer
+(** [protect f ~cleanup] runs [f]. On a user interruption or a Frama-C error,
+ if option -save is set, applies [cleanup]. This is used to clean up and
+ save partial results when the analysis is aborted. *)
+val protect: (unit -> 'a) -> cleanup:(unit -> unit) -> 'a
+
(* Statements for which the analysis has degenerated. [true] means that this is
the statement on which the degeneration occurred, or a statement above in
the callstack *)
diff --git a/tests/fc_script/oracle/make-wrapper.res b/tests/fc_script/oracle/make-wrapper.res
index 09358673bd043241721520d914345a9a782b35d5..8370fe5e49498ce18397bc847647adac6ce49eaf 100644
--- a/tests/fc_script/oracle/make-wrapper.res
+++ b/tests/fc_script/oracle/make-wrapper.res
@@ -25,6 +25,7 @@ Command: ../../bin/frama-c -kernel-warn-key annot:missing-spec=abort -kernel-war
[kernel:annot:missing-spec] make-wrapper.c:13: Warning:
Neither code nor specification for function large_name_to_force_line_break_in_stack_msg, generating default assigns from the prototype
[kernel] User Error: warning annot:missing-spec treated as fatal error.
+[eva] Clean up and save partial results.
[kernel] Frama-C aborted: invalid user input.
[kernel] Warning: attempting to save on non-zero exit code: modifying filename into `PWD/make-for-make-wrapper.eva/framac.sav.error'.