From bfa39cc037d75de60fba3a650f6bc0975f7e942e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 11 Jun 2024 22:41:46 +0200
Subject: [PATCH] [Eva] Adds a test of a soundness issue in offsetmaps.
---
tests/value/offsetmap.i | 38 ++-
tests/value/oracle/offsetmap.0.res.oracle | 50 +++-
tests/value/oracle/offsetmap.1.res.oracle | 48 +++-
tests/value/oracle/offsetmap.2.res.oracle | 237 ++++++++++++++++++
.../value/oracle_apron/offsetmap.0.res.oracle | 8 +-
.../value/oracle_apron/offsetmap.1.res.oracle | 18 +-
.../value/oracle_apron/offsetmap.2.res.oracle | 22 ++
.../oracle_equality/offsetmap.2.res.oracle | 4 +
.../oracle_octagon/offsetmap.2.res.oracle | 4 +
.../oracle_symblocs/offsetmap.2.res.oracle | 4 +
10 files changed, 407 insertions(+), 26 deletions(-)
create mode 100644 tests/value/oracle/offsetmap.2.res.oracle
create mode 100644 tests/value/oracle_apron/offsetmap.2.res.oracle
create mode 100644 tests/value/oracle_equality/offsetmap.2.res.oracle
create mode 100644 tests/value/oracle_octagon/offsetmap.2.res.oracle
create mode 100644 tests/value/oracle_symblocs/offsetmap.2.res.oracle
diff --git a/tests/value/offsetmap.i b/tests/value/offsetmap.i
index 74db362fd49..9aab8c31905 100644
--- a/tests/value/offsetmap.i
+++ b/tests/value/offsetmap.i
@@ -1,6 +1,6 @@
/* run.config*
-
- STDOPT: #""
+ STDOPT: #"-eva-ilevel 8"
+ STDOPT: #"-eva-ilevel 2"
STDOPT: #"-eva-warn-copy-indeterminate=-f,-g"
*/
@@ -70,8 +70,42 @@ void g(int i) {
char c2 = *q;
}
+/*@ assigns \result \from min, max;
+ ensures min <= \result <= max; */
+int Frama_C_interval(int min, int max);
+
+/* Test the soundness in offsetmaps when:
+ - writing an isotropic value [v] (all bits are 0, or all bits are 1);
+ - to an imprecise abstract location when all possible locations are
+ contiguous and non-overlapping;
+ - the number of possible locations is strictly greater than -eva-ilevel;
+ - the target location contains a value with a different size or alignment
+ than the write of [v]. */
+void h(void) {
+ int x = 257;
+ /* Writing one byte to 0 in 4-byte integer x. */
+ int i = Frama_C_interval(0, 3);
+ char *p = (char *)&x + i;
+ *p = 0;
+ Frama_C_show_each_1_256_257(x); // Must at least contain 1, 256 and 257.
+ /* Same operation on 4-byte pointer p. */
+ int *q = &x;
+ p = (char *)&q + i;
+ *p = 0; // q is now completely invalid and should be a garbled mix.
+ if (q != 0) *q = 42; // Thus there must be a memory access alarm here.
+ /* Unaligned write in an array. */
+ short t[8];
+ //@ loop unroll 8;
+ for (int j = 0; j < 8; j++) { t[j] = 257; }
+ p = (char *)t + 1;
+ i = Frama_C_interval(0, 6);
+ short *sp = (short *)p + i;
+ *sp = 0;
+ Frama_C_show_each_1_256_257(t[4]); // Must at least contain 1, 256 and 257.
+}
void main (int i) {
f();
g(i);
+ h();
}
diff --git a/tests/value/oracle/offsetmap.0.res.oracle b/tests/value/oracle/offsetmap.0.res.oracle
index 7172b2b74c3..8dd87df7eb7 100644
--- a/tests/value/oracle/offsetmap.0.res.oracle
+++ b/tests/value/oracle/offsetmap.0.res.oracle
@@ -24,7 +24,7 @@
a2 ∈ {0}
s[0..9999999] ∈ {0}
[eva] computing for function f <- main.
- Called from offsetmap.i:75.
+ Called from offsetmap.i:108.
[eva] offsetmap.i:19: starting to merge loop iterations
[eva] offsetmap.i:29: starting to merge loop iterations
[eva:alarm] offsetmap.i:51: Warning:
@@ -32,7 +32,7 @@
[eva] Recording results for f
[eva] Done for function f
[eva] computing for function g <- main.
- Called from offsetmap.i:76.
+ Called from offsetmap.i:109.
[eva:alarm] offsetmap.i:66: Warning:
accessing out of bounds index. assert 0 ≤ i_0;
[eva:alarm] offsetmap.i:66: Warning:
@@ -41,6 +41,22 @@
[kernel] offsetmap.i:68:
more than 200(10000000) elements to enumerate. Approximating.
[eva] Done for function g
+[eva] computing for function h <- main.
+ Called from offsetmap.i:110.
+[eva] computing for function Frama_C_interval <- h <- main.
+ Called from offsetmap.i:87.
+[eva] using specification for function Frama_C_interval
+[eva] Done for function Frama_C_interval
+[eva] offsetmap.i:90: Frama_C_show_each_1_256_257: {0; 1; 256; 257}
+[eva:alarm] offsetmap.i:95: Warning:
+ pointer comparison. assert \pointer_comparable((void *)q, (void *)0);
+[eva:alarm] offsetmap.i:95: Warning: out of bounds write. assert \valid(q);
+[eva] computing for function Frama_C_interval <- h <- main.
+ Called from offsetmap.i:101.
+[eva] Done for function Frama_C_interval
+[eva] offsetmap.i:104: Frama_C_show_each_1_256_257: {0; 1; 256; 257}
+[eva] Recording results for h
+[eva] Done for function h
[eva] Recording results for main
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
@@ -88,6 +104,24 @@
c1 ∈ {0; 7}
q ∈ {{ &s + [0..9999999] }}
c2 ∈ {0; 1; 3; 7; 8}
+[eva:final-states] Values at end of function h:
+ x[bits 0 to 7]# ∈ {0; 42; 257}%32, bits 0 to 7
+ [bits 8 to 15]# ∈ {0; 42; 257}%32, bits 8 to 15
+ [bits 16 to 23]# ∈ {0; 42; 257}%32, bits 16 to 23
+ [bits 24 to 31]# ∈ {0; 42; 257}%32, bits 24 to 31
+ i_0 ∈ {0; 1; 2; 3; 4; 5; 6}
+ p_0 ∈ {{ &t + {1} }}
+ q ∈ {{ NULL ; &x }}
+ t[0][bits 0 to 7]# ∈ {257}%16, bits 0 to 7
+ [bits 8 to 23]# ∈ {0; 257} repeated %16, bits 8 to 23
+ [bits 24 to 39]# ∈ {0; 257} repeated %16, bits 8 to 23
+ [bits 40 to 55]# ∈ {0; 257} repeated %16, bits 8 to 23
+ [bits 56 to 71]# ∈ {0; 257} repeated %16, bits 8 to 23
+ [bits 72 to 87]# ∈ {0; 257} repeated %16, bits 8 to 23
+ [bits 88 to 103]# ∈ {0; 257} repeated %16, bits 8 to 23
+ [bits 104 to 119]# ∈ {0; 257} repeated %16, bits 8 to 23
+ [7][bits 8 to 15]# ∈ {257}%16, bits 8 to 15
+ sp ∈ {{ &t + {1; 3; 5; 7; 9; 11; 13} }}
[eva:final-states] Values at end of function main:
TT[0][bits 0 to 7]# ∈ [0..8]%32, bits 0 to 7
[bits 8 to 39]# ∈ [0..8] repeated %32, bits 8 to 39
@@ -131,10 +165,16 @@
[from] Done for function f
[from] Computing for function g
[from] Done for function g
+[from] Computing for function h
+[from] Computing for function Frama_C_interval <-h
+[from] Done for function Frama_C_interval
+[from] Done for function h
[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 Frama_C_interval:
+ \result FROM min; max
[from] Function f:
TT{[0..8]; [9][bits 0 to 7]} FROM \nothing (and SELF)
T{{[0][bits 8 to 31]; [1..5]}; {[7..8]; [9][bits 0 to 7]}}
@@ -153,6 +193,8 @@
a2 FROM \nothing
[from] Function g:
s[0..9999999] FROM i_0 (and SELF)
+[from] Function h:
+ NO EFFECTS
[from] Function main:
TT{[0..8]; [9][bits 0 to 7]} FROM \nothing (and SELF)
T{{[0][bits 8 to 31]; [1..5]}; {[7..8]; [9][bits 0 to 7]}}
@@ -181,6 +223,10 @@
s[0..9999999]; p_0; c1; q; c2
[inout] Inputs for function g:
s{[0..9999998]; [9999999][bits 0 to 7]}
+[inout] Out (internal) for function h:
+ x; i_0; p_0; q; t[0..7]; j; sp
+[inout] Inputs for function h:
+ \nothing
[inout] Out (internal) for function main:
TT{[0..8]; [9][bits 0 to 7]};
T{[0][bits 8 to 31]; [1..8]; [9][bits 0 to 7]}; i; a; b; a7; b7;
diff --git a/tests/value/oracle/offsetmap.1.res.oracle b/tests/value/oracle/offsetmap.1.res.oracle
index 396fe80c6c4..e4a0ef1e213 100644
--- a/tests/value/oracle/offsetmap.1.res.oracle
+++ b/tests/value/oracle/offsetmap.1.res.oracle
@@ -24,7 +24,7 @@
a2 ∈ {0}
s[0..9999999] ∈ {0}
[eva] computing for function f <- main.
- Called from offsetmap.i:75.
+ Called from offsetmap.i:108.
[eva] offsetmap.i:19: starting to merge loop iterations
[eva] offsetmap.i:29: starting to merge loop iterations
[eva:alarm] offsetmap.i:51: Warning:
@@ -32,7 +32,7 @@
[eva] Recording results for f
[eva] Done for function f
[eva] computing for function g <- main.
- Called from offsetmap.i:76.
+ Called from offsetmap.i:109.
[eva:alarm] offsetmap.i:66: Warning:
accessing out of bounds index. assert 0 ≤ i_0;
[eva:alarm] offsetmap.i:66: Warning:
@@ -41,6 +41,19 @@
[kernel] offsetmap.i:68:
more than 200(10000000) elements to enumerate. Approximating.
[eva] Done for function g
+[eva] computing for function h <- main.
+ Called from offsetmap.i:110.
+[eva] computing for function Frama_C_interval <- h <- main.
+ Called from offsetmap.i:87.
+[eva] using specification for function Frama_C_interval
+[eva] Done for function Frama_C_interval
+[eva] offsetmap.i:90: Frama_C_show_each_1_256_257: {0; 257}
+[eva] computing for function Frama_C_interval <- h <- main.
+ Called from offsetmap.i:101.
+[eva] Done for function Frama_C_interval
+[eva] offsetmap.i:104: Frama_C_show_each_1_256_257: {0; 257}
+[eva] Recording results for h
+[eva] Done for function h
[eva] Recording results for main
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
@@ -63,8 +76,7 @@
i ∈ {9}
a[bits 0 to 7] ∈ {1; 6}
[bits 8 to 31]# ∈ {6}%32, bits 8 to 31
- b[bits 0 to 7] ∈ {0; 1}
- [bits 8 to 31]# ∈ {0; 6}%32, bits 8 to 31
+ b ∈ {0; 1}
a7[bits 0 to 7] ∈ {1}
[bits 8 to 31]# ∈ {97}%32, bits 8 to 31
b7 ∈ {1}
@@ -86,9 +98,18 @@
[eva:final-states] Values at end of function g:
s[0..9999999] ∈ {0; 16975879}
p_0 ∈ {{ &s + [0..39999996],0%4 }}
- c1# ∈ {0; 16975879}%32, bits 0 to 7
+ c1 ∈ {0; 7}
q ∈ {{ &s + [0..9999999] }}
- c2 ∈ {0; 1; 3; 7; 8}
+ c2 ∈ [0..8]
+[eva:final-states] Values at end of function h:
+ x ∈ [0..257]
+ i_0 ∈ [0..6]
+ p_0 ∈ {{ &t + {1} }}
+ q ∈ {{ NULL ; &x }}
+ t[0][bits 0 to 7]# ∈ {257}%16, bits 0 to 7
+ [bits 8 to 119]# ∈ {0; 257} repeated %16, bits 8 to 119
+ [7][bits 8 to 15]# ∈ {257}%16, bits 8 to 15
+ sp ∈ {{ &t + [1..13],1%2 }}
[eva:final-states] Values at end of function main:
TT[0][bits 0 to 7]# ∈ [0..8]%32, bits 0 to 7
[bits 8 to 39]# ∈ [0..8] repeated %32, bits 8 to 39
@@ -108,8 +129,7 @@
i ∈ {9}
a[bits 0 to 7] ∈ {1; 6}
[bits 8 to 31]# ∈ {6}%32, bits 8 to 31
- b[bits 0 to 7] ∈ {0; 1}
- [bits 8 to 31]# ∈ {0; 6}%32, bits 8 to 31
+ b ∈ {0; 1}
a7[bits 0 to 7] ∈ {1}
[bits 8 to 31]# ∈ {97}%32, bits 8 to 31
b7 ∈ {1}
@@ -133,10 +153,16 @@
[from] Done for function f
[from] Computing for function g
[from] Done for function g
+[from] Computing for function h
+[from] Computing for function Frama_C_interval <-h
+[from] Done for function Frama_C_interval
+[from] Done for function h
[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 Frama_C_interval:
+ \result FROM min; max
[from] Function f:
TT{[0..8]; [9][bits 0 to 7]} FROM \nothing (and SELF)
T{{[0][bits 8 to 31]; [1..5]}; {[7..8]; [9][bits 0 to 7]}}
@@ -155,6 +181,8 @@
a2 FROM \nothing
[from] Function g:
s[0..9999999] FROM i_0 (and SELF)
+[from] Function h:
+ NO EFFECTS
[from] Function main:
TT{[0..8]; [9][bits 0 to 7]} FROM \nothing (and SELF)
T{{[0][bits 8 to 31]; [1..5]}; {[7..8]; [9][bits 0 to 7]}}
@@ -183,6 +211,10 @@
s[0..9999999]; p_0; c1; q; c2
[inout] Inputs for function g:
s{[0..9999998]; [9999999][bits 0 to 7]}
+[inout] Out (internal) for function h:
+ x; i_0; p_0; q; t[0..7]; j; sp
+[inout] Inputs for function h:
+ \nothing
[inout] Out (internal) for function main:
TT{[0..8]; [9][bits 0 to 7]};
T{[0][bits 8 to 31]; [1..8]; [9][bits 0 to 7]}; i; a; b; a7; b7;
diff --git a/tests/value/oracle/offsetmap.2.res.oracle b/tests/value/oracle/offsetmap.2.res.oracle
new file mode 100644
index 00000000000..d39ab3e4cdf
--- /dev/null
+++ b/tests/value/oracle/offsetmap.2.res.oracle
@@ -0,0 +1,237 @@
+[kernel] Parsing offsetmap.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
+ TT[0] ∈ {1}
+ [1] ∈ {2}
+ [2] ∈ {3}
+ [3..9] ∈ {0}
+ T[0] ∈ {1}
+ [1] ∈ {2}
+ [2] ∈ {3}
+ [3..9] ∈ {0}
+ i ∈ {0}
+ a ∈ {0}
+ b ∈ {0}
+ a7 ∈ {0}
+ b7 ∈ {0}
+ O1[0..19] ∈ {0}
+ O2[0..19] ∈ {0}
+ p ∈ {0}
+ x2 ∈ {0}
+ b2 ∈ {0}
+ a2 ∈ {0}
+ s[0..9999999] ∈ {0}
+[eva] computing for function f <- main.
+ Called from offsetmap.i:108.
+[eva] offsetmap.i:19: starting to merge loop iterations
+[eva] offsetmap.i:29: starting to merge loop iterations
+[eva:alarm] offsetmap.i:51: Warning:
+ pointer downcast. assert (unsigned int)(&x2) ≤ 2147483647;
+[eva] Recording results for f
+[eva] Done for function f
+[eva] computing for function g <- main.
+ Called from offsetmap.i:109.
+[eva:alarm] offsetmap.i:66: Warning:
+ accessing out of bounds index. assert 0 ≤ i_0;
+[eva:alarm] offsetmap.i:66: Warning:
+ accessing out of bounds index. assert i_0 < 10000000;
+[eva] Recording results for g
+[kernel] offsetmap.i:68:
+ more than 200(10000000) elements to enumerate. Approximating.
+[eva] Done for function g
+[eva] computing for function h <- main.
+ Called from offsetmap.i:110.
+[eva] computing for function Frama_C_interval <- h <- main.
+ Called from offsetmap.i:87.
+[eva] using specification for function Frama_C_interval
+[eva] Done for function Frama_C_interval
+[eva] offsetmap.i:90: Frama_C_show_each_1_256_257: {0; 1; 256; 257}
+[eva:alarm] offsetmap.i:95: Warning:
+ pointer comparison. assert \pointer_comparable((void *)q, (void *)0);
+[eva:alarm] offsetmap.i:95: Warning: out of bounds write. assert \valid(q);
+[eva] computing for function Frama_C_interval <- h <- main.
+ Called from offsetmap.i:101.
+[eva] Done for function Frama_C_interval
+[eva] offsetmap.i:104: Frama_C_show_each_1_256_257: {0; 1; 256; 257}
+[eva] Recording results for h
+[eva] Done for function h
+[eva] Recording results for main
+[eva] Done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function f:
+ TT[0][bits 0 to 7]# ∈ [0..8]%32, bits 0 to 7
+ [bits 8 to 39]# ∈ [0..8] repeated %32, bits 8 to 39
+ [bits 40 to 71]# ∈ [0..8] repeated %32, bits 8 to 39
+ [bits 72 to 287]# ∈ [0..8] repeated %32, bits 8 to 223
+ [9] ∈ {0}
+ T[0][bits 0 to 7]# ∈ {1}%32, bits 0 to 7
+ [0][bits 8 to 31]# ∈ {0; 1}%32, bits 8 to 31
+ [1][bits 0 to 7]# ∈ {0; 2}%32, bits 0 to 7
+ [1][bits 8 to 31]# ∈ {0; 2}%32, bits 8 to 31
+ [2][bits 0 to 7]# ∈ {0; 3}%32, bits 0 to 7
+ [2][bits 8 to 31]# ∈ {0; 3}%32, bits 8 to 31
+ [3..5] ∈ {0}
+ [6][bits 0 to 7]# ∈ {0; 7}%32, bits 0 to 7
+ [6][bits 8 to 31]# ∈ {0; 7}%32, bits 8 to 31
+ [7..9] ∈ {0}
+ i ∈ {9}
+ a[bits 0 to 7] ∈ {1; 6}
+ [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
+ b[bits 0 to 7] ∈ {0; 1}
+ [bits 8 to 31]# ∈ {0; 6}%32, bits 8 to 31
+ a7[bits 0 to 7] ∈ {1}
+ [bits 8 to 31]# ∈ {97}%32, bits 8 to 31
+ b7 ∈ {1}
+ O1[0][bits 0 to 7] ∈ {0}
+ [0][bits 8 to 15] ∈ {18}
+ [0][bits 16 to 31] ∈ {0}
+ [1] ∈ {17}
+ [2..8] ∈ {0}
+ [9] ∈ {1}
+ [10..19] ∈ {0}
+ O2[0][bits 0 to 7]# ∈ {10}%32, bits 0 to 7
+ [0][bits 8 to 15] ∈ {11}
+ [0][bits 16 to 31]# ∈ {10}%32, bits 16 to 31
+ [1..19] ∈ {0}
+ p ∈ {{ &O1[9] }}
+ x2 ∈ {1}
+ b2 ∈ {{ &x2 }}
+ a2 ∈ {{ (int)&x2 }}
+[eva:final-states] Values at end of function g:
+ s[0..9999999] ∈ {0; 16975879}
+ p_0 ∈ {{ &s + [0..39999996],0%4 }}
+ c1# ∈ {0; 16975879}%32, bits 0 to 7
+ q ∈ {{ &s + [0..9999999] }}
+ c2 ∈ {0; 1; 3; 7; 8}
+[eva:final-states] Values at end of function h:
+ x[bits 0 to 7]# ∈ {0; 42; 257}%32, bits 0 to 7
+ [bits 8 to 15]# ∈ {0; 42; 257}%32, bits 8 to 15
+ [bits 16 to 23]# ∈ {0; 42; 257}%32, bits 16 to 23
+ [bits 24 to 31]# ∈ {0; 42; 257}%32, bits 24 to 31
+ i_0 ∈ {0; 1; 2; 3; 4; 5; 6}
+ p_0 ∈ {{ &t + {1} }}
+ q ∈ {{ NULL ; &x }}
+ t[0][bits 0 to 7]# ∈ {257}%16, bits 0 to 7
+ [bits 8 to 23]# ∈ {0; 257} repeated %16, bits 8 to 23
+ [bits 24 to 39]# ∈ {0; 257} repeated %16, bits 8 to 23
+ [bits 40 to 55]# ∈ {0; 257} repeated %16, bits 8 to 23
+ [bits 56 to 71]# ∈ {0; 257} repeated %16, bits 8 to 23
+ [bits 72 to 87]# ∈ {0; 257} repeated %16, bits 8 to 23
+ [bits 88 to 103]# ∈ {0; 257} repeated %16, bits 8 to 23
+ [bits 104 to 119]# ∈ {0; 257} repeated %16, bits 8 to 23
+ [7][bits 8 to 15]# ∈ {257}%16, bits 8 to 15
+ sp ∈ {{ &t + {1; 3; 5; 7; 9; 11; 13} }}
+[eva:final-states] Values at end of function main:
+ TT[0][bits 0 to 7]# ∈ [0..8]%32, bits 0 to 7
+ [bits 8 to 39]# ∈ [0..8] repeated %32, bits 8 to 39
+ [bits 40 to 71]# ∈ [0..8] repeated %32, bits 8 to 39
+ [bits 72 to 287]# ∈ [0..8] repeated %32, bits 8 to 223
+ [9] ∈ {0}
+ T[0][bits 0 to 7]# ∈ {1}%32, bits 0 to 7
+ [0][bits 8 to 31]# ∈ {0; 1}%32, bits 8 to 31
+ [1][bits 0 to 7]# ∈ {0; 2}%32, bits 0 to 7
+ [1][bits 8 to 31]# ∈ {0; 2}%32, bits 8 to 31
+ [2][bits 0 to 7]# ∈ {0; 3}%32, bits 0 to 7
+ [2][bits 8 to 31]# ∈ {0; 3}%32, bits 8 to 31
+ [3..5] ∈ {0}
+ [6][bits 0 to 7]# ∈ {0; 7}%32, bits 0 to 7
+ [6][bits 8 to 31]# ∈ {0; 7}%32, bits 8 to 31
+ [7..9] ∈ {0}
+ i ∈ {9}
+ a[bits 0 to 7] ∈ {1; 6}
+ [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
+ b[bits 0 to 7] ∈ {0; 1}
+ [bits 8 to 31]# ∈ {0; 6}%32, bits 8 to 31
+ a7[bits 0 to 7] ∈ {1}
+ [bits 8 to 31]# ∈ {97}%32, bits 8 to 31
+ b7 ∈ {1}
+ O1[0][bits 0 to 7] ∈ {0}
+ [0][bits 8 to 15] ∈ {18}
+ [0][bits 16 to 31] ∈ {0}
+ [1] ∈ {17}
+ [2..8] ∈ {0}
+ [9] ∈ {1}
+ [10..19] ∈ {0}
+ O2[0][bits 0 to 7]# ∈ {10}%32, bits 0 to 7
+ [0][bits 8 to 15] ∈ {11}
+ [0][bits 16 to 31]# ∈ {10}%32, bits 16 to 31
+ [1..19] ∈ {0}
+ p ∈ {{ &O1[9] }}
+ x2 ∈ {1}
+ b2 ∈ {{ &x2 }}
+ a2 ∈ {{ (int)&x2 }}
+ s[0..9999999] ∈ {0; 16975879}
+[from] Computing for function f
+[from] Done for function f
+[from] Computing for function g
+[from] Done for function g
+[from] Computing for function h
+[from] Computing for function Frama_C_interval <-h
+[from] Done for function Frama_C_interval
+[from] Done for function h
+[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 Frama_C_interval:
+ \result FROM min; max
+[from] Function f:
+ TT{[0..8]; [9][bits 0 to 7]} FROM \nothing (and SELF)
+ T{{[0][bits 8 to 31]; [1..5]}; {[7..8]; [9][bits 0 to 7]}}
+ FROM \nothing (and SELF)
+ [6] FROM b
+ i FROM \nothing
+ a FROM b
+ b FROM b (and SELF)
+ a7 FROM \nothing
+ b7 FROM \nothing
+ O1{[0][bits 8 to 15]; [1]; [6]; [9]} FROM \nothing
+ O2[0] FROM \nothing
+ p FROM \nothing
+ x2 FROM \nothing
+ b2 FROM \nothing
+ a2 FROM \nothing
+[from] Function g:
+ s[0..9999999] FROM i_0 (and SELF)
+[from] Function h:
+ NO EFFECTS
+[from] Function main:
+ TT{[0..8]; [9][bits 0 to 7]} FROM \nothing (and SELF)
+ T{{[0][bits 8 to 31]; [1..5]}; {[7..8]; [9][bits 0 to 7]}}
+ FROM \nothing (and SELF)
+ [6] FROM b
+ i FROM \nothing
+ a FROM b
+ b FROM b (and SELF)
+ a7 FROM \nothing
+ b7 FROM \nothing
+ O1{[0][bits 8 to 15]; [1]; [6]; [9]} FROM \nothing
+ O2[0] FROM \nothing
+ p FROM \nothing
+ x2 FROM \nothing
+ b2 FROM \nothing
+ a2 FROM \nothing
+ s[0..9999999] FROM i_0 (and SELF)
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function f:
+ TT{[0..8]; [9][bits 0 to 7]};
+ T{[0][bits 8 to 31]; [1..8]; [9][bits 0 to 7]}; i; a; b; a7; b7;
+ O1{[0][bits 8 to 15]; [1]; [6]; [9]}; O2[0]; p; x2; b2; a2
+[inout] Inputs for function f:
+ i; a; b; a7; p; x2; b2; a2
+[inout] Out (internal) for function g:
+ s[0..9999999]; p_0; c1; q; c2
+[inout] Inputs for function g:
+ s{[0..9999998]; [9999999][bits 0 to 7]}
+[inout] Out (internal) for function h:
+ x; i_0; p_0; q; t[0..7]; j; sp
+[inout] Inputs for function h:
+ \nothing
+[inout] Out (internal) for function main:
+ TT{[0..8]; [9][bits 0 to 7]};
+ T{[0][bits 8 to 31]; [1..8]; [9][bits 0 to 7]}; i; a; b; a7; b7;
+ O1{[0][bits 8 to 15]; [1]; [6]; [9]}; O2[0]; p; x2; b2; a2; s[0..9999999]
+[inout] Inputs for function main:
+ i; a; b; a7; p; x2; b2; a2; s{[0..9999998]; [9999999][bits 0 to 7]}
diff --git a/tests/value/oracle_apron/offsetmap.0.res.oracle b/tests/value/oracle_apron/offsetmap.0.res.oracle
index b718988fd80..de3bcc8259f 100644
--- a/tests/value/oracle_apron/offsetmap.0.res.oracle
+++ b/tests/value/oracle_apron/offsetmap.0.res.oracle
@@ -1,19 +1,19 @@
-64,65c64
+80,81c80
< a[bits 0 to 7] ∈ {1; 6}
< [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
---
> a ∈ {1; 6}
-67,68c66
+83,84c82
< a7[bits 0 to 7] ∈ {1}
< [bits 8 to 31]# ∈ {97}%32, bits 8 to 31
---
> a7 ∈ {1}
-108,109c106
+142,143c140
< a[bits 0 to 7] ∈ {1; 6}
< [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
---
> a ∈ {1; 6}
-111,112c108
+145,146c142
< a7[bits 0 to 7] ∈ {1}
< [bits 8 to 31]# ∈ {97}%32, bits 8 to 31
---
diff --git a/tests/value/oracle_apron/offsetmap.1.res.oracle b/tests/value/oracle_apron/offsetmap.1.res.oracle
index 0ee129ee029..5c1fbd1e023 100644
--- a/tests/value/oracle_apron/offsetmap.1.res.oracle
+++ b/tests/value/oracle_apron/offsetmap.1.res.oracle
@@ -1,22 +1,20 @@
-64,69c64,66
+77,78c77
< a[bits 0 to 7] ∈ {1; 6}
< [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
-< b[bits 0 to 7] ∈ {0; 1}
-< [bits 8 to 31]# ∈ {0; 6}%32, bits 8 to 31
+---
+> a ∈ {1; 6}
+80,81c79
< a7[bits 0 to 7] ∈ {1}
< [bits 8 to 31]# ∈ {97}%32, bits 8 to 31
---
-> a ∈ {1; 6}
-> b ∈ {0; 1}
> a7 ∈ {1}
-109,114c106,108
+130,131c128
< a[bits 0 to 7] ∈ {1; 6}
< [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
-< b[bits 0 to 7] ∈ {0; 1}
-< [bits 8 to 31]# ∈ {0; 6}%32, bits 8 to 31
+---
+> a ∈ {1; 6}
+133,134c130
< a7[bits 0 to 7] ∈ {1}
< [bits 8 to 31]# ∈ {97}%32, bits 8 to 31
---
-> a ∈ {1; 6}
-> b ∈ {0; 1}
> a7 ∈ {1}
diff --git a/tests/value/oracle_apron/offsetmap.2.res.oracle b/tests/value/oracle_apron/offsetmap.2.res.oracle
new file mode 100644
index 00000000000..52b123a5270
--- /dev/null
+++ b/tests/value/oracle_apron/offsetmap.2.res.oracle
@@ -0,0 +1,22 @@
+80,85c80,82
+< a[bits 0 to 7] ∈ {1; 6}
+< [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
+< b[bits 0 to 7] ∈ {0; 1}
+< [bits 8 to 31]# ∈ {0; 6}%32, bits 8 to 31
+< a7[bits 0 to 7] ∈ {1}
+< [bits 8 to 31]# ∈ {97}%32, bits 8 to 31
+---
+> a ∈ {1; 6}
+> b ∈ {0; 1}
+> a7 ∈ {1}
+143,148c140,142
+< a[bits 0 to 7] ∈ {1; 6}
+< [bits 8 to 31]# ∈ {6}%32, bits 8 to 31
+< b[bits 0 to 7] ∈ {0; 1}
+< [bits 8 to 31]# ∈ {0; 6}%32, bits 8 to 31
+< a7[bits 0 to 7] ∈ {1}
+< [bits 8 to 31]# ∈ {97}%32, bits 8 to 31
+---
+> a ∈ {1; 6}
+> b ∈ {0; 1}
+> a7 ∈ {1}
diff --git a/tests/value/oracle_equality/offsetmap.2.res.oracle b/tests/value/oracle_equality/offsetmap.2.res.oracle
new file mode 100644
index 00000000000..6bebb89e738
--- /dev/null
+++ b/tests/value/oracle_equality/offsetmap.2.res.oracle
@@ -0,0 +1,4 @@
+40d39
+< [eva] Recording results for g
+42a42
+> [eva] Recording results for g
diff --git a/tests/value/oracle_octagon/offsetmap.2.res.oracle b/tests/value/oracle_octagon/offsetmap.2.res.oracle
new file mode 100644
index 00000000000..6bebb89e738
--- /dev/null
+++ b/tests/value/oracle_octagon/offsetmap.2.res.oracle
@@ -0,0 +1,4 @@
+40d39
+< [eva] Recording results for g
+42a42
+> [eva] Recording results for g
diff --git a/tests/value/oracle_symblocs/offsetmap.2.res.oracle b/tests/value/oracle_symblocs/offsetmap.2.res.oracle
new file mode 100644
index 00000000000..6bebb89e738
--- /dev/null
+++ b/tests/value/oracle_symblocs/offsetmap.2.res.oracle
@@ -0,0 +1,4 @@
+40d39
+< [eva] Recording results for g
+42a42
+> [eva] Recording results for g
--
GitLab