diff --git a/src/plugins/loop_analysis/tests/loop_analysis/oracle/with_value.res.oracle b/src/plugins/loop_analysis/tests/loop_analysis/oracle/with_value.res.oracle
index 504e31673b11bfc0d47a0708faa9b08494ca9d5c..2532c0705debdae0c04bd3b145d657e2f7699ac2 100644
--- a/src/plugins/loop_analysis/tests/loop_analysis/oracle/with_value.res.oracle
+++ b/src/plugins/loop_analysis/tests/loop_analysis/oracle/with_value.res.oracle
@@ -412,6 +412,18 @@
   i ∈ {-154}
 [eva:final-states] Values at end of function main:
   __retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  46 functions analyzed (out of 46): 100% coverage.
+  In these functions, 329 statements reached (out of 329): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  22 alarms generated by the analysis:
+      22 integer overflows
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 [loop] Functions with loops whose bounds we could not find:
   g1
   g2
diff --git a/src/plugins/nonterm/tests/test_config b/src/plugins/nonterm/tests/test_config
index 32af202375114b2ca25b608d6a16a5ef3bef3d9f..1d678ae3e1a635f06f7c8fbf7e30a0da5d6f7ffe 100644
--- a/src/plugins/nonterm/tests/test_config
+++ b/src/plugins/nonterm/tests/test_config
@@ -1 +1 @@
-OPT: -no-autoload-plugins -load-module from,inout,nonterm,scope -val -val-show-progress -then -nonterm -nonterm-verbose 2
+OPT: -no-autoload-plugins -load-module from,inout,nonterm,scope -val -val-show-progress -eva-msg-key=-summary -then -nonterm -nonterm-verbose 2
diff --git a/src/plugins/report/tests/report/oracle/csv.res.oracle b/src/plugins/report/tests/report/oracle/csv.res.oracle
index 639393b8a5af4fca82b1c0e8bdd05cbf4a74a955..aaf1752f36f4d2a5614f9f35f6bd27d7e986d277 100644
--- a/src/plugins/report/tests/report/oracle/csv.res.oracle
+++ b/src/plugins/report/tests/report/oracle/csv.res.oracle
@@ -67,6 +67,26 @@
   r ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
 [eva:final-states] Values at end of function main:
   
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  5 functions analyzed (out of 5): 100% coverage.
+  In these functions, 23 statements reached (out of 23): 100% coverage.
+  ----------------------------------------------------------------------------
+  Some errors and warnings have been raised during the analysis:
+    by the Eva analyzer:      0 errors    0 warnings
+    by the Frama-C kernel:    0 errors    1 warning
+  ----------------------------------------------------------------------------
+  7 alarms generated by the analysis:
+       2 accesses out of bounds index
+       2 integer overflows
+       2 accesses to uninitialized left-values
+       1 nan or infinite floating-point value
+  ----------------------------------------------------------------------------
+  Evaluation of the logical properties reached by the analysis:
+    Assertions        0 valid     0 unknown     0 invalid      0 total
+    Preconditions     2 valid     4 unknown     1 invalid      7 total
+  28% of the logical properties reached have been proven.
+  ----------------------------------------------------------------------------
 [report] Dumping properties in 'tests/report/result/csv.csv'
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
@@ -152,3 +172,23 @@
   r ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
 [eva:final-states] Values at end of function main:
   
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  5 functions analyzed (out of 5): 100% coverage.
+  In these functions, 23 statements reached (out of 23): 100% coverage.
+  ----------------------------------------------------------------------------
+  Some errors and warnings have been raised during the analysis:
+    by the Eva analyzer:      0 errors    0 warnings
+    by the Frama-C kernel:    0 errors    1 warning
+  ----------------------------------------------------------------------------
+  7 alarms generated by the analysis:
+       2 accesses out of bounds index
+       2 integer overflows
+       2 accesses to uninitialized left-values
+       1 nan or infinite floating-point value
+  ----------------------------------------------------------------------------
+  Evaluation of the logical properties reached by the analysis:
+    Assertions        0 valid     0 unknown     0 invalid      0 total
+    Preconditions     2 valid     4 unknown     1 invalid      7 total
+  28% of the logical properties reached have been proven.
+  ----------------------------------------------------------------------------
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index 409a3b2a28558415904f514d257a33ea2a6adfbe..13a6e265714a9c2c28b8b8977a32699613169d52 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -347,6 +347,7 @@ module Make (Abstract: Abstractions.Eva) = struct
       Value_parameters.feedback "done for function %a" Kernel_function.pretty kf;
       post_analysis ();
       Abstract.Dom.post_analysis final_state;
+      Value_results.print_summary ();
     with
     | Db.Value.Aborted ->
       post_analysis_cleanup ~aborted:true;
diff --git a/src/plugins/value/utils/value_results.ml b/src/plugins/value/utils/value_results.ml
index c9db33d1cca57a42727963b1c262e568220b01df..08ccbe8ea20d43eb42c6e888db097015d3924ca6 100644
--- a/src/plugins/value/utils/value_results.ml
+++ b/src/plugins/value/utils/value_results.ml
@@ -355,6 +355,236 @@ let merge r1 r2 =
   { main; before_states; after_states; kf_initial_states; kf_is_called;
     initial_state; initial_args; alarms; statuses; kf_callers }
 
