diff --git a/src/plugins/value/engine/subdivided_evaluation.ml b/src/plugins/value/engine/subdivided_evaluation.ml
index 42e1eec994ff1e24401c645959e19246e03eec3c..f8cd150852485631688939f48782d496a9463ce4 100644
--- a/src/plugins/value/engine/subdivided_evaluation.ml
+++ b/src/plugins/value/engine/subdivided_evaluation.ml
@@ -231,7 +231,9 @@ let compare_bound ival_compare_bound v1 v2 =
let f1 = Cvalue.V.project_ival v1 in
let f2 = Cvalue.V.project_ival v2 in
ival_compare_bound f1 f2
- with Cvalue.V.Not_based_on_null -> assert false
+ (* Cannot compare pointers. This case can however happens on subdivisions
+ of a pointer subexpression to reduce a bigger numeric expression. *)
+ with Cvalue.V.Not_based_on_null -> 0
let has_greater_min_bound = compare_bound Ival.has_greater_min_bound
let has_smaller_max_bound = compare_bound Ival.has_smaller_max_bound
diff --git a/tests/value/nonlin.c b/tests/value/nonlin.c
index 1a05ef68d3147308ca183a5a8b6a18b65e876d76..2fe0f90f17a8ee5072ccd76445e60dfa44ad7708 100644
--- a/tests/value/nonlin.c
+++ b/tests/value/nonlin.c
@@ -16,9 +16,15 @@ void subdivide_pointer () {
int *q = p + i - i;
/* The complete expression is a singleton: no subdivision. */
y = *(&y + i - i);
- /* The complete expression is an imprecise integer: subdivision (but not
+ /* The complete expression is an imprecise integer: subdivision (but no
reduction, as it cannot improve the bounds of the result). */
y = *(p + i - i);
+ /* The subexpression contains a pointer, but the complete expression is an
+ integer, and the subdivision can reduce its value. */
+ int t[10] = {0, 1, 2, 4, 5, 6, 7, 8, 9};
+ p = &t[0];
+ i = Frama_C_interval(0, 10);
+ y = *(p + i - i);
/* The splitted lvalue contains a pointer value: no subdivision. */
i = v ? i : (int) &x;
y = *(p + i - i);
diff --git a/tests/value/oracle/nonlin.res.oracle b/tests/value/oracle/nonlin.res.oracle
index 433ce49eaa0ba5fe807e8a83e3c7550bb2c62d67..5e56b1da308cf04d6375e24a853686f31a88fb09 100644
--- a/tests/value/oracle/nonlin.res.oracle
+++ b/tests/value/oracle/nonlin.res.oracle
@@ -24,28 +24,28 @@
[31] ∈ {5}
[32..35] ∈ {0}
[eva] computing for function subdivide_integer <- main.
- Called from tests/value/nonlin.c:119.
-[eva:nonlin] tests/value/nonlin.c:31:
+ Called from tests/value/nonlin.c:125.
+[eva:nonlin] tests/value/nonlin.c:37:
non-linear '((int)z + 675) * ((int)z + 675)', lv 'z'
-[eva:nonlin] tests/value/nonlin.c:31: subdividing on z
-[eva:nonlin] tests/value/nonlin.c:32:
+[eva:nonlin] tests/value/nonlin.c:37: subdividing on z
+[eva:nonlin] tests/value/nonlin.c:38:
non-linear '((int)z + 17817) * ((int)z + 17817)', lv 'z'
-[eva:nonlin] tests/value/nonlin.c:32: subdividing on z
-[eva:alarm] tests/value/nonlin.c:32: Warning:
+[eva:nonlin] tests/value/nonlin.c:38: subdividing on z
+[eva:alarm] tests/value/nonlin.c:38: Warning:
signed overflow.
assert (int)((int)z + 17817) * (int)((int)z + 17817) ≤ 2147483647;
-[eva:nonlin] tests/value/nonlin.c:39:
+[eva:nonlin] tests/value/nonlin.c:45:
non-linear '(i2 + (long long)3) * (i2 + (long long)3)', lv 'i2'
-[eva:nonlin] tests/value/nonlin.c:39: non-linear 'i1 * i1', lv 'i1'
-[eva:nonlin] tests/value/nonlin.c:39: subdividing on i2
-[eva:nonlin] tests/value/nonlin.c:39: subdividing on i1
-[eva:alarm] tests/value/nonlin.c:43: Warning: assertion got status unknown.
-[eva:nonlin] tests/value/nonlin.c:44: non-linear '(int)idx * (int)idx', lv 'idx'
-[eva:nonlin] tests/value/nonlin.c:44: subdividing on idx
+[eva:nonlin] tests/value/nonlin.c:45: non-linear 'i1 * i1', lv 'i1'
+[eva:nonlin] tests/value/nonlin.c:45: subdividing on i2
+[eva:nonlin] tests/value/nonlin.c:45: subdividing on i1
+[eva:alarm] tests/value/nonlin.c:49: Warning: assertion got status unknown.
+[eva:nonlin] tests/value/nonlin.c:50: non-linear '(int)idx * (int)idx', lv 'idx'
+[eva:nonlin] tests/value/nonlin.c:50: subdividing on idx
[eva] Recording results for subdivide_integer
[eva] Done for function subdivide_integer
[eva] computing for function subdivide_pointer <- main.
- Called from tests/value/nonlin.c:120.
+ Called from tests/value/nonlin.c:126.
[eva] computing for function Frama_C_interval <- subdivide_pointer <- main.
Called from tests/value/nonlin.c:12.
[eva] using specification for function Frama_C_interval
@@ -63,97 +63,103 @@
[eva:nonlin] tests/value/nonlin.c:21: subdividing on i
[eva:alarm] tests/value/nonlin.c:21: Warning:
out of bounds read. assert \valid_read((p + i) - i);
-[eva:alarm] tests/value/nonlin.c:23: Warning:
+[eva] computing for function Frama_C_interval <- subdivide_pointer <- main.
+ Called from tests/value/nonlin.c:26.
+[eva] tests/value/nonlin.c:26:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva:nonlin] tests/value/nonlin.c:27: subdividing on i
+[eva:alarm] tests/value/nonlin.c:29: Warning:
pointer downcast. assert (unsigned int)(&x) ≤ 2147483647;
-[eva:alarm] tests/value/nonlin.c:24: Warning:
+[eva:alarm] tests/value/nonlin.c:30: Warning:
out of bounds read. assert \valid_read((p + i) - i);
[eva] Recording results for subdivide_pointer
[eva] Done for function subdivide_pointer
[eva] computing for function subdivide_several_variables <- main.
- Called from tests/value/nonlin.c:121.
+ Called from tests/value/nonlin.c:127.
[eva] computing for function Frama_C_interval <- subdivide_several_variables <-
main.
- Called from tests/value/nonlin.c:51.
-[eva] tests/value/nonlin.c:51:
+ Called from tests/value/nonlin.c:57.
+[eva] tests/value/nonlin.c:57:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- subdivide_several_variables <-
main.
- Called from tests/value/nonlin.c:52.
-[eva] tests/value/nonlin.c:52:
+ Called from tests/value/nonlin.c:58.
+[eva] tests/value/nonlin.c:58:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- subdivide_several_variables <-
main.
- Called from tests/value/nonlin.c:53.
-[eva] tests/value/nonlin.c:53:
+ Called from tests/value/nonlin.c:59.
+[eva] tests/value/nonlin.c:59:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- subdivide_several_variables <-
main.
- Called from tests/value/nonlin.c:54.
-[eva] tests/value/nonlin.c:54:
+ Called from tests/value/nonlin.c:60.
+[eva] tests/value/nonlin.c:60:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
-[eva:nonlin] tests/value/nonlin.c:56: non-linear 'x * x', lv 'x'
-[eva:nonlin] tests/value/nonlin.c:56: non-linear 'y * y', lv 'y'
-[eva:nonlin] tests/value/nonlin.c:56: subdividing on x
-[eva:nonlin] tests/value/nonlin.c:56: subdividing on y
-[eva:nonlin] tests/value/nonlin.c:60: non-linear 'x * x', lv 'x'
-[eva:nonlin] tests/value/nonlin.c:60: non-linear '((x * x) * y) * y', lv 'y'
-[eva:nonlin] tests/value/nonlin.c:60: subdividing on x
-[eva:nonlin] tests/value/nonlin.c:60: subdividing on y
-[eva:nonlin] tests/value/nonlin.c:62: non-linear 'x * y - y * x', lv 'y, x'
-[eva:nonlin] tests/value/nonlin.c:62: subdividing on x, y
-[eva:nonlin] tests/value/nonlin.c:65:
+[eva:nonlin] tests/value/nonlin.c:62: non-linear 'x * x', lv 'x'
+[eva:nonlin] tests/value/nonlin.c:62: non-linear 'y * y', lv 'y'
+[eva:nonlin] tests/value/nonlin.c:62: subdividing on x
+[eva:nonlin] tests/value/nonlin.c:62: subdividing on y
+[eva:nonlin] tests/value/nonlin.c:66: non-linear 'x * x', lv 'x'
+[eva:nonlin] tests/value/nonlin.c:66: non-linear '((x * x) * y) * y', lv 'y'
+[eva:nonlin] tests/value/nonlin.c:66: subdividing on x
+[eva:nonlin] tests/value/nonlin.c:66: subdividing on y
+[eva:nonlin] tests/value/nonlin.c:68: non-linear 'x * y - y * x', lv 'y, x'
+[eva:nonlin] tests/value/nonlin.c:68: subdividing on x, y
+[eva:nonlin] tests/value/nonlin.c:71:
non-linear '(x * x - (2 * x) * y) + y * y', lv 'y, x'
-[eva:nonlin] tests/value/nonlin.c:65: subdividing on x, y
-[eva:nonlin] tests/value/nonlin.c:66:
+[eva:nonlin] tests/value/nonlin.c:71: subdividing on x, y
+[eva:nonlin] tests/value/nonlin.c:72:
non-linear '(x * x + y * y) - (2 * x) * y', lv 'y, x'
-[eva:nonlin] tests/value/nonlin.c:66: subdividing on x, y
-[eva:nonlin] tests/value/nonlin.c:68:
+[eva:nonlin] tests/value/nonlin.c:72: subdividing on x, y
+[eva:nonlin] tests/value/nonlin.c:74:
non-linear '(z * x + x * y) + y * z', lv 'z, y, x'
-[eva:nonlin] tests/value/nonlin.c:68: non-linear 'w * w', lv 'w'
-[eva:nonlin] tests/value/nonlin.c:68: subdividing on x, y, z
-[eva:nonlin] tests/value/nonlin.c:68: subdividing on w
+[eva:nonlin] tests/value/nonlin.c:74: non-linear 'w * w', lv 'w'
+[eva:nonlin] tests/value/nonlin.c:74: subdividing on x, y, z
+[eva:nonlin] tests/value/nonlin.c:74: subdividing on w
[eva] Recording results for subdivide_several_variables
[eva] Done for function subdivide_several_variables
[eva] computing for function subdivide_table <- main.
- Called from tests/value/nonlin.c:122.
-[eva] tests/value/nonlin.c:87: loop invariant got status valid.
-[eva] tests/value/nonlin.c:88: starting to merge loop iterations
-[eva:nonlin] tests/value/nonlin.c:89:
+ Called from tests/value/nonlin.c:128.
+[eva] tests/value/nonlin.c:93: loop invariant got status valid.
+[eva] tests/value/nonlin.c:94: starting to merge loop iterations
+[eva:nonlin] tests/value/nonlin.c:95:
non-linear '(4 + ((x >> 2) * 3 << 2)) + x % 4', lv 'x'
-[eva:nonlin] tests/value/nonlin.c:89: subdividing on x
+[eva:nonlin] tests/value/nonlin.c:95: subdividing on x
[eva] Recording results for subdivide_table
[eva] Done for function subdivide_table
[eva] computing for function subdivide_reduced_value <- main.
- Called from tests/value/nonlin.c:123.
-[eva:nonlin] tests/value/nonlin.c:101: non-linear 't1[i] - t2[i]', lv 'i'
-[eva:nonlin] tests/value/nonlin.c:101: subdividing on i
-[eva:alarm] tests/value/nonlin.c:101: Warning:
+ Called from tests/value/nonlin.c:129.
+[eva:nonlin] tests/value/nonlin.c:107: non-linear 't1[i] - t2[i]', lv 'i'
+[eva:nonlin] tests/value/nonlin.c:107: subdividing on i
+[eva:alarm] tests/value/nonlin.c:107: Warning:
accessing out of bounds index. assert 0 ≤ i;
-[eva:alarm] tests/value/nonlin.c:101: Warning:
+[eva:alarm] tests/value/nonlin.c:107: Warning:
accessing out of bounds index. assert i < 2;
[eva] Recording results for subdivide_reduced_value
[eva] Done for function subdivide_reduced_value
[eva] computing for function local_subdivide <- main.
- Called from tests/value/nonlin.c:124.
+ Called from tests/value/nonlin.c:130.
[eva] computing for function Frama_C_interval <- local_subdivide <- main.
- Called from tests/value/nonlin.c:107.
-[eva] tests/value/nonlin.c:107:
+ Called from tests/value/nonlin.c:113.
+[eva] tests/value/nonlin.c:113:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- local_subdivide <- main.
- Called from tests/value/nonlin.c:108.
-[eva] tests/value/nonlin.c:108:
+ Called from tests/value/nonlin.c:114.
+[eva] tests/value/nonlin.c:114:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
-[eva:nonlin] tests/value/nonlin.c:112:
+[eva:nonlin] tests/value/nonlin.c:118:
non-linear '(x * x - (2 * x) * y) + y * y', lv 'y, x'
-[eva:nonlin] tests/value/nonlin.c:112: subdividing on x, y
-[eva:nonlin] tests/value/nonlin.c:113: subdividing on x, y
-[eva:nonlin] tests/value/nonlin.c:115: subdividing on x, y
+[eva:nonlin] tests/value/nonlin.c:118: subdividing on x, y
+[eva:nonlin] tests/value/nonlin.c:119: subdividing on x, y
+[eva:nonlin] tests/value/nonlin.c:121: subdividing on x, y
[eva] Recording results for local_subdivide
[eva] Done for function local_subdivide
[eva] Recording results for main
@@ -181,11 +187,21 @@
idx ∈ [0..10]
[eva:final-states] Values at end of function subdivide_pointer:
Frama_C_entropy_source ∈ [--..--]
- y ∈ [-10..10]
+ y ∈ [--..--]
x ∈ [-10..10]
- p ∈ {{ &x }}
- i ∈ {{ NULL + [0..100] ; (int)&x }}
+ p ∈ {{ &t[0] }}
+ i ∈ {{ NULL + [0..10] ; (int)&x }}
q ∈ {{ &x + [-400..400],0%4 }}
+ t[0] ∈ {0}
+ [1] ∈ {1}
+ [2] ∈ {2}
+ [3] ∈ {4}
+ [4] ∈ {5}
+ [5] ∈ {6}
+ [6] ∈ {7}
+ [7] ∈ {8}
+ [8] ∈ {9}
+ [9] ∈ {0}
[eva:final-states] Values at end of function subdivide_reduced_value:
t1[0] ∈ {0}
[1] ∈ {1}
@@ -256,7 +272,7 @@
[inout] Inputs for function subdivide_integer:
v; vs
[inout] Out (internal) for function subdivide_pointer:
- Frama_C_entropy_source; y; x; p; i; q
+ Frama_C_entropy_source; y; x; p; i; q; t[0..9]
[inout] Inputs for function subdivide_pointer:
Frama_C_entropy_source; v
[inout] Out (internal) for function subdivide_reduced_value: