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
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/syntax/decl-function.i (no preprocessing)
/* Generated by Frama-C */
int x;
void (*pf)(void);
extern void f_undefined(void);
void g(void)
{
f_undefined();
/*@ assert fcs_limitation: pf == &f_undefined; */ ;
return;
}
/*@ logic integer foo(integer y) = y;
*/
/*@ requires fcs_limitation: pf == &f_undefined;
ensures x == foo(x); */
extern void f_undefined(void);
void main(void)
{
pf = & f_undefined;
f_undefined();
f_undefined();
return;
}
|
