From 638c7d98661247f8cedcf38b16c48a1e07bda574 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 20 Jan 2025 14:33:33 +0100
Subject: [PATCH] [Eva] Adds test printing the offsetmap of a scalar variable.

---
 tests/value/domains.i                 |  5 +++++
 tests/value/oracle/domains.res.oracle | 22 ++++++++++++++++++++--
 tests/value/oracle/domains_dump_0     |  4 +++-
 3 files changed, 28 insertions(+), 3 deletions(-)

diff --git a/tests/value/domains.i b/tests/value/domains.i
index cbb0f5f20a..defe295b67 100644
--- a/tests/value/domains.i
+++ b/tests/value/domains.i
@@ -50,4 +50,9 @@ void main (int a) {
   Frama_C_domain_show_each(a, i, j, k, r);
   Frama_C_dump_each();
   Frama_C_dump_each_file_domains_dump();
+
+  /* Tests printing offsetmap of scalar value. */
+  int scalar = 65537;
+  *(((char *)&scalar)+1) = 42;
+  Frama_C_domain_show_each(scalar);
 }
diff --git a/tests/value/oracle/domains.res.oracle b/tests/value/oracle/domains.res.oracle
index b189955388..55968e3431 100644
--- a/tests/value/oracle/domains.res.oracle
+++ b/tests/value/oracle/domains.res.oracle
@@ -62,6 +62,7 @@
    [65..99] ∈ [--..--] or UNINITIALIZED
   b1 ∈ {0; 1}
   b2 ∈ {0; 1}
+  scalar ∈ UNINITIALIZED
   # equality:
   {k = ((i - j) + 1) + j}
   # symbolic-locations:
@@ -117,10 +118,24 @@
             },
               {})
       b1 -> ({0; 1}, {})
-      b2 -> ({0; 1}, {}) ]},
+      b2 -> ({0; 1}, {})
+      scalar -> (UNINITIALIZED, {}) ]},
      None)
   ==END OF DUMP==
 [eva] domains.i:52: Dumping state in file 'domains_dump_0'
+[eva] domains.i:57: 
+  Frama_C_domain_show_each:
+  scalar : # cvalue: [bits 0 to 7]# ∈ {65537}%32, bits 0 to 7 
+                     [bits 8 to 15] ∈ {42}
+                     [bits 16 to 31]# ∈ {65537}%32, bits 16 to 31 
+                     This amounts to: {76289}
+           # equality: 
+           # symbolic-locations: (not implemented)
+           # octagon: (not implemented)
+           # gauges: (not implemented)
+           # sign: -0+
+           # bitwise: (not implemented)
+           # multidim: T
 [eva] Recording results for main
 [eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -135,6 +150,9 @@
    [65..99] ∈ [--..--] or UNINITIALIZED
   b1 ∈ {0; 1}
   b2 ∈ {0; 1}
+  scalar[bits 0 to 7]# ∈ {65537}%32, bits 0 to 7 
+        [bits 8 to 15] ∈ {42}
+        [bits 16 to 31]# ∈ {65537}%32, bits 16 to 31 
 [from] Computing for function main
 [from] Done for function main
 [from] ====== DEPENDENCIES COMPUTED ======
@@ -143,6 +161,6 @@
   NO EFFECTS
 [from] ====== END OF DEPENDENCIES ======
 [inout] Out (internal) for function main:
-    a; i; j; k; r; t[0..99]; b1; b2
+    a; i; j; k; r; t[0..99]; b1; b2; scalar
 [inout] Inputs for function main:
     nondet
diff --git a/tests/value/oracle/domains_dump_0 b/tests/value/oracle/domains_dump_0
index 243759089d..69dce4193f 100644
--- a/tests/value/oracle/domains_dump_0
+++ b/tests/value/oracle/domains_dump_0
@@ -11,6 +11,7 @@ t[0..63] ∈ [--..--] or UNINITIALIZED
  [65..99] ∈ [--..--] or UNINITIALIZED
 b1 ∈ {0; 1}
 b2 ∈ {0; 1}
+scalar ∈ UNINITIALIZED
 # equality:
 {k = ((i - j) + 1) + j}
 # symbolic-locations:
@@ -66,5 +67,6 @@ a[bits 0 to 2] ∈ {0}
           },
             {})
     b1 -> ({0; 1}, {})
-    b2 -> ({0; 1}, {}) ]},
+    b2 -> ({0; 1}, {})
+    scalar -> (UNINITIALIZED, {}) ]},
    None)
-- 
GitLab