[Eva] Adds a test of the summary when using both RTE and Eva.

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

@@ -5,7 +5,7 @@
 [eva:initial-state] Values of globals at initialization
   undet ∈ [--..--]
   volatile_d ∈ [--..--]
-[kernel:annot:missing-spec] tests/value/summary.i:18: Warning: 
+[kernel:annot:missing-spec] tests/value/summary.i:19: 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

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

@@ -5,10 +5,10 @@
 [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:alarm] tests/value/summary.i:15: Warning: division by zero. assert 0 ≢ 0;
 [eva] Recording results for bottom
 [eva] done for function bottom
-[eva] tests/value/summary.i:14: 
+[eva] tests/value/summary.i:15: 
   assertion 'Eva,division_by_zero' got final status invalid.
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function bottom:

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

@@ -6,56 +6,56 @@
   undet ∈ [--..--]
   volatile_d ∈ [--..--]
 [eva] computing for function alarms <- main.
-  Called from tests/value/summary.i:52.
-[eva:alarm] tests/value/summary.i:26: Warning: 
+  Called from tests/value/summary.i:53.
+[eva:alarm] tests/value/summary.i:27: 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: 
+  out of bounds write. assert \valid(p);
+[eva:alarm] tests/value/summary.i:30: 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;
+  accessing out of bounds index. assert undet < 10;
 [eva:alarm] tests/value/summary.i:31: Warning: 
+  division by zero. assert undet ≢ 0;
+[eva:alarm] tests/value/summary.i:32: 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: 
+  signed overflow. assert undet + undet ≤ 2147483647;
+[eva:alarm] tests/value/summary.i:33: Warning: 
   invalid LHS operand for left shift. assert 0 ≤ undet;
-[eva:alarm] tests/value/summary.i:32: Warning: 
+[eva:alarm] tests/value/summary.i:33: 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);
+  signed overflow. assert undet << undet ≤ 2147483647;
 [eva:alarm] tests/value/summary.i:34: Warning: 
-  non-finite double value. assert \is_finite((double)(d - d));
+  non-finite double value. assert \is_finite(volatile_d);
 [eva:alarm] tests/value/summary.i:35: Warning: 
+  non-finite double value. assert \is_finite((double)(d - d));
+[eva:alarm] tests/value/summary.i:36: Warning: 
   overflow in conversion from floating-point to integer.
   assert -2147483649 < d;
-[eva:alarm] tests/value/summary.i:35: Warning: 
+[eva:alarm] tests/value/summary.i:36: 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 subtraction. assert \base_addr(p) ≡ \base_addr(q);
+[eva:alarm] tests/value/summary.i:40: Warning: 
   pointer comparison. assert \pointer_comparable((void *)p, (void *)q);
-[eva:locals-escaping] tests/value/summary.i:42: Warning: 
+[eva:locals-escaping] tests/value/summary.i:43: Warning: 
   locals {z} escaping the scope of a block of alarms through p
-[eva:alarm] tests/value/summary.i:44: Warning: 
+[eva:alarm] tests/value/summary.i:45: 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: 
+  Called from tests/value/summary.i:54.
+[kernel:annot:missing-spec] tests/value/summary.i:54: 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: 
+  Called from tests/value/summary.i:55.
+[kernel:annot:missing-spec] tests/value/summary.i:55: 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

tests/value/oracle/summary.4.res.oracle

+[kernel] Parsing tests/value/summary.i (no preprocessing)
+[rte] annotating function alarms
+[rte] annotating function bottom
+[rte] tests/value/summary.i:15: Warning: 
+  guaranteed RTE: assert division_by_zero: 0 ≢ 0;
+[rte] annotating function main
+[rte] annotating function minimal
+[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:53.
+[eva:alarm] tests/value/summary.i:27: Warning: 
+  assertion 'rte,mem_access' got status unknown.
+[eva:alarm] tests/value/summary.i:29: Warning: 
+  assertion 'rte,mem_access' got status unknown.
+[eva:alarm] tests/value/summary.i:30: Warning: 
+  assertion 'rte,index_bound' got status unknown.
+[eva:alarm] tests/value/summary.i:30: Warning: 
+  accessing out of bounds index. assert 0 ≤ undet;
+[eva:alarm] tests/value/summary.i:30: Warning: 
+  accessing out of bounds index. assert undet < 10;
+[eva:alarm] tests/value/summary.i:31: Warning: 
+  assertion 'rte,division_by_zero' got status unknown.
+[eva:alarm] tests/value/summary.i:31: Warning: 
+  division by zero. assert undet ≢ 0;
+[eva:alarm] tests/value/summary.i:32: Warning: 
+  assertion 'rte,signed_overflow' got status unknown.
+[eva:alarm] tests/value/summary.i:32: Warning: 
+  signed overflow. assert -2147483648 ≤ undet + undet;
+[eva:alarm] tests/value/summary.i:32: Warning: 
+  signed overflow. assert undet + undet ≤ 2147483647;
+[eva:alarm] tests/value/summary.i:33: Warning: 
+  assertion 'rte,shift' got status unknown.
+[eva:alarm] tests/value/summary.i:33: Warning: 
+  assertion 'rte,shift' got status unknown.
+[eva:alarm] tests/value/summary.i:33: Warning: 
+  assertion 'rte,signed_overflow' got status unknown.
+[eva:alarm] tests/value/summary.i:33: Warning: 
+  invalid LHS operand for left shift. assert 0 ≤ undet;
+[eva:alarm] tests/value/summary.i:33: Warning: 
+  invalid RHS operand for shift. assert 0 ≤ undet < 32;
+[eva:alarm] tests/value/summary.i:33: Warning: 
+  signed overflow. assert undet << undet ≤ 2147483647;
+[eva:alarm] tests/value/summary.i:34: Warning: 
+  non-finite double value. assert \is_finite(volatile_d);
+[eva:alarm] tests/value/summary.i:35: Warning: 
+  assertion 'rte,is_nan_or_infinite' got status unknown.
+[eva:alarm] tests/value/summary.i:35: Warning: 
+  non-finite double value. assert \is_finite((double)(d - d));
+[eva:alarm] tests/value/summary.i:36: Warning: 
+  assertion 'rte,float_to_int' got status unknown.
+[eva:alarm] tests/value/summary.i:39: Warning: 
+  pointer subtraction. assert \base_addr(p) ≡ \base_addr(q);
+[eva:alarm] tests/value/summary.i:40: Warning: 
+  pointer comparison. assert \pointer_comparable((void *)p, (void *)q);
+[eva:locals-escaping] tests/value/summary.i:43: Warning: 
+  locals {z} escaping the scope of a block of alarms through p
+[eva:alarm] tests/value/summary.i:45: Warning: 
+  assertion 'rte,mem_access' got status unknown.
+[eva:alarm] tests/value/summary.i:45: 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:54.
+[kernel:annot:missing-spec] tests/value/summary.i:54: 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:55.
+[kernel:annot:missing-spec] tests/value/summary.i:55: 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 4): 50% 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
+  ----------------------------------------------------------------------------
+  18 alarms generated by the analysis:
+       1 division by zero
+       3 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

@@ -3,6 +3,7 @@
   STDOPT: +"-eva-msg-key=summary -main minimal"
   STDOPT: +"-eva-msg-key=summary -main bottom"
   STDOPT: +"-eva-msg-key=summary -main main"
+  STDOPT: +"-rte -eva-msg-key=summary -main main"
 */
 
 /* Tests the summary on the smallest possible program. */