From 0e3ec3deb23e37bb1fd5003f28cd4bb0fb2b41a4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 9 Nov 2020 14:22:56 +0100
Subject: [PATCH] [Eva] New test file widening_thresholds.

---
 .../oracle/widening_thresholds.res.oracle     | 66 +++++++++++++++++++
 tests/value/widening_thresholds.i             | 27 ++++++++
 2 files changed, 93 insertions(+)
 create mode 100644 tests/value/oracle/widening_thresholds.res.oracle
 create mode 100644 tests/value/widening_thresholds.i

diff --git a/tests/value/oracle/widening_thresholds.res.oracle b/tests/value/oracle/widening_thresholds.res.oracle
new file mode 100644
index 00000000000..af0372f3b04
--- /dev/null
+++ b/tests/value/oracle/widening_thresholds.res.oracle
@@ -0,0 +1,66 @@
+[kernel] Parsing tests/value/widening_thresholds.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 ∈ [--..--]
+  g ∈ {0}
+[eva] computing for function modulo <- main.
+  Called from tests/value/widening_thresholds.i:26.
+[eva] computing for function incr_modulo <- modulo <- main.
+  Called from tests/value/widening_thresholds.i:21.
+[eva] Recording results for incr_modulo
+[eva] Done for function incr_modulo
+[eva] tests/value/widening_thresholds.i:18: starting to merge loop iterations
+[eva] computing for function incr_modulo <- modulo <- main.
+  Called from tests/value/widening_thresholds.i:21.
+[eva] Recording results for incr_modulo
+[eva] Done for function incr_modulo
+[eva] computing for function incr_modulo <- modulo <- main.
+  Called from tests/value/widening_thresholds.i:21.
+[eva] Recording results for incr_modulo
+[eva] Done for function incr_modulo
+[eva] computing for function incr_modulo <- modulo <- main.
+  Called from tests/value/widening_thresholds.i:21.
+[eva] Recording results for incr_modulo
+[eva] Done for function incr_modulo
+[eva] Recording results for modulo
+[eva] Done for function modulo
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function incr_modulo:
+  g ∈ [0..999]
+[eva:final-states] Values at end of function modulo:
+  s ∈ [0..9]
+  i ∈ [0..99]
+  g ∈ [0..999]
+[eva:final-states] Values at end of function main:
+  g ∈ [0..999]
+[from] Computing for function incr_modulo
+[from] Done for function incr_modulo
+[from] Computing for function modulo
+[from] Done for function modulo
+[from] Computing for function main
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function incr_modulo:
+  g FROM g
+[from] Function modulo:
+  g FROM nondet; g (and SELF)
+[from] Function main:
+  g FROM nondet; g (and SELF)
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function incr_modulo:
+    g
+[inout] Inputs for function incr_modulo:
+    g
+[inout] Out (internal) for function modulo:
+    s; i; g
+[inout] Inputs for function modulo:
+    nondet; g
+[inout] Out (internal) for function main:
+    g
+[inout] Inputs for function main:
+    nondet; g
diff --git a/tests/value/widening_thresholds.i b/tests/value/widening_thresholds.i
new file mode 100644
index 00000000000..a1d332c5c8f
--- /dev/null
+++ b/tests/value/widening_thresholds.i
@@ -0,0 +1,27 @@
+/* run.config*
+  STDOPT: +""
+*/
+
+/* Tests the inference of widening thresholds. */
+
+volatile int nondet;
+static int g;
+
+void incr_modulo (void) {
+  g = (g + 1) % 1000;
+}
+
+/* Tests the inference of widening thresholds according to modulo operations. */
+void modulo (void) {
+  short s = 0;
+  int i = 17;
+  while (nondet) {
+    s = (s + 1) % 10;
+    i = (i + 3) % 100;
+    incr_modulo();
+  }
+}
+
+void main (void) {
+  modulo();
+}
-- 
GitLab