[Eva] Adds a new test for the analysis summary.

tests/value/oracle/summary.0.res.oracle

+[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 ======

tests/value/oracle/summary.1.res.oracle

+[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

tests/value/oracle/summary.2.res.oracle

+[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

tests/value/oracle/summary.3.res.oracle

+[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

tests/value/summary.i

+/* 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
+}