diff --git a/tests/value/octagons.c b/tests/value/octagons.c
index 101dafb7febcfda4bf4d2d67b16d71a76e55aa50..cbc98a770dce506d2b40a7381db9045d56d17f0f 100644
--- a/tests/value/octagons.c
+++ b/tests/value/octagons.c
@@ -223,6 +223,39 @@ void pub301 () {
}
}
+#define MAX 20
+
+void arrays () {
+ int a[MAX], t[MAX];
+ /*@ loop unroll MAX; */ // Unroll to ensure array initialization.
+ for (int i = 0; i < MAX; i++) {
+ a[i] = undet;
+ }
+
+ int x = Frama_C_interval(1, MAX);
+ for (int j = x - 1; j >= 0; j--) {
+ // Need the relation j <= x-1 to prove that index x-1-j >= 0.
+ t[j] = a[x - 1 - j];
+ }
+
+ int y = Frama_C_interval(0, MAX-1);
+ int index = (MAX-1) - y;
+ for (int j = y; j < MAX; j++) {
+ // Need the relation index + j == MAX-1 to prove index >= 0.
+ t[index] = a[j];
+ index --;
+ }
+
+ // Same with a floating-point variable f instead of x.
+ float f = Frama_C_float_interval(0., (float)(MAX-1));
+ index = (MAX-1) - (int)f;
+ for (int j = (int)f; j < MAX; j++) {
+ // Need the relation index + j == MAX-1 to prove index >= 0.
+ t[index] = a[j];
+ index --;
+ }
+}
+
void main () {
demo ();
integer_types ();
@@ -234,4 +267,5 @@ void main () {
interprocedural ();
dump ();
pub301 ();
+ arrays ();
}
diff --git a/tests/value/oracle/octagons.res.oracle b/tests/value/oracle/octagons.res.oracle
index c5865a36e4b056718034bb0d8e4f90972ed6f8ea..467fabee6f41493dd9b4c639b48505dba0e3073a 100644
--- a/tests/value/oracle/octagons.res.oracle
+++ b/tests/value/oracle/octagons.res.oracle
@@ -5,7 +5,7 @@
[eva:initial-state] Values of globals at initialization
undet ∈ [--..--]
[eva] computing for function demo <- main.
- Called from octagons.c:227.
+ Called from octagons.c:260.
[eva] computing for function Frama_C_interval <- demo <- main.
Called from octagons.c:12.
[eva] using specification for function Frama_C_interval
@@ -19,7 +19,7 @@
[eva] Recording results for demo
[eva] Done for function demo
[eva] computing for function integer_types <- main.
- Called from octagons.c:228.
+ Called from octagons.c:261.
[eva] computing for function Frama_C_interval <- integer_types <- main.
Called from octagons.c:23.
[eva] octagons.c:23:
@@ -69,7 +69,7 @@
[eva] Recording results for integer_types
[eva] Done for function integer_types
[eva] computing for function arith <- main.
- Called from octagons.c:229.
+ Called from octagons.c:262.
[eva] computing for function Frama_C_interval <- arith <- main.
Called from octagons.c:70.
[eva] octagons.c:70:
@@ -107,7 +107,7 @@
[eva] Recording results for arith
[eva] Done for function arith
[eva] computing for function join <- main.
- Called from octagons.c:230.
+ Called from octagons.c:263.
[eva] computing for function Frama_C_interval <- join <- main.
Called from octagons.c:103.
[eva] octagons.c:103:
@@ -138,7 +138,7 @@
[eva] Recording results for join
[eva] Done for function join
[eva] computing for function loop <- main.
- Called from octagons.c:231.
+ Called from octagons.c:264.
[eva] computing for function Frama_C_interval <- loop <- main.
Called from octagons.c:128.
[eva] octagons.c:128:
@@ -164,7 +164,7 @@
[eva] Recording results for loop
[eva] Done for function loop
[eva] computing for function pointers <- main.
- Called from octagons.c:232.
+ Called from octagons.c:265.
[eva] computing for function Frama_C_interval <- pointers <- main.
Called from octagons.c:151.
[eva] octagons.c:151:
@@ -188,7 +188,7 @@
[eva] Recording results for pointers
[eva] Done for function pointers
[eva] computing for function saturate <- main.
- Called from octagons.c:233.
+ Called from octagons.c:266.
[eva] computing for function Frama_C_interval <- saturate <- main.
Called from octagons.c:169.
[eva] octagons.c:169:
@@ -203,7 +203,7 @@
[eva] Recording results for saturate
[eva] Done for function saturate
[eva] computing for function interprocedural <- main.
- Called from octagons.c:234.
+ Called from octagons.c:267.
[eva] computing for function Frama_C_interval <- interprocedural <- main.
Called from octagons.c:182.
[eva] octagons.c:182:
@@ -234,7 +234,7 @@
[eva] Recording results for interprocedural
[eva] Done for function interprocedural
[eva] computing for function dump <- main.
- Called from octagons.c:235.
+ Called from octagons.c:268.
[eva] computing for function Frama_C_interval <- dump <- main.
Called from octagons.c:206.
[eva] octagons.c:206:
@@ -259,7 +259,7 @@
[eva] Recording results for dump
[eva] Done for function dump
[eva] computing for function pub301 <- main.
- Called from octagons.c:236.
+ Called from octagons.c:269.
[eva] computing for function Frama_C_interval <- pub301 <- main.
Called from octagons.c:216.
[eva] octagons.c:216:
@@ -272,6 +272,31 @@
[eva] Done for function Frama_C_interval
[eva] Recording results for pub301
[eva] Done for function pub301
+[eva] computing for function arrays <- main.
+ Called from octagons.c:270.
+[eva] computing for function Frama_C_interval <- arrays <- main.
+ Called from octagons.c:235.
+[eva] octagons.c:235:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] octagons.c:236: starting to merge loop iterations
+[eva] computing for function Frama_C_interval <- arrays <- main.
+ Called from octagons.c:241.
+[eva] octagons.c:241:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] octagons.c:243: starting to merge loop iterations
+[eva] computing for function Frama_C_float_interval <- arrays <- main.
+ Called from octagons.c:250.
+[eva] using specification for function Frama_C_float_interval
+[eva] octagons.c:250:
+ function Frama_C_float_interval: precondition 'finite' got status valid.
+[eva] octagons.c:250:
+ function Frama_C_float_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_float_interval
+[eva] octagons.c:252: starting to merge loop iterations
+[eva] Recording results for arrays
+[eva] Done for function arrays
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -283,6 +308,14 @@
x ∈ [-28..0]
y ∈ [1..29]
r ∈ [-29..106]
+[eva:final-states] Values at end of function arrays:
+ Frama_C_entropy_source ∈ [--..--]
+ a[0..19] ∈ [--..--]
+ t[0..19] ∈ [--..--] or UNINITIALIZED
+ x ∈ [1..20]
+ y ∈ [0..19]
+ index ∈ {-1}
+ f ∈ [-0. .. 19.]
[eva:final-states] Values at end of function demo:
Frama_C_entropy_source ∈ [--..--]
y ∈ [--..--]
@@ -364,6 +397,10 @@
[from] Computing for function Frama_C_interval <-arith
[from] Done for function Frama_C_interval
[from] Done for function arith
+[from] Computing for function arrays
+[from] Computing for function Frama_C_float_interval <-arrays
+[from] Done for function Frama_C_float_interval
+[from] Done for function arrays
[from] Computing for function demo
[from] Done for function demo
[from] Computing for function diff
@@ -390,11 +427,16 @@
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_float_interval:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ \result FROM Frama_C_entropy_source; min; max
[from] Function Frama_C_interval:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
\result FROM Frama_C_entropy_source; min; max
[from] Function arith:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] Function arrays:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function demo:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function diff:
@@ -424,6 +466,10 @@
Frama_C_entropy_source; k; a; b; x; y; r
[inout] Inputs for function arith:
Frama_C_entropy_source
+[inout] Out (internal) for function arrays:
+ Frama_C_entropy_source; a[0..19]; t[0..19]; i; x; j; y; index; j_0; f; j_1
+[inout] Inputs for function arrays:
+ Frama_C_entropy_source; undet
[inout] Out (internal) for function demo:
Frama_C_entropy_source; y; k; x; r; t
[inout] Inputs for function demo:
diff --git a/tests/value/oracle_apron/octagons.res.oracle b/tests/value/oracle_apron/octagons.res.oracle
index 431455b54fd064e93b64e9536f2b4b3c53d9326f..b97678e683e847c47493ab076e688d4dd49654cb 100644
--- a/tests/value/oracle_apron/octagons.res.oracle
+++ b/tests/value/oracle_apron/octagons.res.oracle
@@ -1,4 +1,4 @@
-325,328c325,328
+358,361c358,361
< a ∈ [-1024..2147483647]
< b ∈ [-1023..2147483647]
< c ∈ [-1023..2147483647]
diff --git a/tests/value/oracle_equality/octagons.res.oracle b/tests/value/oracle_equality/octagons.res.oracle
index 1917faccaadbc5d43d3e549c0832dba3b8ad3ddb..abca6359403c77796f85f7af8887c5f768258aa0 100644
--- a/tests/value/oracle_equality/octagons.res.oracle
+++ b/tests/value/oracle_equality/octagons.res.oracle
@@ -2,7 +2,7 @@
< [eva] octagons.c:54: Frama_C_show_each_unreduced_char: [-128..127], [-128..127]
---
> [eva] octagons.c:54: Frama_C_show_each_unreduced_char: [-118..114], [6..127]
-312c312
+345c345
< ct ∈ [--..--] or UNINITIALIZED
---
> ct ∈ [6..127] or UNINITIALIZED
diff --git a/tests/value/oracle_gauges/octagons.res.oracle b/tests/value/oracle_gauges/octagons.res.oracle
index 37ac2f4f7980b9d318b6577cc9d68019f762f69c..f65503794d5e3a35cfa3a0c62bfdceccc32849dc 100644
--- a/tests/value/oracle_gauges/octagons.res.oracle
+++ b/tests/value/oracle_gauges/octagons.res.oracle
@@ -11,7 +11,7 @@
< [eva] octagons.c:143: Frama_C_show_each_imprecise: [-2147483648..1]
---
> [eva] octagons.c:143: Frama_C_show_each_imprecise: [-2468..1]
-325,328c317,320
+358,361c350,353
< a ∈ [-1024..2147483647]
< b ∈ [-1023..2147483647]
< c ∈ [-1023..2147483647]
@@ -21,7 +21,7 @@
> b ∈ [-181..1867]
> c ∈ [-602..1446]
> d ∈ [-190..1874]
-330c322
+363c355
< d2 ∈ [-2147483648..1]
---
> d2 ∈ [-2468..1]