[Eva] In the summary, do not count unreachable logical properties as proven.

src/plugins/value/utils/value_results.ml

@@ -498,7 +498,8 @@ let make_report ()  =
   let report = empty_report () in
   let report_property ip =
     match ip with
-    | Property.IPCodeAnnot {Property.ica_ca} ->
+    | Property.IPCodeAnnot Property.{ ica_ca; ica_stmt; }
+      when Db.Value.is_reachable_stmt ica_stmt ->
       begin
         let status = get_status ip in
         match Alarms.find ica_ca with
@@ -510,9 +511,9 @@ let make_report ()  =
           | None | Some Property_status.True -> ()
           | _ -> report_alarm acc_alarms alarm
       end
-    | Property.IPPropertyInstance _ ->
-      let status = get_status ip in
-      report_status report.preconds status
+    | Property.IPPropertyInstance {Property.ii_stmt}
+      when Db.Value.is_reachable_stmt ii_stmt ->
+      report_status report.preconds (get_status ip)
     | _ -> ()
   in
   Property_status.iter report_property;

tests/journal/oracle/intra.res.oracle

@@ -68,7 +68,7 @@
   0 alarms generated by the analysis.
   ----------------------------------------------------------------------------
   Evaluation of the logical properties reached by the analysis:
-    Assertions        6 valid     0 unknown     0 invalid      6 total
+    Assertions        4 valid     0 unknown     0 invalid      4 total
     Preconditions     0 valid     0 unknown     0 invalid      0 total
   100% of the logical properties reached have been proven.
   ----------------------------------------------------------------------------

tests/misc/oracle/bts1201.res.oracle

@@ -35,10 +35,7 @@
   ----------------------------------------------------------------------------
   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.
+  No logical properties have been reached by the analysis.
   ----------------------------------------------------------------------------
 /* Generated by Frama-C */
 void main(void)