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
47
48
49
50
51
52
|
// This file should be entirely accepted
struct Type {
int field ;
} ;
void decl_ghost(void) /*@ ghost (int \ghost * p) */ ;
void def_ghost(void) /*@ ghost (int \ghost * p) */ {
}
void decl_not_ghost(void) /*@ ghost (int * p) */ ;
void def_not_ghost(void) /*@ ghost (int * p) */ {
}
int main(){
int i ;
int *p ;
int a[10];
//@ ghost int * gp1 = &i ;
//@ ghost int * gp2 = p ;
//@ ghost int * gp3 = a ;
/*@
ghost {
gp1 = &i ;
gp2 = p ;
gp3 = a ;
}
*/
struct Type ng_var ;
//@ ghost struct Type g_var ;
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) */ ;
}
|
