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
|
[kernel] Parsing asm_goto.i (no preprocessing)
/* Generated by Frama-C */
void basic(void)
{
__asm__ ("xor %eax, %eax\n\t");
return;
}
void pretty(void)
{
/*@ assigns \nothing; */
__asm__ volatile ("pxor %%mm7, %%mm7\n\t"
"pcmpeqd %%mm6, %%mm6" : );
return;
}
int main(unsigned short bit)
{
int __retres;
/*@ assigns \nothing; */
__asm__ goto ("1: jmp %l[t_no]\n" : : "i" (bit) : :t_no);
__retres = 1;
goto return_label;
t_no: __retres = 0;
return_label: return __retres;
}
|