+(* ---------------------- Printing an analysis summary ---------------------- *)
+
+open Cil_types
+
+let plural count = if count = 1 then "" else "s"
+
+let consider_function vi =
+  not (Cil.is_builtin vi
+       || Cil.is_special_builtin vi.vname
+       || Cil.hasAttribute "fc_stdlib" vi.vattr
+       || Cil.hasAttribute "fc_stdlib_generated" vi.vattr)
+
+let print_coverage fmt =
+  let ignored, analyzed = ref 0, ref 0
+  and dead, reachable = ref 0, ref 0 in
+  let is_reachable = Db.Value.is_reachable_stmt in
+  let do_stmt stmt = incr (if is_reachable stmt then reachable else dead) in
+  let visit fundec =
+    if consider_function fundec.svar then
+      if is_called (Globals.Functions.get fundec.svar)
+      then (incr analyzed; List.iter do_stmt fundec.sallstmts)
+      else incr ignored
+  in
+  Globals.Functions.iter_on_fundecs visit;
+  let all = !dead + !analyzed in
+  if all = 0
+  then Format.fprintf fmt "No function to be analyzed.@;"
+  else
+    Format.fprintf fmt
+      "%i function%s analyzed (out of %i): %i%% coverage.@;"
+      !analyzed (plural !analyzed) all (!analyzed * 100 / all);
+  let total = !dead + !reachable in
+  if !analyzed > 0 && total > 0 then
+    Format.fprintf fmt
+      "In %s, %i statements reached (out of %i): %i%% coverage.@;"
+      (if !analyzed > 1 then "these functions" else "this function")
+      !reachable total (!reachable * 100 / total)
+
+let print_warning fmt =
+  let eva_warnings, eva_errors = ref 0, ref 0
+  and kernel_warnings, kernel_errors = ref 0, ref 0 in
+  let report_event event =
+    let open Log in
+    match event.evt_kind, event.evt_plugin with
+    | Warning, "eva" when event.evt_category <> Some "alarm" -> incr eva_warnings
+    | Warning, name when name = Log.kernel_label_name -> incr kernel_warnings
+    | Error, "eva" when event.evt_category <> Some "alarm" -> incr eva_errors
+    | Error, name when name = Log.kernel_label_name -> incr kernel_errors
+    | _ -> ()
+  in
+  Messages.iter report_event;
+  let total = !eva_errors + !eva_warnings + !kernel_errors + !kernel_warnings in
+  if total = 0
+  then Format.fprintf fmt "No errors or warnings raised during the analysis.@;"
+  else
+    let print str errors warnings =
+      Format.fprintf fmt "  by %-19s  %3i error%s  %3i warning%s@;"
+        (str ^ ":") errors (plural errors) warnings (plural warnings)
+    in
+    Format.fprintf fmt
+      "Some errors and warnings have been raised during the analysis:@;";
+    print "the Eva analyzer" !eva_errors !eva_warnings;
+    print "the Frama-C kernel" !kernel_errors !kernel_warnings
+
+type alarms =
+  { division_by_zero: int ref;
+    memory_access: int ref;
+    index_out_of_bound: int ref;
+    overflow: int ref;
+    invalid_shift: int ref;
+    uninitialized: int ref;
+    dangling: int ref;
+    nan_or_infinite: int ref;
+    float_to_int: int ref;
+    others: int ref; }
+
+type statuses = { valid: int ref; unknown: int ref; invalid: int ref; }
+
+type report =
+  { alarms: statuses * alarms;
+    assertions: statuses;
+    preconds: statuses; }
+
+let empty_report () =
+  let empty () = { valid = ref 0; unknown = ref 0; invalid = ref 0 } in
+  let empty_alarms =
+    { division_by_zero = ref 0;
+      memory_access = ref 0;
+      index_out_of_bound = ref 0;
+      overflow = ref 0;
+      invalid_shift = ref 0;
+      uninitialized = ref 0;
+      dangling = ref 0;
+      nan_or_infinite = ref 0;
+      float_to_int = ref 0;
+      others = ref 0; }
+  in
+  { alarms = empty (), empty_alarms;
+    assertions = empty ();
+    preconds = empty (); }
+
+let report_alarm report alarm =
+  let open Alarms in
+  let counter = match alarm with
+    | Division_by_zero _   -> report.division_by_zero
+    | Memory_access _      -> report.memory_access
+    | Index_out_of_bound _ -> report.index_out_of_bound
+    | Invalid_shift _      -> report.invalid_shift
+    | Overflow _           -> report.overflow
+    | Uninitialized _      -> report.uninitialized
+    | Dangling _           -> report.dangling
+    | Is_nan_or_infinite _
+    | Is_nan _             -> report.nan_or_infinite
+    | Float_to_int _       -> report.float_to_int
+    | _                    -> report.others
+  in
+  incr counter
+
+let eva_emitter = Value_util.emitter
+
+let get_status ip =
+  let aux_status emitter status acc =
+    let emitter = Emitter.Usable_emitter.get emitter.Property_status.emitter in
+    if Emitter.equal eva_emitter emitter
+    then Some status
+    else acc
+  in
+  Property_status.fold_on_statuses aux_status ip None
+
+let report_status acc = function
+  | None -> ()
+  | Some status -> match status with
+    | Property_status.Dont_know           -> incr acc.unknown
+    | Property_status.True                -> incr acc.valid
+    | Property_status.False_if_reachable
+    | Property_status.False_and_reachable -> incr acc.invalid
+
+let make_report ()  =
+  let report = empty_report () in
+  let report_property ip =
+    match ip with
+    | Property.IPCodeAnnot (_kf, _stmt, code_annot) ->
+      begin
+        let status = get_status ip in
+        match Alarms.find code_annot with
+        | None -> report_status report.assertions status
+        | Some alarm ->
+          let acc_status, acc_alarms = report.alarms in
+          report_status acc_status status;
+          report_alarm acc_alarms alarm
+      end
+    | Property.IPPropertyInstance _ ->
+      let status = get_status ip in
+      report_status report.preconds status
+    | _ -> ()
+  in
+  Property_status.iter report_property;
+  report
+
+let print_alarms_kind fmt kind =
+  let print count str plural str' =
+    if !count > 0 then
+      Format.fprintf fmt "  %4i %s%s%s@;"
+        !count str (if !count > 1 then plural else "") str'
+  in
+  print kind.division_by_zero "division" "s" " by zero";
+  print kind.memory_access "invalid memory access" "es" "";
+  print kind.index_out_of_bound "access" "es" " out of bounds index";
+  print kind.overflow "integer overflow" "s" "";
+  print kind.invalid_shift "invalid shift" "s" "";
+  print kind.uninitialized "access" "es" " to uninitialized left-values";
+  print kind.dangling "escaping address" "es" "";
+  print kind.nan_or_infinite "nan or infinite floating-point value" "s" "";
+  print kind.float_to_int "illegal conversion" "s" " from floating-point to integer";
+  print kind.others "other" "s" ""
+
+let print_alarms fmt report =
+  let alarms, kind = report.alarms in
+  let total = !(alarms.unknown) + !(alarms.invalid) in
+  Format.fprintf fmt "%i alarm%s generated by the analysis" total (plural total);
+  if total = !(kind.others)
+  then Format.fprintf fmt ".@;"
+  else Format.fprintf fmt ":@;%a" print_alarms_kind kind;
+  let invalid = !(alarms.invalid) in
+  if invalid > 0 then
+    Format.fprintf fmt "%i of them %s sure alarm%s (invalid status).@;"
+      invalid (if invalid = 1 then "is a" else "are") (plural invalid)
+
+let print_properties fmt report =
+  let { assertions; preconds } = report in
+  let total acc = !(acc.valid) + !(acc.unknown) + !(acc.invalid) in
+  let total_assertions = total assertions
+  and total_preconds = total preconds in
+  let total = total_assertions + total_preconds in
+  if total = 0
+  then
+    Format.fprintf fmt
+      "No logical properties have been reached by the analysis.@;"
+  else
+    let print_line header status total =
+      Format.fprintf fmt
+        "  %-14s %4d valid  %4d unknown  %4d invalid   %4d total@;"
+        header !(status.valid) !(status.unknown) !(status.invalid) total;
+    in
+    Format.fprintf fmt
+      "Evaluation of the logical properties reached by the analysis:@;";
+    print_line "Assertions" assertions total_assertions;
+    print_line "Preconditions" preconds total_preconds;
+    let proven = !(assertions.valid) + !(preconds.valid) in
+    let proven = proven * 100 / total in
+    Format.fprintf fmt
+      "%i%% of the logical properties reached have been proven.@;" proven
+
+let print_summary fmt =
+  let bar = String.make 76 '-' in
+  let report = make_report () in
+  Format.fprintf fmt "%s@;" bar;
+  print_coverage fmt;
+  Format.fprintf fmt "%s@;" bar;
+  print_warning fmt;
+  Format.fprintf fmt "%s@;" bar;
+  print_alarms fmt report;
+  Format.fprintf fmt "%s@;" bar;
+  print_properties fmt report;
+  Format.fprintf fmt "%s" bar
+
+let print_summary () =
+  let dkey = Value_parameters.dkey_summary in
+  let header fmt = Format.fprintf fmt " ====== ANALYSIS SUMMARY ======" in
+  Value_parameters.printf ~header ~dkey ~level:1 "  @[<v>%t@]" print_summary
 
 (*
 Local Variables:
diff --git a/src/plugins/value/utils/value_results.mli b/src/plugins/value/utils/value_results.mli
index ae92d8878ad5f6a6dd35716ef6a6fdac8abbae83..5238a634bbfdfe97e8cf10131b53475eec1f81a1 100644
--- a/src/plugins/value/utils/value_results.mli
+++ b/src/plugins/value/utils/value_results.mli
@@ -46,6 +46,8 @@ val change_callstacks:
     For technical reasons, the top of the callstack must currently
     be preserved. *)
 
+(** Prints a summary of the analysis. *)
+val print_summary: unit -> unit
 
 (*
 Local Variables:
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 0f8cb4ca773b121746c0af4c6c998912fbb4df51..7b0254eb4854e6efd6d47df74d0e7ef0ed107de7 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -70,6 +70,7 @@ let () = add_plugin_output_aliases [ "value" ]
 (* Debug categories. *)
 let dkey_initial_state = register_category "initial-state"
 let dkey_final_states = register_category "final-states"
+let dkey_summary = register_category "summary"
 let dkey_pointer_comparison = register_category "pointer-comparison"
 let dkey_cvalue_domain = register_category "d-cvalue"
 let dkey_incompatible_states = register_category "incompatible-states"
@@ -80,7 +81,7 @@ let dkey_widening = register_category "widening"
 let () =
   let activate dkey = add_debug_keys dkey in
   List.iter activate
-    [dkey_initial_state; dkey_final_states; dkey_cvalue_domain]
+    [dkey_initial_state; dkey_final_states; dkey_summary; dkey_cvalue_domain]
 
 (* Warning categories. *)
 let wkey_alarm = register_warn_category "alarm"
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 1edd3dac575243c6c528a686411f75ac92df9a65..c6a81aa6e935db912cd109fdec2d1c5f6ea3c6cf 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -166,6 +166,7 @@ val parameters_abstractions: Typed_parameter.t list
     -value-msg-key="-initial_state,-final_state" *)
 val dkey_initial_state : category
 val dkey_final_states : category
+val dkey_summary : category
 
 (** Warning category used when emitting an alarm in "warning" mode. *)
 val wkey_alarm: warn_category
