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
|
[kernel] Parsing asm_with_contracts.i (no preprocessing)
/* Generated by Frama-C */
/*@ behavior b:
assumes z ≥ 0;
ensures \true; */
int f(int z)
{
int x = z;
int y = 2;
/*@ assigns y; */
__asm__ ("mov %1, %0\n\t" : "=r" (y) : "r" (x));
/*@ for b: assigns x, y; */
/*@ assigns x;
assigns x \from 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;
}
__inline static void insw(unsigned short __port, void *__addr,
unsigned long __count)
{
/*@ assigns __addr, __count, *((char *)__addr + (..));
assigns __addr
\from __port, (indirect: __addr), __count, *((char *)__addr + (..));
assigns __count
\from __port, (indirect: __addr), __count, *((char *)__addr + (..));
assigns *((char *)__addr + (..))
\from __port, (indirect: __addr), __count, *((char *)__addr + (..));
*/
__asm__ volatile (
"cld ; rep ; insw"
: "=D" (__addr), "=c" (__count)
: "d" (__port), "0" (__addr), "1" (__count)
);
return;
}
|
