[Eva] Adds a test of a "clean" analysis stop when aborting with -save.

tests/value/clean_abort.i

+/* run.config
+  EXIT: 1
+  EXECNOW: BIN @PTEST_NAME@.sav.error LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ -eva @EVA_OPTIONS@ -eva-stop-at-nth-alarm 4 @PTEST_FILE@ -save @PTEST_NAME@.sav > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
+  EXIT: 0
+  PLUGIN: @PTEST_PLUGIN@ report
+  OPT: -load %{dep:@PTEST_NAME@.sav.error} -out -input -deps -report
+*/
+/* run.config*
+   DONTRUN: avoids duplication of oracles
+*/
+
+/* Tests the "clean" stop of the analysis (here via -eva-stop-at-nth-alarm)
+   with -save name: save a valid session file "name.error", which can then be
+   reloaded and contains partial results of the functions analyzed before the
+   crash. */
+
+volatile unsigned int nondet;
+
+int t[10];
+
+int g;
+
+/* Completely analyzed: results should be correct. */
+void init (int x) {
+  int i = 0;
+  //@ loop unroll 10;
+  for (; i < 10; i++) {
+    t[i] = nondet % x;  // alarm: modulo by zero
+  }
+  g = t[x];             // alarm: out of bound index
+  if (nondet) g = t[i]; // invalid alarm: out of bound index
+  //@ assert valid: i == 10;
+}
+
+/* Partially analyzed, so partial results… */
+void partial (int x) {
+  //@ assert valid: 0 <= x;
+  g = 100 / x; // division by zero
+  // The analysis stops here. Alarms below are never emitted.
+  g = nondet + x; // overflow alarm
+  g = t[x];       // out of bounds alarms
+  //@ assert unreached: g > 0;
+}
+
+/* Unreached by the analysis, as it stops before. */
+void unreached (int x) {
+  g = x / x;
+  //@ assert unreached: g == 1;
+}
+
+void main (void) {
+  init(nondet % 100);
+  partial(nondet % 100);
+  unreached(nondet % 100);
+}

tests/value/oracle/clean_abort.res.oracle

+[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
+[from] Computing for function init
+[from] Done for function init
+[from] Computing for function partial
+[from] Non-terminating function partial (no dependencies)
+[from] Done for function partial
+[from] Computing for function main
+[from] Non-terminating function main (no dependencies)
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function init:
+  t[0..9] FROM nondet; x (and SELF)
+  g FROM nondet; t[1..9]; x
+[from] Function partial:
+  NON TERMINATING - NO EFFECTS
+[from] Function main:
+  NON TERMINATING - NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function init:
+    t[0..9]; g; i
+[inout] Inputs for function init:
+    nondet; t[1..9]
+[inout] Out (internal) for function partial:
+    g
+[inout] Inputs for function partial:
+    \nothing
+[inout] Out (internal) for function main:
+    t[0..9]; g
+[inout] Inputs for function main:
+    nondet; t[1..9]
+[report] Computing properties status...
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'init'
+--------------------------------------------------------------------------------
+
+[  Valid  ] Assertion 'valid' (file clean_abort.i, line 32)
+            by Eva.
+[    -    ] Assertion 'Eva,division_by_zero' (file clean_abort.i, line 28)
+            tried with Eva.
+[    -    ] Assertion 'Eva,index_bound' (file clean_abort.i, line 30)
+            tried with Eva.
+[    -    ] Assertion 'Eva,index_bound' (file clean_abort.i, line 31)
+            tried with Eva.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'partial'
+--------------------------------------------------------------------------------
+
+[  Valid  ] Assertion 'valid' (file clean_abort.i, line 37)
+            by Eva.
+[    -    ] Assertion 'Eva,division_by_zero' (file clean_abort.i, line 38)
+            tried with Eva.
+
+--------------------------------------------------------------------------------
+--- Status Report Summary
+--------------------------------------------------------------------------------
+     2 Completely validated
+     4 To be validated
+     6 Total
+--------------------------------------------------------------------------------

tests/value/oracle/clean_abort_sav.res

+[kernel] Parsing clean_abort.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
+  nondet ∈ [--..--]
+  t[0..9] ∈ {0}
+  g ∈ {0}
+[eva] computing for function init <- main.
+  Called from clean_abort.i:52.
+[eva:alarm] clean_abort.i:28: Warning: 
+  division by zero. assert (unsigned int)x ≢ 0;
+[eva:alarm] clean_abort.i:30: Warning: 
+  accessing out of bounds index. assert x < 10;
+[eva:alarm] clean_abort.i:31: Warning: 
+  accessing out of bounds index. assert i < 10;
+[eva] clean_abort.i:32: assertion 'valid' got status valid.
+[eva] Recording results for init
+[eva] Done for function init
+[eva] computing for function partial <- main.
+  Called from clean_abort.i:53.
+[eva] clean_abort.i:37: assertion 'valid' got status valid.
+[eva:alarm] clean_abort.i:38: Warning: division by zero. assert x ≢ 0;
+[eva] User Error: Stopping at nth alarm
+[eva] Clean up and save partial results.
+[kernel] Plug-in eva aborted: invalid user input.
+[kernel] Warning: attempting to save on non-zero exit code: modifying filename into `clean_abort.sav.error'.