diff --git a/src/plugins/variadic/tests/test_config b/src/plugins/variadic/tests/test_config
index 70aafaf12a62b221d4c08d43db6deea360a3e3d5..9d83090791bf7d3f4f62b2e69990d30fefd28fc8 100644
--- a/src/plugins/variadic/tests/test_config
+++ b/src/plugins/variadic/tests/test_config
@@ -1 +1 @@
-OPT: -no-autoload-plugins -load-module from,inout,eva,variadic,scope -check -print -kernel-verbose 0 -variadic-verbose 2 -eva -slevel 10 -eva-msg-key=-initial-state -eva-no-show-progress -eva-print
+OPT: -no-autoload-plugins -load-module from,inout,eva,variadic,scope -check -print -kernel-verbose 0 -variadic-verbose 2 -eva -slevel 10 -eva-msg-key=-initial-state,-summary -eva-no-show-progress -eva-print
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/checks.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/checks.0.res.oracle
index a99ec33e26d36787a9fc88e173e145acb5ac2b4a..bae891952be7ca996280d35951a229bd1336993e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/checks.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/checks.0.res.oracle
@@ -42,6 +42,20 @@ Prove: true.
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 5 statements reached (out of 5): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  Evaluation of the logical properties reached by the analysis:
+    Assertions        0 valid     4 unknown     0 invalid      4 total
+    Preconditions     0 valid     0 unknown     0 invalid      0 total
+  0% of the logical properties reached have been proven.
+  ----------------------------------------------------------------------------
 [report] Computing properties status...
 --------------------------------------------------------------------------------
 --- Global Properties
