Skip to content
Snippets Groups Projects
Commit 68e7678d authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[tests] add test for RTE issue mentioned in MR !2261

parent 16031ca0
No related branches found
No related tags found
No related merge requests found
......@@ -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)];
}
......@@ -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;
......
......@@ -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;
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment