[eva] annotate dead code

src/plugins/eva/utils/annot.ml

@@ -250,9 +250,13 @@ let eval_instr ?callstack ?name stmt =
     match callstack with
     | None -> r
     | Some c -> Results.in_callstack c r in
-  let engine = new evaluator request in
-  let _ = Visitor.visitFramacStmt (engine :> visitor) stmt in
-  List.map (predicate ?name ~loc:(Cil_datatype.Stmt.loc stmt)) engine#flush
+  List.map (predicate ?name ~loc:(Cil_datatype.Stmt.loc stmt)) @@
+  if Results.is_empty request then [False] else
+    let engine = new evaluator request in
+    let _ = Visitor.visitFramacStmt (engine :> visitor) stmt in
+    engine#flush
+
+let is_dead stmt = Results.is_empty @@ Results.before stmt
 
 (* -------------------------------------------------------------------------- *)
 (* --- Annotation Generator                                               --- *)
@@ -285,7 +289,7 @@ class generator =
                     Property_status.emit Analysis.emitter ~hyps:[] ip True
                  ) (Property.ip_of_code_annot kf stmt ca)
           ) stmt ;
-        DoChildren
+        if is_dead stmt then SkipChildren else DoChildren
 
   end
 

tests/misc/eva_annot_dead.c

+/* run.config
+   PLUGIN: @EVA_PLUGINS@
+   OPT: -eva -eva-annot main -print
+*/
+
+/* -------------------------------------------------------------------------- */
+/* --- Testing EVA Annotations                                            --- */
+/* -------------------------------------------------------------------------- */
+
+int main(int a) {
+  int b = 0;
+  if (a < 0) { a = 1; b++; }
+  if (a < 0) { a = 2; b++; }
+  return b;
+}
+
+/* -------------------------------------------------------------------------- */

tests/misc/oracle/eva_annot_dead.res.oracle

+[kernel] Parsing eva_annot_dead.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva:initial-state] Values of globals at initialization
+  
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  a ∈ [0..2147483647]
+  b ∈ {0; 1}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 1): 100% coverage.
+  In this function, 6 statements reached (out of 8): 75% 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] Annotate main
+/* Generated by Frama-C */
+int main(int a)
+{
+  int b = 0;
+  /*@ assert Eva_domain: -2147483648 ≤ a ≤ 2147483647; */
+  if (a < 0) {
+    a = 1;
+    /*@ assert Eva_domain: b ≡ 0; */
+    b ++;
+  }
+  /*@ assert Eva_domain: 0 ≤ a ≤ 2147483647; */
+  if (a < 0) {
+    /*@ assert Eva_domain: \false; */
+    a = 2;
+    /*@ assert Eva_domain: \false; */
+    b ++;
+  }
+  /*@ assert Eva_domain: 0 ≤ b ≤ 1; */
+  return b;
+}
+
+