diff --git a/tests/rte/array_index.c b/tests/rte/array_index.c index 85c8c6bd1ddbf1a68b88992f3e5ca834aa44f37f..b976e42cce80e05920e1870208d858e4db473a18 100644 --- a/tests/rte/array_index.c +++ b/tests/rte/array_index.c @@ -44,4 +44,7 @@ void main(int i, int j, unsigned int k) { s.t[k] = 0; s.s.u[k] = 0; s.v[k].t[c[k]] = 0; + + int x; + int t[100 / sizeof(x)]; } diff --git a/tests/rte/oracle/array_index.0.res.oracle b/tests/rte/oracle/array_index.0.res.oracle index 6acdd373586e604dd2da7626f9e3051dfde58a75..5c3fb974325cbda6d9de1021b6dbb256232021df 100644 --- a/tests/rte/oracle/array_index.0.res.oracle +++ b/tests/rte/oracle/array_index.0.res.oracle @@ -20,6 +20,8 @@ ts s; unsigned int c[10]; void main(int i, int j, unsigned int k) { + int x; + int t_0[(unsigned int)100 / sizeof(x)]; t[0] = 0; u[1] = 0; v[2][3] = 0; @@ -89,6 +91,8 @@ ts s; unsigned int c[10]; void main(int i, int j, unsigned int k) { + int x; + int t_0[(unsigned int)100 / sizeof(x)]; /*@ assert rte: index_bound: 0 ≤ 0; */ /*@ assert rte: index_bound: 0 < 10; */ t[0] = 0; diff --git a/tests/rte/oracle/array_index.1.res.oracle b/tests/rte/oracle/array_index.1.res.oracle index 31cf7a921b3d4ccc106b05db4eda7683c0acae49..79017aa000bce2cb6547667f2d43b6cf3088cdba 100644 --- a/tests/rte/oracle/array_index.1.res.oracle +++ b/tests/rte/oracle/array_index.1.res.oracle @@ -20,6 +20,8 @@ ts s; unsigned int c[10]; void main(int i, int j, unsigned int k) { + int x; + int t_0[(unsigned int)100 / sizeof(x)]; t[0] = 0; u[1] = 0; v[2][3] = 0;