1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
|
[kernel] Parsing vla_multidim.c (with preprocessing)
/* Generated by Frama-C */
int const n = 10;
/*@ assigns \nothing;
frees p; */
__attribute__((__FC_BUILTIN__)) void __fc_vla_free(void *p);
/*@ assigns \result;
assigns \result \from \nothing;
allocates \result; */
__attribute__((__FC_BUILTIN__)) void *__fc_vla_alloc(unsigned int size);
void main(void)
{
unsigned int __lengthof_a;
unsigned int __lengthof_b;
/*@ assert alloca_bounds: 0 < sizeof(int [42]) * n ≤ 4294967295; */ ;
__lengthof_a = (unsigned int)n;
int (*a)[42] = __fc_vla_alloc(sizeof(int [42]) * __lengthof_a);
(*(a + 0))[0] = 1;
/*@
assert
alloca_bounds: 0 < sizeof(int [5][10]) * (*(a + 0))[0] ≤ 4294967295; */
;
__lengthof_b = (unsigned int)(*(a + 0))[0];
int (*b)[5][10] = __fc_vla_alloc(sizeof(int [5][10]) * __lengthof_b);
__fc_vla_free((void *)b);
__fc_vla_free((void *)a);
return;
}
|
