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
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/syntax/asm_with_contracts.i (no preprocessing)
/* Generated by Frama-C */
/*@ behavior b:
assumes z ≥ 0;
ensures \true; */
int f(int z)
{
int x;
int y;
x = z;
y = 2;
/*@ assigns y; */
__asm__ ("mov %1, %0\n\t" : "=r" (y) : "r" (x));
/*@ assigns x;
assigns x \from y; */
/*@ for b: assigns x, y; */
__asm__ ("mov %1, %0\n\t" : "=r" (x) : "r" (y));
/*@ assigns x, y;
behavior c:
assumes x ≥ 0;
ensures y ≥ 0;
assigns y;
assigns y \from x;
*/
__asm__ ("mov %1, %0\n\t" : "=r" (y) : "r" (x));
return x;
}
|
