From d0745437df7bb692b277b0d051f52affc55f8ed3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 20 Jan 2025 21:05:41 +0100
Subject: [PATCH] [Eva] Adds a test of a "clean" analysis stop when aborting
with -save.
---
tests/value/clean_abort.i | 55 ++++++++++++++++++++
tests/value/oracle/clean_abort.res.oracle | 62 +++++++++++++++++++++++
tests/value/oracle/clean_abort_sav.res | 27 ++++++++++
3 files changed, 144 insertions(+)
create mode 100644 tests/value/clean_abort.i
create mode 100644 tests/value/oracle/clean_abort.res.oracle
create mode 100644 tests/value/oracle/clean_abort_sav.res
diff --git a/tests/value/clean_abort.i b/tests/value/clean_abort.i
new file mode 100644
index 0000000000..d06a5c35c0
--- /dev/null
+++ b/tests/value/clean_abort.i
@@ -0,0 +1,55 @@
+/* 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);
+}
diff --git a/tests/value/oracle/clean_abort.res.oracle b/tests/value/oracle/clean_abort.res.oracle
new file mode 100644
index 0000000000..284520def2
--- /dev/null
+++ b/tests/value/oracle/clean_abort.res.oracle
@@ -0,0 +1,62 @@
+[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
+--------------------------------------------------------------------------------
diff --git a/tests/value/oracle/clean_abort_sav.res b/tests/value/oracle/clean_abort_sav.res
new file mode 100644
index 0000000000..575493d727
--- /dev/null
+++ b/tests/value/oracle/clean_abort_sav.res
@@ -0,0 +1,27 @@
+[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'.
--
GitLab