\separated for stack-allocated variable length arrays
I have been trying to verify the following program with Frama-c (WP plugin).
#include <stdlib.h>
#define assume(e) if(!(e)) exit(-1);
extern int unknown_int(void);
int N;
int main()
{
N = unknown_int();
if(N <=0 ) return 1;
int i;
int a[N];
int b[N];
a[0] = 0;
b[0] = 1;
//@ assert b[0] == 1;
//@ assert \separated(a,b);
//@ assert a[0] == 0;
return 1;
}
For which frama-c, outputs the following statuses for each assertion
Assertion 0 < sizeof(int) * N <= 18446744073709551615: Valid
Assertion 0 < sizeof(int) * N <= 18446744073709551615: Valid
Assertion *(b + 0) == 1: Valid
Assertion \separated(a + 0, b + 0): Unknown
Assertion *(a + 0) == 0: Partially proven
When I change one of the arrays to a constant-sized array, say b to int [100], the output changes to
Assertion 0 < sizeof(int) * N <= 18446744073709551615: Valid
Assertion b[0] == 1: Valid
Assertion \separated(a + 0, &b[0]): Valid
Assertion *(a + 0) == 0: Valid
Is it not fair to assume stack-allocated arrays don't alias? Why does Frama-c treat variable length arrays differently from constant-sized ones?