Skip to content
Snippets Groups Projects
Commit 5da3ed83 authored by David Bühler's avatar David Bühler
Browse files

[Eva] Adds a test of the subdivision of evaluation on a pointer subexpression.

parent 0df0c707
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
tests/value/nonlin.c
+ 7
− 1
View file @ 5da3ed83
...@@ -16,9 +16,15 @@ void subdivide_pointer () { ...@@ -16,9 +16,15 @@ void subdivide_pointer () {
int *q = p + i - i; int *q = p + i - i;
/* The complete expression is a singleton: no subdivision. */ /* The complete expression is a singleton: no subdivision. */
y = *(&y + i - i); 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). */ reduction, as it cannot improve the bounds of the result). */
y = *(p + i - i); 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. */ /* The splitted lvalue contains a pointer value: no subdivision. */
i = v ? i : (int) &x; i = v ? i : (int) &x;
y = *(p + i - i); y = *(p + i - i);
......
tests/value/oracle/nonlin.res.oracle
+ 82
− 66
View file @ 5da3ed83
...@@ -24,28 +24,28 @@ ...@@ -24,28 +24,28 @@
[31] ∈ {5} [31] ∈ {5}
[32..35] ∈ {0} [32..35] ∈ {0}
[eva] computing for function subdivide_integer <- main. [eva] computing for function subdivide_integer <- main.
Called from tests/value/nonlin.c:119. Called from tests/value/nonlin.c:125.
[eva:nonlin] tests/value/nonlin.c:31: [eva:nonlin] tests/value/nonlin.c:37:
non-linear '((int)z + 675) * ((int)z + 675)', lv 'z' 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:37: subdividing on z
[eva:nonlin] tests/value/nonlin.c:32: [eva:nonlin] tests/value/nonlin.c:38:
non-linear '((int)z + 17817) * ((int)z + 17817)', lv 'z' non-linear '((int)z + 17817) * ((int)z + 17817)', lv 'z'
[eva:nonlin] tests/value/nonlin.c:32: subdividing on z [eva:nonlin] tests/value/nonlin.c:38: subdividing on z
[eva:alarm] tests/value/nonlin.c:32: Warning: [eva:alarm] tests/value/nonlin.c:38: Warning:
signed overflow. signed overflow.
assert (int)((int)z + 17817) * (int)((int)z + 17817) ≤ 2147483647; 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' 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:45: non-linear 'i1 * i1', lv 'i1'
[eva:nonlin] tests/value/nonlin.c:39: subdividing on i2 [eva:nonlin] tests/value/nonlin.c:45: subdividing on i2
[eva:nonlin] tests/value/nonlin.c:39: subdividing on i1 [eva:nonlin] tests/value/nonlin.c:45: subdividing on i1
[eva:alarm] tests/value/nonlin.c:43: Warning: assertion got status unknown. [eva:alarm] tests/value/nonlin.c:49: 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:50: non-linear '(int)idx * (int)idx', lv 'idx'
[eva:nonlin] tests/value/nonlin.c:44: subdividing on idx [eva:nonlin] tests/value/nonlin.c:50: subdividing on idx
[eva] Recording results for subdivide_integer [eva] Recording results for subdivide_integer
[eva] Done for function subdivide_integer [eva] Done for function subdivide_integer
[eva] computing for function subdivide_pointer <- main. [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. [eva] computing for function Frama_C_interval <- subdivide_pointer <- main.
Called from tests/value/nonlin.c:12. Called from tests/value/nonlin.c:12.
[eva] using specification for function Frama_C_interval [eva] using specification for function Frama_C_interval
...@@ -63,97 +63,103 @@ ...@@ -63,97 +63,103 @@
[eva:nonlin] tests/value/nonlin.c:21: subdividing on i [eva:nonlin] tests/value/nonlin.c:21: subdividing on i
[eva:alarm] tests/value/nonlin.c:21: Warning: [eva:alarm] tests/value/nonlin.c:21: Warning:
out of bounds read. assert \valid_read((p + i) - i); 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; 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); out of bounds read. assert \valid_read((p + i) - i);
[eva] Recording results for subdivide_pointer [eva] Recording results for subdivide_pointer
[eva] Done for function subdivide_pointer [eva] Done for function subdivide_pointer
[eva] computing for function subdivide_several_variables <- main. [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 <- [eva] computing for function Frama_C_interval <- subdivide_several_variables <-
main. main.
Called from tests/value/nonlin.c:51. Called from tests/value/nonlin.c:57.
[eva] tests/value/nonlin.c:51: [eva] tests/value/nonlin.c:57:
function Frama_C_interval: precondition 'order' got status valid. function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval [eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- subdivide_several_variables <- [eva] computing for function Frama_C_interval <- subdivide_several_variables <-
main. main.
Called from tests/value/nonlin.c:52. Called from tests/value/nonlin.c:58.
[eva] tests/value/nonlin.c:52: [eva] tests/value/nonlin.c:58:
function Frama_C_interval: precondition 'order' got status valid. function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval [eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- subdivide_several_variables <- [eva] computing for function Frama_C_interval <- subdivide_several_variables <-
main. main.
Called from tests/value/nonlin.c:53. Called from tests/value/nonlin.c:59.
[eva] tests/value/nonlin.c:53: [eva] tests/value/nonlin.c:59:
function Frama_C_interval: precondition 'order' got status valid. function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval [eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- subdivide_several_variables <- [eva] computing for function Frama_C_interval <- subdivide_several_variables <-
main. main.
Called from tests/value/nonlin.c:54. Called from tests/value/nonlin.c:60.
[eva] tests/value/nonlin.c:54: [eva] tests/value/nonlin.c:60:
function Frama_C_interval: precondition 'order' got status valid. function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval [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:62: 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:62: non-linear 'y * y', lv 'y'
[eva:nonlin] tests/value/nonlin.c:56: subdividing on x [eva:nonlin] tests/value/nonlin.c:62: subdividing on x
[eva:nonlin] tests/value/nonlin.c:56: subdividing on y [eva:nonlin] tests/value/nonlin.c:62: subdividing on y
[eva:nonlin] tests/value/nonlin.c:60: non-linear 'x * x', lv 'x' [eva:nonlin] tests/value/nonlin.c:66: 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:66: non-linear '((x * x) * y) * y', lv 'y'
[eva:nonlin] tests/value/nonlin.c:60: subdividing on x [eva:nonlin] tests/value/nonlin.c:66: subdividing on x
[eva:nonlin] tests/value/nonlin.c:60: subdividing on y [eva:nonlin] tests/value/nonlin.c:66: 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:68: 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:68: subdividing on x, y
[eva:nonlin] tests/value/nonlin.c:65: [eva:nonlin] tests/value/nonlin.c:71:
non-linear '(x * x - (2 * x) * y) + y * y', lv 'y, x' 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:71: subdividing on x, y
[eva:nonlin] tests/value/nonlin.c:66: [eva:nonlin] tests/value/nonlin.c:72:
non-linear '(x * x + y * y) - (2 * x) * y', lv 'y, x' 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:72: subdividing on x, y
[eva:nonlin] tests/value/nonlin.c:68: [eva:nonlin] tests/value/nonlin.c:74:
non-linear '(z * x + x * y) + y * z', lv 'z, y, x' 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:74: non-linear 'w * w', lv 'w'
[eva:nonlin] tests/value/nonlin.c:68: subdividing on x, y, z [eva:nonlin] tests/value/nonlin.c:74: subdividing on x, y, z
[eva:nonlin] tests/value/nonlin.c:68: subdividing on w [eva:nonlin] tests/value/nonlin.c:74: subdividing on w
[eva] Recording results for subdivide_several_variables [eva] Recording results for subdivide_several_variables
[eva] Done for function subdivide_several_variables [eva] Done for function subdivide_several_variables
[eva] computing for function subdivide_table <- main. [eva] computing for function subdivide_table <- main.
Called from tests/value/nonlin.c:122. Called from tests/value/nonlin.c:128.
[eva] tests/value/nonlin.c:87: loop invariant got status valid. [eva] tests/value/nonlin.c:93: loop invariant got status valid.
[eva] tests/value/nonlin.c:88: starting to merge loop iterations [eva] tests/value/nonlin.c:94: starting to merge loop iterations
[eva:nonlin] tests/value/nonlin.c:89: [eva:nonlin] tests/value/nonlin.c:95:
non-linear '(4 + ((x >> 2) * 3 << 2)) + x % 4', lv 'x' 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] Recording results for subdivide_table
[eva] Done for function subdivide_table [eva] Done for function subdivide_table
[eva] computing for function subdivide_reduced_value <- main. [eva] computing for function subdivide_reduced_value <- main.
Called from tests/value/nonlin.c:123. Called from tests/value/nonlin.c:129.
[eva:nonlin] tests/value/nonlin.c:101: non-linear 't1[i] - t2[i]', lv 'i' [eva:nonlin] tests/value/nonlin.c:107: non-linear 't1[i] - t2[i]', lv 'i'
[eva:nonlin] tests/value/nonlin.c:101: subdividing on i [eva:nonlin] tests/value/nonlin.c:107: subdividing on i
[eva:alarm] tests/value/nonlin.c:101: Warning: [eva:alarm] tests/value/nonlin.c:107: Warning:
accessing out of bounds index. assert 0 ≤ i; 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; accessing out of bounds index. assert i < 2;
[eva] Recording results for subdivide_reduced_value [eva] Recording results for subdivide_reduced_value
[eva] Done for function subdivide_reduced_value [eva] Done for function subdivide_reduced_value
[eva] computing for function local_subdivide <- main. [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. [eva] computing for function Frama_C_interval <- local_subdivide <- main.
Called from tests/value/nonlin.c:107. Called from tests/value/nonlin.c:113.
[eva] tests/value/nonlin.c:107: [eva] tests/value/nonlin.c:113:
function Frama_C_interval: precondition 'order' got status valid. function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval [eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- local_subdivide <- main. [eva] computing for function Frama_C_interval <- local_subdivide <- main.
Called from tests/value/nonlin.c:108. Called from tests/value/nonlin.c:114.
[eva] tests/value/nonlin.c:108: [eva] tests/value/nonlin.c:114:
function Frama_C_interval: precondition 'order' got status valid. function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval [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' 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:118: subdividing on x, y
[eva:nonlin] tests/value/nonlin.c:113: subdividing on x, y [eva:nonlin] tests/value/nonlin.c:119: subdividing on x, y
[eva:nonlin] tests/value/nonlin.c:115: subdividing on x, y [eva:nonlin] tests/value/nonlin.c:121: subdividing on x, y
[eva] Recording results for local_subdivide [eva] Recording results for local_subdivide
[eva] Done for function local_subdivide [eva] Done for function local_subdivide
[eva] Recording results for main [eva] Recording results for main
...@@ -181,11 +187,21 @@ ...@@ -181,11 +187,21 @@
idx ∈ [0..10] idx ∈ [0..10]
[eva:final-states] Values at end of function subdivide_pointer: [eva:final-states] Values at end of function subdivide_pointer:
Frama_C_entropy_source ∈ [--..--] Frama_C_entropy_source ∈ [--..--]
y ∈ [-10..10] y ∈ [--..--]
x ∈ [-10..10] x ∈ [-10..10]
p ∈ {{ &x }} p ∈ {{ &t[0] }}
i ∈ {{ NULL + [0..100] ; (int)&x }} i ∈ {{ NULL + [0..10] ; (int)&x }}
q ∈ {{ &x + [-400..400],0%4 }} 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: [eva:final-states] Values at end of function subdivide_reduced_value:
t1[0] ∈ {0} t1[0] ∈ {0}
[1] ∈ {1} [1] ∈ {1}
...@@ -256,7 +272,7 @@ ...@@ -256,7 +272,7 @@
[inout] Inputs for function subdivide_integer: [inout] Inputs for function subdivide_integer:
v; vs v; vs
[inout] Out (internal) for function subdivide_pointer: [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: [inout] Inputs for function subdivide_pointer:
Frama_C_entropy_source; v Frama_C_entropy_source; v
[inout] Out (internal) for function subdivide_reduced_value: [inout] Out (internal) for function subdivide_reduced_value:
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment