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
33
34
35
36
37
38
39
40
41
42
43
44
45
46
|
[kernel] Parsing ghost_cv_valid_ref.i (no preprocessing)
/* Generated by Frama-C */
struct Type {
int field ;
};
void decl_ghost(void) /*@ ghost (int \ghost *p) */;
void def_ghost(void) /*@ ghost (int \ghost *p) */
{
return;
}
void decl_not_ghost(void) /*@ ghost (int *p) */;
void def_not_ghost(void) /*@ ghost (int *p) */
{
return;
}
int main(void)
{
int __retres;
int i;
int *p;
int a[10];
struct Type ng_var;
/*@ ghost struct Type g_var; */
/*@ ghost int *gp1 = & i; */
/*@ ghost int *gp2 = p; */
/*@ ghost int *gp3 = a; */
/*@ ghost gp1 = & i;
gp2 = p;
gp3 = a; */
int *a_ptr_1 = & ng_var.field;
/*@ ghost int *a_ptr_2 = & ng_var.field; */
/*@ ghost int \ghost *a_ptr_4 = & g_var.field; */
/*@ ghost int b = 42; */
decl_ghost() /*@ ghost (& b) */;
def_ghost() /*@ ghost (& b) */;
decl_not_ghost() /*@ ghost (& i) */;
def_not_ghost() /*@ ghost (& i) */;
__retres = 0;
return __retres;
}
|
