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
|
[kernel] Parsing attributes-declarations-definitions.c (with preprocessing)
[kernel] attributes-declarations-definitions.c:12: Warning:
found two contracts (old location: attributes-declarations-definitions.c:6). Merging them
[kernel] attributes-declarations-definitions.c:21: Warning:
found two contracts (old location: attributes-declarations-definitions.c:13). Merging them
/* Generated by Frama-C */
typedef int __attribute__((__a1__)) aint;
typedef int __attribute__((__p1__)) * __attribute__((__p2__)) iptr;
int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f
(int const __attribute__((__arg3__)) p3) __attribute__((__f5__, __f4__,
__f2__, __f1__));
/*@ requires p3 ≥ 3;
requires p3 ≥ 1;
requires p3 ≥ 4; */
int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f
(int const __attribute__((__arg3__)) p3) __attribute__((__f5__, __f4__,
__f2__, __f1__));
int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f
(int const __attribute__((__arg3__)) p3)
{
int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) __retres;
__retres = (int __attribute__((__tret3__, __tret2__, __tret1__)))p3;
return __retres;
}
aint g(int __attribute__((__a2__)) i3);
aint g(int __attribute__((__a2__)) i3)
{
aint __retres;
__retres = (aint)i3;
return __retres;
}
iptr h(iptr volatile ip2);
iptr h(iptr volatile ip2)
{
iptr __retres;
__retres = (iptr)0;
return __retres;
}
void test(void)
{
int a;
int b __attribute__((__unused__));
return;
}
int __attribute__((__o__)) one_letter_attribute;
int __attribute__((__n__)) one_letter_attribute_with_underscore;
int __attribute__((__e__)) one_letter_attribute_with_underscore_after;
|
