diff --git a/tests/value/diff_gauges b/tests/value/diff_gauges index 99a2a77d76eb36ec86e285bdbb15fcf7486ddd9e..dd12f253ce78f91b8ba95eddc542732157afda92 100644 --- a/tests/value/diff_gauges +++ b/tests/value/diff_gauges @@ -147,33 +147,33 @@ diff tests/value/oracle/gauges.res.oracle tests/value/oracle_gauges/gauges.res.o > # Gauges domain: > V: [{[ p -> {{ &x }} > i -> {1} ]}] -> s395: λ(0) +> s398: λ(0) 478a437,440 > # Gauges domain: > V: [{[ i -> {1} ]}] -> s395: λ([0 .. 1]) +> s398: λ([0 .. 1]) > {[ i -> {1} ]} 537a500,503 > # Gauges domain: > V: [{[ i -> {1} ]}] -> s395: λ([0 .. 2]) +> s398: λ([0 .. 2]) > {[ i -> {1} ]} 596a563,566 > # Gauges domain: > V: [{[ i -> {1} ]}] -> s395: λ([0 .. 10]) +> s398: λ([0 .. 10]) > {[ i -> {1} ]} 661a632,636 > # Gauges domain: > V: [{[ p -> {{ &a }} > i -> {2} ]}] -> s409: λ(0) -> s408: λ(0) +> s412: λ(0) +> s411: λ(0) 722a698,702 > # Gauges domain: > V: [{[ i -> {2} ]}] -> s409: λ(0) -> s408: λ([0 .. 1]) +> s412: λ(0) +> s411: λ([0 .. 1]) > {[ i -> {0} ]} 724a705,832 > [eva] tests/value/gauges.c:325: @@ -236,8 +236,8 @@ diff tests/value/oracle/gauges.res.oracle tests/value/oracle_gauges/gauges.res.o > S_1___fc_env[0..1] ∈ [--..--] > # Gauges domain: > V: [{[ i -> {2} ]}] -> s409: λ(0) -> s408: λ([0 .. 2]) +> s412: λ(0) +> s411: λ([0 .. 2]) > {[ i -> {0} ]} > ==END OF DUMP== > [eva] tests/value/gauges.c:325: @@ -300,8 +300,8 @@ diff tests/value/oracle/gauges.res.oracle tests/value/oracle_gauges/gauges.res.o > S_1___fc_env[0..1] ∈ [--..--] > # Gauges domain: > V: [{[ i -> {2} ]}] -> s409: λ(0) -> s408: λ([0 .. +oo]) +> s412: λ(0) +> s411: λ([0 .. +oo]) > {[ i -> {0} ]} > ==END OF DUMP== 732a841,842 diff --git a/tests/value/gauges.c b/tests/value/gauges.c index cd1619e90e511a5f15dfd714a89486470171026b..ab2963f70b41dbb3f18e2a7915fc2d81a7c0d5d4 100644 --- a/tests/value/gauges.c +++ b/tests/value/gauges.c @@ -170,12 +170,12 @@ void main8_aux (unsigned int n) { int *p = arr; do { Frama_C_show_each(n); - *p++ = n; + *p++ = n; // Invalid access memory if more than 65536 iterations. } while (--n); } void main8() { - main8_aux(0); + if (v) main8_aux(0); // This call can legitimately lead to bottom. } void main9() { diff --git a/tests/value/oracle/gauges.res.oracle b/tests/value/oracle/gauges.res.oracle index 18dd8eea6bdd67932e7fc01d51851c6e6edc9444..fa19ee9d0ef3002d43a7656080239d7a89f6a42b 100644 --- a/tests/value/oracle/gauges.res.oracle +++ b/tests/value/oracle/gauges.res.oracle @@ -1163,7 +1163,7 @@ [inout] Out (internal) for function main8: \nothing [inout] Inputs for function main8: - \nothing + v [inout] Out (internal) for function main9: x[0..9]; y[0..9]; p; q; z; i; r [inout] Inputs for function main9: