[WP] Value of 2D-array does not work well
Steps to reproduce the issue
#define NUM 5
int x[NUM][NUM];
/*@
@ requires \forall integer i, j; 0 <= i < NUM && 0 <= j < NUM ==> 0 <= x[i][j] < 100;
@*/
void foo()
{
int tmp;
for (int i = 0; i < NUM; i++)
{
for (int j = 0; j < NUM; j++)
{
tmp = x[i][j] + 1;
//@ assert PASS: 1 <= tmp < 101;
//@ assert ASSERTED: tmp < 100;
}
}
if (tmp > 100)
{
tmp = 1;
return;
}
else
{
tmp = 2;
return;
}
}
Expected behaviour
PASS should be pass and ASSERTED should be triggered.
Actual behaviour
Both of the assertion were triggered in WP
i'm using command:
frama-c -wp -wp-no-rte -wp-prover z3-nobv,alt-ergo -wp-cache 'rebuild' -wp-model 'Typed' -pp-annot -c11 -kernel-msg-key pp -main foo -lib-entry ./test.c
Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 26.1 (as reported by
frama-c -version
) - Plug-in used: WP
- OS name: Ubuntu
- OS version: 20.04
Additional information (optional)
this 2d-array phenomenon is also observed when I'm writing loop assigns like this:
#define NUM 5
int x[NUM][NUM];
/*@
@ ;
@*/
void foo()
{
/*@
@ loop assigns x[0 .. NUM - 1][0 .. NUM - 1];
@*/
for (int i = 0; i < NUM; i++)
{
/*@
@ loop assigns x[i][0 .. NUM - 1];
@*/
for (int j = 0; j < NUM; j++)
{
x[i][j] = i * j;
}
}
return;
}