diff --git a/src/plugins/wp/tests/wp_plugin/removed.i b/src/plugins/wp/tests/wp_plugin/removed.i
index 060f7e15435fe72e046f671f1bbef4d7131b4a2d..e865b65ae689e3fc680dfc6ff64320ce00d84e81 100644
--- a/src/plugins/wp/tests/wp_plugin/removed.i
+++ b/src/plugins/wp/tests/wp_plugin/removed.i
@@ -1,6 +1,6 @@
 /* run.config_qualif
    CMD: @frama-c@ -wp-share ./share -wp-msg-key success-only -wp-par 1 -wp-timeout 100 -wp-steps 500
-   OPT: -eva -then -wp -then -no-eva -warn-unsigned-overflow -wp
+   OPT: -eva -eva-msg-key=-summary -then -wp -then -no-eva -warn-unsigned-overflow -wp
  */
 
 /* run.config
diff --git a/tests/callgraph/oracle/issue_55_iter_over_unregistered_function.res.oracle b/tests/callgraph/oracle/issue_55_iter_over_unregistered_function.res.oracle
index 912046cbc683279ca4b87d64509e674f76e1ac4b..f2b3a6b73869d6056238fbd7bb1d8b664c3957b1 100644
--- a/tests/callgraph/oracle/issue_55_iter_over_unregistered_function.res.oracle
+++ b/tests/callgraph/oracle/issue_55_iter_over_unregistered_function.res.oracle
@@ -9,6 +9,19 @@
 [eva] done for function main
 [eva] tests/callgraph/issue_55_iter_over_unregistered_function.i:12: 
   assertion 'Eva,initialization' got final status invalid.
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 3): 33% coverage.
+  In this function, 1 statements reached (out of 3): 33% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  1 alarm generated by the analysis:
+       1 access to uninitialized left-values
+  1 of them is a sure alarm (invalid status).
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 [inout] InOut (internal) for function main:
   Operational inputs:
     q
diff --git a/tests/callgraph/oracle/no_fp_unsound_warning.0.res.oracle b/tests/callgraph/oracle/no_fp_unsound_warning.0.res.oracle
index f92e8ed4637457992e96534d767763525ad2623b..302afc81d0db9b556b86b10ca214cc82f795ee26 100644
--- a/tests/callgraph/oracle/no_fp_unsound_warning.0.res.oracle
+++ b/tests/callgraph/oracle/no_fp_unsound_warning.0.res.oracle
@@ -5,5 +5,16 @@
 [eva:initial-state] Values of globals at initialization
   
 [eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 1 statements reached (out of 1): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 [inout] Out (internal) for function main:
     \nothing
diff --git a/tests/callgraph/oracle/no_fp_unsound_warning.1.res.oracle b/tests/callgraph/oracle/no_fp_unsound_warning.1.res.oracle
index 4f2c24befe204e6d5d21b74ab9455631cc1c0e17..69a91fb9cf5e48c751f375293aaea9e2cd52ce47 100644
--- a/tests/callgraph/oracle/no_fp_unsound_warning.1.res.oracle
+++ b/tests/callgraph/oracle/no_fp_unsound_warning.1.res.oracle
@@ -5,6 +5,17 @@
 [eva:initial-state] Values of globals at initialization
   
 [eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 1 statements reached (out of 1): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 [cg] Warning: using callgraph while option -cg-function-pointers is unset, result may be unsound
 [inout] Out (internal) for function main:
     \nothing
diff --git a/tests/idct/diff_equalities b/tests/idct/diff_equalities
index 6d1b02bed20ea33526cb44e99c993a8b13876539..4ed73b90e44bd7a7e5fb827e497ac3b792169bb2 100644
--- a/tests/idct/diff_equalities
+++ b/tests/idct/diff_equalities
@@ -130,3 +130,7 @@ diff tests/idct/oracle/ieee_1180_1990.res.oracle tests/idct/oracle_equalities/ie
 >   Call to builtin Frama_C_cos for function cos
 > [eva] tests/idct/ieee_1180_1990.c:140: 
 >   Call to builtin Frama_C_sqrt for function sqrt
+980c1060
+<     by the Eva analyzer:      0 errors   42 warnings
+---
+>     by the Eva analyzer:      0 errors   48 warnings
diff --git a/tests/idct/ieee_1180_1990.c b/tests/idct/ieee_1180_1990.c
index 1f0f4325eeb430e18ca50f20b716f4ecdcc6f207..6c5b0285d74841904ecffe54670abca54e6c0b93 100644
--- a/tests/idct/ieee_1180_1990.c
+++ b/tests/idct/ieee_1180_1990.c
@@ -1,6 +1,6 @@
 /* run.config*
    GCC:
-   STDOPT: +"-load-module report,scope,variadic -float-normal -no-warn-signed-overflow tests/idct/idct.c -remove-redundant-alarms -eva-memexec -eva-builtin sqrt:Frama_C_sqrt,cos:Frama_C_cos -then -report -report-print-properties"
+   STDOPT: +"-eva-msg-key=summary -load-module report,scope,variadic -float-normal -no-warn-signed-overflow tests/idct/idct.c -remove-redundant-alarms -eva-memexec -eva-builtin sqrt:Frama_C_sqrt,cos:Frama_C_cos -then -report -report-print-properties"
 */
 /* IEEE_1180_1990: a testbed for IDCT accuracy
  * Copyright (C) 2001  Renaud Pacalet
diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index 701da61a7a281513ca4425510286d513f568e803..a0c2c414fd9f4785327dea18761f3ff05f3f9fa8 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -971,6 +971,24 @@
   idct_mc2[0..7][0..7] ∈ [-8192..8192]
   __retres ∈ {0; 1}
   S___fc_stdout[0..1] ∈ [--..--]
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  6 functions analyzed (out of 44): 13% coverage.
+  In these functions, 588 statements reached (out of 626): 93% coverage.
+  ----------------------------------------------------------------------------
+  Some errors and warnings have been raised during the analysis:
+    by the Eva analyzer:      0 errors   42 warnings
+    by the Frama-C kernel:    0 errors    0 warnings
+  ----------------------------------------------------------------------------
+  72 alarms generated by the analysis:
+      64 accesses to uninitialized left-values
+       8 illegal conversions from floating-point to integer
+  ----------------------------------------------------------------------------
+  Evaluation of the logical properties reached by the analysis:
+    Assertions        0 valid     0 unknown     0 invalid      0 total
+    Preconditions    11 valid     0 unknown     0 invalid     11 total
+  100% of the logical properties reached have been proven.
+  ----------------------------------------------------------------------------
 [from] Computing for function IEEE_1180_1990_rand
 [from] Done for function IEEE_1180_1990_rand
 [from] Computing for function IEEE_1180_1990_mkbk
diff --git a/tests/impact/oracle/depend5.res.oracle b/tests/impact/oracle/depend5.res.oracle
index 8ebb3a55b259b013d269dc286549ddc1a47a1fdc..415d327aa48e2ce9f2a753cf94e0667a2ea0b345 100644
--- a/tests/impact/oracle/depend5.res.oracle
+++ b/tests/impact/oracle/depend5.res.oracle
@@ -17,6 +17,17 @@
 [from] Computing for function main
 [from] Done for function main
 [eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  3 functions analyzed (out of 3): 100% coverage.
+  In these functions, 13 statements reached (out of 13): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 [from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
 [from] call to f at tests/impact/depend5.i:18 (by g):
   b FROM a; e
diff --git a/tests/journal/oracle/control.0.res.oracle b/tests/journal/oracle/control.0.res.oracle
index a04a28a513c7a7a17daa9e0a36f3b9daa84f2e59..2ee981ccf351c5624f462d99bd30b24696a4e799 100644
--- a/tests/journal/oracle/control.0.res.oracle
+++ b/tests/journal/oracle/control.0.res.oracle
@@ -16,6 +16,18 @@
 [eva:final-states] Values at end of function f:
   x ∈ [0..2147483647]
   i ∈ {4}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 4): 25% coverage.
+  In this function, 9 statements reached (out of 12): 75% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  1 alarm generated by the analysis:
+       1 integer overflow
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 [from] Computing for function f
 [from] Done for function f
 [kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/journal/oracle/control.1.res.oracle b/tests/journal/oracle/control.1.res.oracle
index 0d4cd66ed390271e928405b836d12f8bdb684395..55c6fcda9b26c40ee167dcf8563665b5dd72ab26 100644
--- a/tests/journal/oracle/control.1.res.oracle
+++ b/tests/journal/oracle/control.1.res.oracle
@@ -16,6 +16,18 @@
 [eva:final-states] Values at end of function f:
   x ∈ [0..2147483647]
   i ∈ {4}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 4): 25% coverage.
+  In this function, 9 statements reached (out of 12): 75% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  1 alarm generated by the analysis:
+       1 integer overflow
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 [from] Computing for function f
 [from] Done for function f
 [kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
@@ -42,6 +54,20 @@
 [eva:final-states] Values at end of function f:
   x ∈ [0..2147483647]
   i ∈ {4}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 4): 25% coverage.
+  In this function, 9 statements reached (out of 12): 75% coverage.
+  ----------------------------------------------------------------------------
+  Some errors and warnings have been raised during the analysis:
+    by the Eva analyzer:      0 errors    0 warnings
+    by the Frama-C kernel:    0 errors    1 warning
+  ----------------------------------------------------------------------------
+  1 alarm generated by the analysis:
+       1 integer overflow
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 [from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
 [from] entry point:
   x FROM x (and SELF)
diff --git a/tests/journal/oracle/control2.res.oracle b/tests/journal/oracle/control2.res.oracle
index 65f6972933b6d55079a46623f905c5dd4781c67d..f73d56171f0db23c4055406812a7c19107de9100 100644
--- a/tests/journal/oracle/control2.res.oracle
+++ b/tests/journal/oracle/control2.res.oracle
@@ -15,6 +15,18 @@
 [eva:final-states] Values at end of function f:
   x ∈ [0..2147483647]
   i ∈ {4}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 4): 25% coverage.
+  In this function, 9 statements reached (out of 12): 75% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  1 alarm generated by the analysis:
+       1 integer overflow
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 [from] Computing for function f
 [from] Done for function f
 [eva] Analyzing an incomplete application starting at f
@@ -37,6 +49,18 @@
   x ∈ [--..--]
   y ∈ [--..--]
   i ∈ {4}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 12 statements reached (out of 12): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  3 alarms generated by the analysis:
+       3 integer overflows
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 [from] Computing for function f
 [from] Done for function f
 [kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
diff --git a/tests/journal/oracle/control2_sav.res b/tests/journal/oracle/control2_sav.res
index 3f2f015507ecaba23d749a4b1a96195a1b714ff6..cfefb7770292c8cb107c3032b830803c8191e095 100644
--- a/tests/journal/oracle/control2_sav.res
+++ b/tests/journal/oracle/control2_sav.res
@@ -15,6 +15,18 @@
 [eva:final-states] Values at end of function f:
   x ∈ [0..2147483647]
   i ∈ {4}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 4): 25% coverage.
+  In this function, 9 statements reached (out of 12): 75% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  1 alarm generated by the analysis:
+       1 integer overflow
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 [from] Computing for function f
 [from] Done for function f
 [kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
@@ -38,6 +50,20 @@
   x ∈ [--..--]
   y ∈ [--..--]
   i ∈ {4}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 12 statements reached (out of 12): 100% coverage.
+  ----------------------------------------------------------------------------
+  Some errors and warnings have been raised during the analysis:
+    by the Eva analyzer:      0 errors    0 warnings
+    by the Frama-C kernel:    0 errors    1 warning
+  ----------------------------------------------------------------------------
+  3 alarms generated by the analysis:
+       3 integer overflows
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 [from] Computing for function f
 [from] Done for function f
 [from] ====== DEPENDENCIES COMPUTED ======
diff --git a/tests/journal/oracle/intra.res.oracle b/tests/journal/oracle/intra.res.oracle
index e2f814d04a544f8528f553003c53056efcf76aaa..5e39a5c278bb9da6f9f575e1bfa755291fb626d9 100644
--- a/tests/journal/oracle/intra.res.oracle
+++ b/tests/journal/oracle/intra.res.oracle
@@ -56,6 +56,22 @@
 [eva] Done for function stop
 [eva] Recording results for main
 [eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  8 functions analyzed (out of 9): 88% coverage.
+  In these functions, 58 statements reached (out of 59): 98% coverage.
+  ----------------------------------------------------------------------------
+  Some errors and warnings have been raised during the analysis:
+    by the Eva analyzer:      0 errors    0 warnings
+    by the Frama-C kernel:    0 errors    1 warning
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  Evaluation of the logical properties reached by the analysis:
+    Assertions        6 valid     0 unknown     0 invalid      6 total
+    Preconditions     0 valid     0 unknown     0 invalid      0 total
+  100% of the logical properties reached have been proven.
+  ----------------------------------------------------------------------------
 [pdg] computing for function main
 [from] Computing for function param
 [from] Done for function param
diff --git a/tests/metrics/oracle/func_ptr.0.res.oracle b/tests/metrics/oracle/func_ptr.0.res.oracle
index 9ad14445a9209e71ea101cea19402366ef688035..428986010691df4429d28efc6da6ca2e449b53bb 100644
--- a/tests/metrics/oracle/func_ptr.0.res.oracle
+++ b/tests/metrics/oracle/func_ptr.0.res.oracle
@@ -46,6 +46,19 @@
   bar ∈ {0}
   bar_extern ∈ {0}
 [eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 8): 12% coverage.
+  In this function, 6 statements reached (out of 13): 46% coverage.
+  ----------------------------------------------------------------------------
+  Some errors and warnings have been raised during the analysis:
+    by the Eva analyzer:      0 errors    0 warnings
+    by the Frama-C kernel:    0 errors    1 warning
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 [metrics] Eva coverage statistics
   =======================
   Syntactically reachable functions = 3 (out of 5)
diff --git a/tests/metrics/oracle/func_ptr.1.res.oracle b/tests/metrics/oracle/func_ptr.1.res.oracle
index e5937b139f68d51c065640b27c4fa32d8d6982b6..703415595918a67d1441bee0b6d26d1cef1dddd4 100644
--- a/tests/metrics/oracle/func_ptr.1.res.oracle
+++ b/tests/metrics/oracle/func_ptr.1.res.oracle
@@ -46,6 +46,19 @@
   bar ∈ {0}
   bar_extern ∈ {0}
 [eva] done for function foobar
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  2 functions analyzed (out of 2): 100% coverage.
+  In these functions, 5 statements reached (out of 5): 100% coverage.
+  ----------------------------------------------------------------------------
+  Some errors and warnings have been raised during the analysis:
+    by the Eva analyzer:      0 errors    0 warnings
+    by the Frama-C kernel:    0 errors    1 warning
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 [metrics] Eva coverage statistics
   =======================
   Syntactically reachable functions = 2 (out of 5)
diff --git a/tests/metrics/oracle/libc.0.res.oracle b/tests/metrics/oracle/libc.0.res.oracle
index 3cff2f1a191389113a805b4da2240e279a026555..76a9cd7cd795af18278d1e949a4e6407dcbec6a9 100644
--- a/tests/metrics/oracle/libc.0.res.oracle
+++ b/tests/metrics/oracle/libc.0.res.oracle
@@ -38,6 +38,20 @@
 [eva] using specification for function isalpha
 [eva] using specification for function isblank
 [eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  4 functions analyzed (out of 4): 100% coverage.
+  In these functions, 10 statements reached (out of 10): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  Evaluation of the logical properties reached by the analysis:
+    Assertions        0 valid     0 unknown     0 invalid      0 total
+    Preconditions     2 valid     0 unknown     0 invalid      2 total
+  100% of the logical properties reached have been proven.
+  ----------------------------------------------------------------------------
 [metrics] Eva coverage statistics
   =======================
   Syntactically reachable functions = 4 (out of 5)
diff --git a/tests/metrics/oracle/libc.1.res.oracle b/tests/metrics/oracle/libc.1.res.oracle
index 4f1b84793b0cdddb3255ee72a288a2185f1122be..890b92c6ed6f4576aded31faf97765ab72a9cf68 100644
--- a/tests/metrics/oracle/libc.1.res.oracle
+++ b/tests/metrics/oracle/libc.1.res.oracle
@@ -56,6 +56,20 @@
 [eva] using specification for function isalpha
 [eva] using specification for function isblank
 [eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  4 functions analyzed (out of 4): 100% coverage.
+  In these functions, 10 statements reached (out of 10): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  Evaluation of the logical properties reached by the analysis:
+    Assertions        0 valid     0 unknown     0 invalid      0 total
+    Preconditions     2 valid     0 unknown     0 invalid      2 total
+  100% of the logical properties reached have been proven.
+  ----------------------------------------------------------------------------
 [metrics] Eva coverage statistics
   =======================
   Syntactically reachable functions = 7 (out of 76)
diff --git a/tests/metrics/oracle/reach.res.oracle b/tests/metrics/oracle/reach.res.oracle
index 3bf756a5a54dd8ce98852cfbd896521f5e130ca5..e568528660bde94fa24656908310b1b9822a4dd9 100644
--- a/tests/metrics/oracle/reach.res.oracle
+++ b/tests/metrics/oracle/reach.res.oracle
@@ -83,6 +83,17 @@
   t[0] ∈ {{ &baz }}
    [1] ∈ {0}
 [eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 6): 16% coverage.
+  In this function, 7 statements reached (out of 12): 58% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 [metrics] Eva coverage statistics
   =======================
   Syntactically reachable functions = 3 (out of 3)
diff --git a/tests/metrics/oracle/unreachable.res.oracle b/tests/metrics/oracle/unreachable.res.oracle
index ac7dad1c8c1d4676a07e7ceefbb6a82e01282460..f542548237b0d0a7f7567f3951bbb2da54de561c 100644
--- a/tests/metrics/oracle/unreachable.res.oracle
+++ b/tests/metrics/oracle/unreachable.res.oracle
@@ -35,6 +35,17 @@
 [eva:initial-state] Values of globals at initialization
   
 [eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 5): 20% coverage.
+  In this function, 6 statements reached (out of 10): 60% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 [metrics] Eva coverage statistics
   =======================
   Syntactically reachable functions = 2 (out of 2)
@@ -56,6 +67,17 @@
 [eva:initial-state] Values of globals at initialization
   
 [eva] done for function foo
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 2 statements reached (out of 2): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 [metrics] Eva coverage statistics
   =======================
   Syntactically reachable functions = 1 (out of 2)
diff --git a/tests/misc/oracle/bts1201.res.oracle b/tests/misc/oracle/bts1201.res.oracle
index 1f86ad9db0ec5a63a16f794d0d3aff8ccf38e9bc..bf9968e480cc7fb94343c74c0e71eb5a44bef38d 100644
--- a/tests/misc/oracle/bts1201.res.oracle
+++ b/tests/misc/oracle/bts1201.res.oracle
@@ -6,12 +6,40 @@
   
 [eva] tests/misc/bts1201.i:5: assertion got status valid.
 [eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 2 statements reached (out of 2): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  Evaluation of the logical properties reached by the analysis:
+    Assertions        1 valid     0 unknown     0 invalid      1 total
+    Preconditions     0 valid     0 unknown     0 invalid      0 total
+  100% of the logical properties reached have been proven.
+  ----------------------------------------------------------------------------
 [eva] Analyzing a complete application starting at main2
 [eva] Computing initial state
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
 [eva] done for function main2
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 1 statements reached (out of 1): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  Evaluation of the logical properties reached by the analysis:
+    Assertions        1 valid     0 unknown     0 invalid      1 total
+    Preconditions     0 valid     0 unknown     0 invalid      0 total
+  100% of the logical properties reached have been proven.
+  ----------------------------------------------------------------------------
 /* Generated by Frama-C */
 void main(void)
 {
diff --git a/tests/misc/oracle/change_main.res.oracle b/tests/misc/oracle/change_main.res.oracle
index 6b17595c9d5a78fb1d6dbf5ac62bb7de4d92dbeb..b8d9d6fde811d0da2effd143924adadba3783044 100644
--- a/tests/misc/oracle/change_main.res.oracle
+++ b/tests/misc/oracle/change_main.res.oracle
@@ -8,6 +8,17 @@
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function f:
   
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 1 statements reached (out of 1): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 [eva] Analyzing a complete application starting at g
 [eva] Computing initial state
 [eva] Initial state computed
@@ -17,3 +28,14 @@
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function g:
   
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 1 statements reached (out of 1): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
diff --git a/tests/misc/oracle/ensures.res.oracle b/tests/misc/oracle/ensures.res.oracle
index 7acf87d61616ae7b517495ee6013e35bbdeaf2a7..ee0832cdeffc1cc003c4ae54db0a7947af527c57 100644
--- a/tests/misc/oracle/ensures.res.oracle
+++ b/tests/misc/oracle/ensures.res.oracle
@@ -7,6 +7,17 @@
 [eva:alarm] tests/misc/ensures.i:5: Warning: 
   function main: postcondition got status invalid.
 [eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 2 statements reached (out of 2): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 [kernel] main: behavior default!
   **NOT** VALID according to Frama-C kernel (under hypotheses)
 [kernel] main: behavior default! **NOT** VALID according to Eva (under hypotheses)
diff --git a/tests/misc/oracle/well_typed_alarm.res.oracle b/tests/misc/oracle/well_typed_alarm.res.oracle
index 3ba7b848d7601547c3df402938180028ebd6fe61..cff9cdaaa88971d0ae07d576c88835d8e353efe0 100644
--- a/tests/misc/oracle/well_typed_alarm.res.oracle
+++ b/tests/misc/oracle/well_typed_alarm.res.oracle
@@ -7,6 +7,17 @@
 [eva:alarm] tests/misc/well_typed_alarm.i:11: Warning: 
   pointer comparison. assert \pointer_comparable((void *)p, (void *)q);
 [eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 10 statements reached (out of 10): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  1 alarm generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 /* Generated by Frama-C */
 int main(int c)
 {
diff --git a/tests/saveload/oracle/basic_sav.1.res b/tests/saveload/oracle/basic_sav.1.res
index 056059606204259f47c4619d6aa71f6dd14adaa0..d2c84cb5472a81605ccd30aad3736fefb3012431 100644
--- a/tests/saveload/oracle/basic_sav.1.res
+++ b/tests/saveload/oracle/basic_sav.1.res
@@ -15,6 +15,21 @@
   i ∈ [-2147483648..9]
   j ∈ {5}
   __retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 12 statements reached (out of 12): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  1 alarm generated by the analysis:
+       1 integer overflow
+  ----------------------------------------------------------------------------
+  Evaluation of the logical properties reached by the analysis:
+    Assertions        1 valid     0 unknown     0 invalid      1 total
+    Preconditions     0 valid     0 unknown     0 invalid      0 total
+  100% of the logical properties reached have been proven.
+  ----------------------------------------------------------------------------
 [from] Computing for function main
 [from] Done for function main
 [from] ====== DEPENDENCIES COMPUTED ======
diff --git a/tests/saveload/oracle/basic_sav.res b/tests/saveload/oracle/basic_sav.res
index 056059606204259f47c4619d6aa71f6dd14adaa0..d2c84cb5472a81605ccd30aad3736fefb3012431 100644
--- a/tests/saveload/oracle/basic_sav.res
+++ b/tests/saveload/oracle/basic_sav.res
@@ -15,6 +15,21 @@
   i ∈ [-2147483648..9]
   j ∈ {5}
   __retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 12 statements reached (out of 12): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  1 alarm generated by the analysis:
+       1 integer overflow
+  ----------------------------------------------------------------------------
+  Evaluation of the logical properties reached by the analysis:
+    Assertions        1 valid     0 unknown     0 invalid      1 total
+    Preconditions     0 valid     0 unknown     0 invalid      0 total
+  100% of the logical properties reached have been proven.
+  ----------------------------------------------------------------------------
 [from] Computing for function main
 [from] Done for function main
 [from] ====== DEPENDENCIES COMPUTED ======
diff --git a/tests/saveload/oracle/bool_sav.res b/tests/saveload/oracle/bool_sav.res
index 91b80def8d2d6316bebfd69690759d3c1442a3d0..42cfadd177d9795b61e0ab5ef909a7f2ab78dc5c 100644
--- a/tests/saveload/oracle/bool_sav.res
+++ b/tests/saveload/oracle/bool_sav.res
@@ -54,3 +54,18 @@
   x ∈ {1}
   y ∈ {2}
   S___fc_stdout[0..1] ∈ [--..--]
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  2 functions analyzed (out of 2): 100% coverage.
+  In these functions, 24 statements reached (out of 24): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  1 alarm generated by the analysis:
+       1 integer overflow
+  ----------------------------------------------------------------------------
+  Evaluation of the logical properties reached by the analysis:
+    Assertions        1 valid     0 unknown     0 invalid      1 total
+    Preconditions     5 valid     0 unknown     0 invalid      5 total
+  100% of the logical properties reached have been proven.
+  ----------------------------------------------------------------------------
diff --git a/tests/saveload/oracle/callbacks_initial.res b/tests/saveload/oracle/callbacks_initial.res
index 7ae40acf1929984ee3ad46dcc680ee34749f64a8..25b036ba64125f63b83322c481bbdb8145af540e 100644
--- a/tests/saveload/oracle/callbacks_initial.res
+++ b/tests/saveload/oracle/callbacks_initial.res
@@ -33,6 +33,17 @@
 [from] Computing for function main1
 [from] Done for function main1
 [eva] done for function main1
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  4 functions analyzed (out of 4): 100% coverage.
+  In these functions, 9 statements reached (out of 9): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 [from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
 [from] call to f at tests/saveload/callbacks.i:16 (by g1):
   x FROM p
diff --git a/tests/saveload/oracle/deps_sav.res b/tests/saveload/oracle/deps_sav.res
index 40f9aeda11453a63ab6d1a1c2a1b0b9083ec2cbe..c52779de1ee27f18ae17e8ab60348d97820dbefe 100644
--- a/tests/saveload/oracle/deps_sav.res
+++ b/tests/saveload/oracle/deps_sav.res
@@ -14,6 +14,18 @@
   i ∈ [-2147483648..9]
   j ∈ {5}
   __retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 11 statements reached (out of 11): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  1 alarm generated by the analysis:
+       1 integer overflow
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 [from] Computing for function main
 [from] Done for function main
 [from] ====== DEPENDENCIES COMPUTED ======
diff --git a/tests/saveload/oracle/multi_project.1.res.oracle b/tests/saveload/oracle/multi_project.1.res.oracle
index 1cd5eaed301e7605d863fc6f45aa6e8ca1326a5a..1ca91d867296f076e2a0a71a83f86eddebc8b32a 100644
--- a/tests/saveload/oracle/multi_project.1.res.oracle
+++ b/tests/saveload/oracle/multi_project.1.res.oracle
@@ -18,6 +18,20 @@
   x ∈ {2}
   y ∈ {4}
   __retres ∈ {8}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  2 functions analyzed (out of 2): 100% coverage.
+  In these functions, 7 statements reached (out of 7): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  Evaluation of the logical properties reached by the analysis:
+    Assertions        1 valid     0 unknown     0 invalid      1 total
+    Preconditions     0 valid     0 unknown     0 invalid      0 total
+  100% of the logical properties reached have been proven.
+  ----------------------------------------------------------------------------
 [kernel] Checking "foo"
 [kernel] Checking "foobar"
 [kernel] Checking "default"
diff --git a/tests/saveload/oracle/multi_project_sav.res b/tests/saveload/oracle/multi_project_sav.res
index c6cb667f22790752799c6073a046dd5a4f4d07a2..6968a8ec6bec3d45c4bafa4c62f29beab29467df 100644
--- a/tests/saveload/oracle/multi_project_sav.res
+++ b/tests/saveload/oracle/multi_project_sav.res
@@ -12,6 +12,20 @@
 [eva] tests/saveload/multi_project.i:15: assertion got status valid.
 [eva] Recording results for main
 [eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  2 functions analyzed (out of 2): 100% coverage.
+  In these functions, 7 statements reached (out of 7): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  Evaluation of the logical properties reached by the analysis:
+    Assertions        1 valid     0 unknown     0 invalid      1 total
+    Preconditions     0 valid     0 unknown     0 invalid      0 total
+  100% of the logical properties reached have been proven.
+  ----------------------------------------------------------------------------
 /* Generated by Frama-C */
 int f(int x)
 {
diff --git a/tests/saveload/oracle/segfault_datatypes_sav.res b/tests/saveload/oracle/segfault_datatypes_sav.res
index a67d19e53c35d8b2b99e4d14186c88dd929a4f51..1cf0a3182aa799855b6b8135f9bfc4bcc08f6746 100644
--- a/tests/saveload/oracle/segfault_datatypes_sav.res
+++ b/tests/saveload/oracle/segfault_datatypes_sav.res
@@ -14,6 +14,18 @@
   i ∈ [-2147483648..9]
   j ∈ {5}
   __retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 11 statements reached (out of 11): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  1 alarm generated by the analysis:
+       1 integer overflow
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 [from] Computing for function main
 [from] Done for function main
 [from] ====== DEPENDENCIES COMPUTED ======
diff --git a/tests/saveload/oracle/sparecode_sav.res b/tests/saveload/oracle/sparecode_sav.res
index 87fe698cd5e96a4e76080db43d43fb7c6b43d9f1..f1ac9d2f24dc8133113b67db5feb21a631f000bc 100644
--- a/tests/saveload/oracle/sparecode_sav.res
+++ b/tests/saveload/oracle/sparecode_sav.res
@@ -19,6 +19,17 @@
 [eva] Done for function f
 [eva] Recording results for main
 [eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  2 functions analyzed (out of 2): 100% coverage.
+  In these functions, 9 statements reached (out of 9): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 [slicing] initializing slicing ...
 [slicing] interpreting slicing requests from the command line...
 [pdg] computing for function main
diff --git a/tests/spec/oracle/default_assigns_bts0966.res.oracle b/tests/spec/oracle/default_assigns_bts0966.res.oracle
index 7fb0bd7fa3693bab1e859ba911eec5c6cbd8f579..525ec649affa3ac23429cd1408acd16667082f02 100644
--- a/tests/spec/oracle/default_assigns_bts0966.res.oracle
+++ b/tests/spec/oracle/default_assigns_bts0966.res.oracle
@@ -16,6 +16,19 @@
              [1] ∈ {1}
              [2..3] ∈ {0}
   __retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 7 statements reached (out of 7): 100% coverage.
+  ----------------------------------------------------------------------------
+  Some errors and warnings have been raised during the analysis:
+    by the Eva analyzer:      0 errors    1 warning
+    by the Frama-C kernel:    0 errors    1 warning
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 /* Generated by Frama-C */
 enum states {
     Init = 0,
diff --git a/tests/spec/oracle/logic_def.res.oracle b/tests/spec/oracle/logic_def.res.oracle
index 068ba78e31da714037077c5f602d3cb9fb8b6b1e..a363bbc1f4af37ee378a86e65f0e6c8f3e4b4134 100644
--- a/tests/spec/oracle/logic_def.res.oracle
+++ b/tests/spec/oracle/logic_def.res.oracle
@@ -10,6 +10,20 @@
 [eva:final-states] Values at end of function main:
   x ∈ {42}
   __retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 4 statements reached (out of 4): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  Evaluation of the logical properties reached by the analysis:
+    Assertions        1 valid     0 unknown     0 invalid      1 total
+    Preconditions     0 valid     0 unknown     0 invalid      0 total
+  100% of the logical properties reached have been proven.
+  ----------------------------------------------------------------------------
 /* Generated by Frama-C */
 /*@ logic ℤ foo(int x) = x + 2;
  */
diff --git a/tests/syntax/oracle/copy_logic.res.oracle b/tests/syntax/oracle/copy_logic.res.oracle
index 30b1c2e6d09c3740020ab25e56bddbea1a9d455d..654c5e3a503a0e2bb24d6a9d131b3ac87b6f57ad 100644
--- a/tests/syntax/oracle/copy_logic.res.oracle
+++ b/tests/syntax/oracle/copy_logic.res.oracle
@@ -19,6 +19,21 @@
 [eva:final-states] Values at end of function main:
   y ∈ [-2147483606..2147483647]
   __retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 6 statements reached (out of 6): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  1 alarm generated by the analysis:
+       1 integer overflow
+  ----------------------------------------------------------------------------
+  Evaluation of the logical properties reached by the analysis:
+    Assertions        0 valid     2 unknown     0 invalid      2 total
+    Preconditions     0 valid     0 unknown     0 invalid      0 total
+  0% of the logical properties reached have been proven.
+  ----------------------------------------------------------------------------
 /* Generated by Frama-C */
 /*@ predicate p(int x) ;
  */
diff --git a/tests/syntax/oracle/loop-case-switch-for-unroll.0.res.oracle b/tests/syntax/oracle/loop-case-switch-for-unroll.0.res.oracle
index 3d21e2b53792ea9a3ed56da9ff3f57ac6e8046dc..4407cbebb995be38963c081af07126d4ee7385ce 100644
--- a/tests/syntax/oracle/loop-case-switch-for-unroll.0.res.oracle
+++ b/tests/syntax/oracle/loop-case-switch-for-unroll.0.res.oracle
@@ -112,6 +112,17 @@
   x ∈ {32}
   n ∈ {0}
   gen_nondet_i ∈ {31}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  2 functions analyzed (out of 5): 40% coverage.
+  In these functions, 45 statements reached (out of 48): 93% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 /* Generated by Frama-C */
 int gen_nondet(int line);
 
diff --git a/tests/syntax/oracle/loop-case-switch-for-unroll.1.res.oracle b/tests/syntax/oracle/loop-case-switch-for-unroll.1.res.oracle
index 9284243105698190efe952fd6994c375a159a1f3..ccd8dec4937e12ce19a03bca5e7be6379d4cb91c 100644
--- a/tests/syntax/oracle/loop-case-switch-for-unroll.1.res.oracle
+++ b/tests/syntax/oracle/loop-case-switch-for-unroll.1.res.oracle
@@ -112,6 +112,17 @@
   x ∈ {32}
   n ∈ {0}
   gen_nondet_i ∈ {31}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  2 functions analyzed (out of 52): 3% coverage.
+  In these functions, 75 statements reached (out of 125): 60% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 /* Generated by Frama-C */
 int gen_nondet(int line);
 
diff --git a/tests/syntax/oracle/loop-case-switch-for-unroll.2.res.oracle b/tests/syntax/oracle/loop-case-switch-for-unroll.2.res.oracle
index 817e4bba61835baf1760948d7bd0dd08d16de0f0..f029ae319170bc1e849e524390a368aca68a6c87 100644
--- a/tests/syntax/oracle/loop-case-switch-for-unroll.2.res.oracle
+++ b/tests/syntax/oracle/loop-case-switch-for-unroll.2.res.oracle
@@ -112,6 +112,17 @@
   x ∈ {32}
   n ∈ {0}
   gen_nondet_i ∈ {31}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  2 functions analyzed (out of 166): 1% coverage.
+  In these functions, 74 statements reached (out of 238): 31% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
 /* Generated by Frama-C */
 int gen_nondet(int line);
 
diff --git a/tests/test_config b/tests/test_config
index 10fa9a74e569e6de5964ff808cd032bcaab8d674..6efe608ac844b6bfd35b978ccf9915ef6adab07f 100644
--- a/tests/test_config
+++ b/tests/test_config
@@ -1,3 +1,3 @@
-MACRO: EVA_OPTIONS -eva-show-progress
+MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary
 MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
 OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_apron b/tests/test_config_apron
index ccb5342259ce6871ec6fe0580eafa68a41d227bd..2d6cff1926f6598e15c22f97ede264377dedf042 100644
--- a/tests/test_config_apron
+++ b/tests/test_config_apron
@@ -1,3 +1,3 @@
-MACRO: EVA_OPTIONS -eva-show-progress -eva-apron-oct -eva-msg-key experimental-ok
+MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-apron-oct -eva-msg-key experimental-ok
 MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
 OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_bitwise b/tests/test_config_bitwise
index 146e7721ea21c31e274e3dc99ca7395e814f06ab..7e1be236655fdf63e47056f790c1e3c9b30dcdb0 100644
--- a/tests/test_config_bitwise
+++ b/tests/test_config_bitwise
@@ -1,3 +1,3 @@
-MACRO: EVA_OPTIONS -eva-show-progress -eva-bitwise-domain
+MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-bitwise-domain
 MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
 OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_equalities b/tests/test_config_equalities
index 1e592c46e5ca534cd7636927a4f6d926eb124b8b..d84a7e2a8b21674dad528c1927b0630aa948a2f3 100644
--- a/tests/test_config_equalities
+++ b/tests/test_config_equalities
@@ -1,3 +1,3 @@
-MACRO: EVA_OPTIONS -eva-show-progress -eva-equality-domain
+MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-equality-domain
 MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
 OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_gauges b/tests/test_config_gauges
index 7e0fb7cbdac0328ebedf501a2b648a00cf6c6b46..b6a460ae1e45ec4c85dc60eb2a4851b6d84f63b7 100644
--- a/tests/test_config_gauges
+++ b/tests/test_config_gauges
@@ -1,3 +1,3 @@
-MACRO: EVA_OPTIONS -eva-show-progress -eva-gauges-domain
+MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-gauges-domain
 MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
 OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/test_config_symblocs b/tests/test_config_symblocs
index 77ad2e247406b67f866fc55c5e9bc0c6b554ceea..47ce23088d402b091d071c21699c8fb9d4f7f268 100644
--- a/tests/test_config_symblocs
+++ b/tests/test_config_symblocs
@@ -1,3 +1,3 @@
-MACRO: EVA_OPTIONS -eva-show-progress -eva-symbolic-locations-domain
+MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-symbolic-locations-domain
 MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
 OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps
diff --git a/tests/value/numerors/oracle/numerors.res.oracle b/tests/value/numerors/oracle/numerors.res.oracle
index ed54ec83da044cbae19d8b23fe57d391f51ae626..b6bde3cbebb23d7897c74e3661ee2ec094742a7a 100644
--- a/tests/value/numerors/oracle/numerors.res.oracle
+++ b/tests/value/numerors/oracle/numerors.res.oracle
@@ -292,3 +292,19 @@
 [eva:final-states] Values at end of function main:
   Frama_C_entropy_source ∈ [--..--]
   __retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  29 functions analyzed (out of 29): 100% coverage.
+  In these functions, 257 statements reached (out of 257): 100% coverage.
+  ----------------------------------------------------------------------------
+  Some errors and warnings have been raised during the analysis:
+    by the Eva analyzer:      0 errors    0 warnings
+    by the Frama-C kernel:    0 errors    3 warnings
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  Evaluation of the logical properties reached by the analysis:
+    Assertions        0 valid     0 unknown     0 invalid      0 total
+    Preconditions   146 valid     0 unknown     0 invalid    146 total
+  100% of the logical properties reached have been proven.
+  ----------------------------------------------------------------------------
diff --git a/tests/value/oracle/summary.0.res.oracle b/tests/value/oracle/summary.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..18d328c7689fe090af56982f7196f186335068d2
--- /dev/null
+++ b/tests/value/oracle/summary.0.res.oracle
@@ -0,0 +1,31 @@
+[kernel] Parsing tests/value/summary.i (no preprocessing)
+[eva] Analyzing a complete application starting at minimalist
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  undet ∈ [--..--]
+  volatile_d ∈ [--..--]
+[kernel:annot:missing-spec] tests/value/summary.i:18: Warning: 
+  Neither code nor specification for function minimalist, generating default assigns from the prototype
+[eva] using specification for function minimalist
+[eva] done for function minimalist
+[eva] ====== VALUES COMPUTED ======
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  No function to be analyzed.
+  ----------------------------------------------------------------------------
+  Some errors and warnings have been raised during the analysis:
+    by the Eva analyzer:      0 errors    0 warnings
+    by the Frama-C kernel:    0 errors    1 warning
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function minimalist:
+[from] Computing for function minimalist
+[from] Done for function minimalist
+  NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
diff --git a/tests/value/oracle/summary.1.res.oracle b/tests/value/oracle/summary.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..05e3490c3ef8a52ea6ac273e8d1acadc8a85b390
--- /dev/null
+++ b/tests/value/oracle/summary.1.res.oracle
@@ -0,0 +1,34 @@
+[kernel] Parsing tests/value/summary.i (no preprocessing)
+[eva] Analyzing a complete application starting at minimal
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  undet ∈ [--..--]
+  volatile_d ∈ [--..--]
+[eva] Recording results for minimal
+[eva] done for function minimal
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function minimal:
+  
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 1 statements reached (out of 1): 100% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  0 alarms generated by the analysis.
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
+[from] Computing for function minimal
+[from] Done for function minimal
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function minimal:
+  NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function minimal:
+    \nothing
+[inout] Inputs for function minimal:
+    \nothing
diff --git a/tests/value/oracle/summary.2.res.oracle b/tests/value/oracle/summary.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7326ccc855202f51023362d23a736ca553142729
--- /dev/null
+++ b/tests/value/oracle/summary.2.res.oracle
@@ -0,0 +1,40 @@
+[kernel] Parsing tests/value/summary.i (no preprocessing)
+[eva] Analyzing a complete application starting at bottom
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  undet ∈ [--..--]
+  volatile_d ∈ [--..--]
+[eva:alarm] tests/value/summary.i:14: Warning: division by zero. assert 0 ≢ 0;
+[eva] Recording results for bottom
+[eva] done for function bottom
+[eva] tests/value/summary.i:14: 
+  assertion 'Eva,division_by_zero' got final status invalid.
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function bottom:
+  NON TERMINATING FUNCTION
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 2): 50% coverage.
+  In this function, 1 statements reached (out of 2): 50% coverage.
+  ----------------------------------------------------------------------------
+  No errors or warnings raised during the analysis.
+  ----------------------------------------------------------------------------
+  1 alarm generated by the analysis:
+       1 division by zero
+  1 of them is a sure alarm (invalid status).
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
+[from] Computing for function bottom
+[from] Non-terminating function bottom (no dependencies)
+[from] Done for function bottom
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function bottom:
+  NON TERMINATING - NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function bottom:
+    x
+[inout] Inputs for function bottom:
+    \nothing
diff --git a/tests/value/oracle/summary.3.res.oracle b/tests/value/oracle/summary.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..58a58f35480ae093a3f912184836bb2e09ad129b
--- /dev/null
+++ b/tests/value/oracle/summary.3.res.oracle
@@ -0,0 +1,122 @@
+[kernel] Parsing tests/value/summary.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  undet ∈ [--..--]
+  volatile_d ∈ [--..--]
+[eva] computing for function alarms <- main.
+  Called from tests/value/summary.i:52.
+[eva:alarm] tests/value/summary.i:26: Warning: 
+  out of bounds read. assert \valid_read(p);
+[eva:alarm] tests/value/summary.i:28: Warning: 
+  out of bounds write. assert \valid(p);
+[eva:alarm] tests/value/summary.i:29: Warning: 
+  accessing out of bounds index. assert 0 ≤ undet;
+[eva:alarm] tests/value/summary.i:29: Warning: 
+  accessing out of bounds index. assert undet < 10;
+[eva:alarm] tests/value/summary.i:30: Warning: 
+  division by zero. assert undet ≢ 0;
+[eva:alarm] tests/value/summary.i:31: Warning: 
+  signed overflow. assert -2147483648 ≤ undet + undet;
+[eva:alarm] tests/value/summary.i:31: Warning: 
+  signed overflow. assert undet + undet ≤ 2147483647;
+[eva:alarm] tests/value/summary.i:32: Warning: 
+  invalid LHS operand for left shift. assert 0 ≤ undet;
+[eva:alarm] tests/value/summary.i:32: Warning: 
+  invalid RHS operand for shift. assert 0 ≤ undet < 32;
+[eva:alarm] tests/value/summary.i:32: Warning: 
+  signed overflow. assert undet << undet ≤ 2147483647;
+[eva:alarm] tests/value/summary.i:33: Warning: 
+  non-finite double value. assert \is_finite(volatile_d);
+[eva:alarm] tests/value/summary.i:34: Warning: 
+  non-finite double value. assert \is_finite((double)(d - d));
+[eva:alarm] tests/value/summary.i:35: Warning: 
+  overflow in conversion from floating-point to integer.
+  assert -2147483649 < d;
+[eva:alarm] tests/value/summary.i:35: Warning: 
+  overflow in conversion from floating-point to integer. assert d < 2147483648;
+[eva:alarm] tests/value/summary.i:38: Warning: 
+  pointer subtraction. assert \base_addr(p) ≡ \base_addr(q);
+[eva:alarm] tests/value/summary.i:39: Warning: 
+  pointer comparison. assert \pointer_comparable((void *)p, (void *)q);
+[eva:locals-escaping] tests/value/summary.i:42: Warning: 
+  locals {z} escaping the scope of a block of alarms through p
+[eva:alarm] tests/value/summary.i:44: Warning: 
+  accessing left-value that contains escaping addresses.
+  assert ¬\dangling(&p);
+[eva] Recording results for alarms
+[eva] Done for function alarms
+[eva] computing for function f <- main.
+  Called from tests/value/summary.i:53.
+[kernel:annot:missing-spec] tests/value/summary.i:53: Warning: 
+  Neither code nor specification for function f, generating default assigns from the prototype
+[eva] using specification for function f
+[eva] Done for function f
+[eva] computing for function g <- main.
+  Called from tests/value/summary.i:54.
+[kernel:annot:missing-spec] tests/value/summary.i:54: Warning: 
+  Neither code nor specification for function g, generating default assigns from the prototype
+[eva] using specification for function g
+[eva] Done for function g
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function alarms:
+  x ∈ [--..--]
+  y ∈ {0}
+  p ∈ {{ &x ; &y }}
+  q ∈ {{ &x ; &y }}
+  t[0..9] ∈ {0}
+  d ∈ [-2147483649. .. 2147483648.]
+[eva:final-states] Values at end of function main:
+  
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  2 functions analyzed (out of 2): 100% coverage.
+  In these functions, 32 statements reached (out of 32): 100% coverage.
+  ----------------------------------------------------------------------------
+  Some errors and warnings have been raised during the analysis:
+    by the Eva analyzer:      0 errors    1 warning
+    by the Frama-C kernel:    0 errors    2 warnings
+  ----------------------------------------------------------------------------
+  17 alarms generated by the analysis:
+       1 division by zero
+       2 invalid memory accesses
+       2 accesses out of bounds index
+       3 integer overflows
+       2 invalid shifts
+       1 escaping address
+       2 nan or infinite floating-point values
+       2 illegal conversions from floating-point to integer
+       2 others
+  ----------------------------------------------------------------------------
+  No logical properties have been reached by the analysis.
+  ----------------------------------------------------------------------------
+[from] Computing for function alarms
+[from] Done for function alarms
+[from] Computing for function main
+[from] Computing for function f <-main
+[from] Done for function f
+[from] Computing for function g <-main
+[from] Done for function g
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function alarms:
+  NO EFFECTS
+[from] Function f:
+  NO EFFECTS
+[from] Function g:
+  NO EFFECTS
+[from] Function main:
+  NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function alarms:
+    x; y; p; q; t[0..9]; d
+[inout] Inputs for function alarms:
+    undet; volatile_d
+[inout] Out (internal) for function main:
+    \nothing
+[inout] Inputs for function main:
+    undet; volatile_d
diff --git a/tests/value/summary.i b/tests/value/summary.i
new file mode 100644
index 0000000000000000000000000000000000000000..b037fa17050b083cf6758ef68c9579ea5223544e
--- /dev/null
+++ b/tests/value/summary.i
@@ -0,0 +1,55 @@
+/* run.config*
+  STDOPT: +"-eva-msg-key=summary -main minimalist"
+  STDOPT: +"-eva-msg-key=summary -main minimal"
+  STDOPT: +"-eva-msg-key=summary -main bottom"
+  STDOPT: +"-eva-msg-key=summary -main main"
+*/
+
+/* Tests the summary on the smallest possible program. */
+void minimalist ();
+void minimal () {}
+
+/* Sure alarm and non-terminating function. */
+void bottom () {
+  int x = 10 / 0;
+}
+
+volatile int undet;
+volatile double volatile_d;
+
+/* Tests the summary on most kinds of alarms. */
+void alarms () {
+  int x = 0, y = 0;
+  int *p, *q;
+  int t[10] = {0};
+  p = &x + undet;
+  x = *p;                 // invalid read memory access
+  p = &x + undet;
+  *p = x;                 // invalid write memory access
+  x = t[undet];           // out of bound index + uninitialized read
+  x = 100 / undet;        // division by zero
+  x = undet + undet;      // overflow
+  x = undet << undet;     // invalid shift
+  double d = volatile_d;
+  d = d - d;              // nan and infinite floating-point value
+  x = (int) d;            // invalid cast from floating-point to integer
+  p = undet ? &x : &y;
+  q = undet ? &y : &x;
+  if (undet) x = p - q;   // invalid pointer comparison
+  if (p < q) x = 0;       // invalid pointer comparison
+  if (undet) {
+    int z;
+    p = &z;  // eva warning about escaping z
+  }
+  x = *p;                 // dangling pointer
+}
+
+void f(void);
+void g(void);
+
+// 2 kernel warnings, 1 eva warning, no error.
+void main () {
+  alarms ();
+  f(); // kernel warning: no specification for function f
+  g(); // kernel warning: no specification for function g
+}