diff --git a/tests/value/domains.i b/tests/value/domains.i index 22b198ea39fc8bd5e37848ce41c3dbf82294acd3..4d00d8b9d74ca6102a5ac5e120d4be8f742a5338 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 5bb482d01c270bc8a4f948c4ec50f9277129a034..d4fe3a14f49259e070e14ca2d9d70d781afec137 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