From 70bbfd97d2ee2f2c844fa81208f64ded3136a24d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 10 Aug 2023 14:58:27 +0200
Subject: [PATCH] [Eva] Improves test of multiple domains at once.

---
 tests/value/domains.i                 | 43 ++++++++++++++++++---------
 tests/value/oracle/domains.res.oracle | 22 +++++++++-----
 2 files changed, 43 insertions(+), 22 deletions(-)

diff --git a/tests/value/domains.i b/tests/value/domains.i
index 22b198ea39f..4d00d8b9d74 100644
--- a/tests/value/domains.i
+++ b/tests/value/domains.i
@@ -1,25 +1,40 @@
 /* run.config*
-   STDOPT: #"-eva-domains sign,equality,bitwise,symbolic-locations,gauges -eva-slevel 2"
+   STDOPT: #"-eva-domains sign,equality,bitwise,symbolic-locations,gauges,octagon,multidim"
 */
 
-/*  Tests five domains together. */
+volatile int nondet;
+
+/*  Tests multiple domains together. */
 void main (int a) {
-  int b, i, k, r;
-  /* Tests the equality domain: b is reduced after the condition, no overflow. */
-  b = a;
-  if (a < 10)
-    r = b + 1;
-  /* Tests the symbolic locations domain: t[i] is smaller than 10, no overflow. */
-  int t[2] = {a, a};
-  i = a > 0;
-  if (t[i] < 10)
-    r = t[i] + 1;
+  int i, j, k, r;
+  int t[100];
+  /* Tests the multidim domain: the array is initialized after the loop. */
+  for (i = 0; i < 100; i++) {
+    t[i] = nondet;
+  }
+  i = t[64];
+  /* Tests the equality domain: i is reduced through the condition,
+     no invalid read. */
+  int b1 = i <= 0;
+  int b2 = i >= 100;
+  if (b1 || b2)
+    i = 1;
+  r = t[i];
+  /* Tests the symbolic locations domain: t[i]/i is smaller than 1000,
+     no overflow. */
+  if (t[i] / i < 1000)
+    r = t[i] / i + 1;
   /* Tests the gauges domain: k==i during the loop, no overflow. */
   k = 0;
-  while (k < 12) {
+  j = 10;
+  while (k < 200 && nondet) {
     k++;
-    i++;
+    j++;
   }
+  /* Tests the octagon domain. */
+  r = i - j + 1;
+  k = r + j;
+  r = t[k-1];
   /* Tests the sign domain: no division by zero. */
   if (a != 0)
     r = 100 / a;
diff --git a/tests/value/oracle/domains.res.oracle b/tests/value/oracle/domains.res.oracle
index 5bb482d01c2..d4fe3a14f49 100644
--- a/tests/value/oracle/domains.res.oracle
+++ b/tests/value/oracle/domains.res.oracle
@@ -1,20 +1,26 @@
 [kernel] Parsing domains.i (no preprocessing)
+[eva:experimental] Warning: The multidim domain is experimental.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
-  
-[eva:partition] domains.i:19: starting to merge loop iterations
+  nondet ∈ [--..--]
+[eva:partition] domains.i:12: starting to merge loop iterations
+[eva:partition] domains.i:30: starting to merge loop iterations
 [eva] Recording results for main
 [eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   a ∈ {8}
-  b ∈ [--..--]
-  i ∈ [1..2147483647]
-  k ∈ {12}
+  i ∈ [1..99]
+  j ∈ [10..210]
+  k ∈ [2..100]
   r ∈ {1}
-  t[0..1] ∈ [--..--]
+  t[0..63] ∈ [--..--] or UNINITIALIZED
+   [64] ∈ [--..--]
+   [65..99] ∈ [--..--] or UNINITIALIZED
+  b1 ∈ {0; 1}
+  b2 ∈ {0; 1}
 [from] Computing for function main
 [from] Done for function main
 [from] ====== DEPENDENCIES COMPUTED ======
@@ -23,6 +29,6 @@
   NO EFFECTS
 [from] ====== END OF DEPENDENCIES ======
 [inout] Out (internal) for function main:
-    a; b; i; k; r; t[0..1]
+    a; i; j; k; r; t[0..99]; b1; b2
 [inout] Inputs for function main:
-    \nothing
+    nondet
-- 
GitLab