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
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
|
[kernel] Parsing ghost_else.i (no preprocessing)
/* Generated by Frama-C */
/* run.config
OPT: -no-autoload-plugins -keep-comments -print
*/
void normal_only_if(int x, int y)
{
if (x) x ++;
return;
}
void normal_if_else(int x, int y)
{
if (x) x ++; else y ++;
return;
}
void normal_if_else_intricated(int x, int y)
{
if (x)
if (y) y ++; else x ++;
return;
}
void if_ghost_else_one_line(int x) /*@ ghost (int y) */
{
if (x) x ++;
/*@ ghost else y ++;*/
return;
}
void if_ghost_else_one_line_escaped(int x) /*@ ghost (int y) */
{
if (x) x ++;
/*@ ghost else y ++;*/
return;
}
void if_ghost_else_block(int x) /*@ ghost (int y) */
{
if (x) x ++;
/*@ ghost else y ++;*/
return;
}
void if_ghost_else_multi_line_block(int x) /*@ ghost (int y) */
{
if (x) x ++;
/*@ ghost else {
y ++;
y += x;
y --;
}*/
return;
}
void if_ghost_else_block_comments(int x) /*@ ghost (int y) */
{
if (x) x ++;
/*@ ghost else y ++;*/
//// comment 1
//// comment 2
return;
}
void if_ghost_else_block_comments_escaped(int x) /*@ ghost (int y) */
{
if (x) x ++;
/*@ ghost else y ++;*/
//// comment 1\
//continued
return;
}
void normal_if_ghost_else_intricated(int x) /*@ ghost (int y) */
{
if (x)
if (x) x ++;
/*@ ghost else y ++;*/
return;
}
// we must take care to keep the "if" bloc when pretty-printing
// as removing the brackets changes the program.
void ghost_else_plus_else_association(int x) /*@ ghost (int y) */
{
if (x) {
if (x) x ++;
/*@ ghost else y --;*/
}
else x ++;
return;
}
// pretty-printer must take care of keeping the braces around the
// single-(ghost)-statement blocks. Otherwise, the code is syntactically
// invalid (empty, from a non-ghost point-of-view, then clause)
void non_ghost_if_with_ghost_body(int x) /*@ ghost (int y) */
{
if (x) {
/*@ ghost y ++; */
}
else {
/*@ ghost y --; */
}
return;
}
// pretty-printer must take care of keeping the braces around the
// single-(ghost)-statement blocks. Even if the ghost statement is an
// empty block!
void non_ghost_if_with_nop_ghost_body(int x) /*@ ghost (int y) */
{
if (! x) {
/*@ ghost y ++; */
}
return;
}
|
