[Metrics] fix crash with -metrics-eva-cover and unvisited ACSL references

src/plugins/metrics/metrics_coverage.ml

@@ -150,7 +150,13 @@ class deadCallsVisitor fmt ~libc cov_metrics =
         match self#current_kf with
         | None ->
           (match current_initializer with
-           | None -> assert false
+           | None ->
+             (* This can happen in the rare cases a function is referenced by
+                a specification *)
+             Format.fprintf fmt
+               "@[<h>%s referenced by an ACSL specification (at %a)@]@ "
+               vi.vname
+               Location.pretty (Cil.CurrentLoc.get ())
            | Some vinit ->
              Format.fprintf fmt
                "@[<h>Initializer of %s references %s (at %t)@]@ "

tests/metrics/oracle/referenced-by-acsl.res.oracle

+[kernel] Parsing tests/metrics/referenced-by-acsl.c (with preprocessing)
+[metrics] Defined functions (2)
+  =====================
+   f (address taken) (0 call); main (0 call); 
+  
+  Specified-only functions (0)
+  ============================
+   
+  
+  Undefined and unspecified functions (0)
+  =======================================
+   
+  
+  'Extern' global variables (0)
+  =============================
+   
+  
+  Potential entry points (1)
+  ==========================
+   main; 
+  
+  Global metrics
+  ============== 
+  Sloc = 3
+  Decision point = 0
+  Global variables = 0
+  If = 0
+  Loop = 0
+  Goto = 0
+  Assignment = 1
+  Exit point = 2
+  Function = 2
+  Function call = 0
+  Pointer dereferencing = 0
+  Cyclomatic complexity = 2
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  
+[eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  1 function analyzed (out of 2): 50% 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 = 2 (out of 2)
+  Semantically reached functions = 1
+  Coverage estimation = 50.0% 
+  
+  Unreached functions (1) =
+    <tests/metrics/referenced-by-acsl.c>: f;
+[metrics] References to non-analyzed functions
+  ------------------------------------
+  f referenced by an ACSL specification (at tests/metrics/referenced-by-acsl.c:7)
+[metrics] Statements analyzed by Eva
+  --------------------------
+  2 stmts in analyzed functions, 2 stmts analyzed (100.0%)
+  main: 2 stmts out of 2 (100.0%)

tests/metrics/referenced-by-acsl.c

+/* run.config
+   STDOPT: +"-metrics-eva-cover"
+**/
+
+void f() {}
+
+/*@ requires \valid_function(&f); */
+int main () {}