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
|
[kernel] Parsing const_formals.i (no preprocessing)
[kernel:typing:incompatible-types-call] const_formals.i:28: Warning:
implicit conversion between incompatible function types:
int (*)(int *x)
and
int (*)(int const *y)
[kernel:typing:incompatible-types-call] const_formals.i:28: Warning:
expected 'int (*)(int const *y)' but got argument of type 'int (*)(int *x)': & incr_get
/* Generated by Frama-C */
char const *s = "foo";
char mutable_s[4] = {(char)'b', (char)'a', (char)'r', (char)'\000'};
char const **p = & s;
char f(char const *s_0)
{
char __retres;
__retres = *(s_0 + 0);
return __retres;
}
char g(char const * const *a)
{
char __retres;
__retres = *(*a);
return __retres;
}
void foo(int *x, int * restrict y);
void foo(int *x, int * restrict y)
{
int *tmp;
int *tmp_0;
tmp = x;
x ++;
;
tmp_0 = y;
y --;
;
return;
}
int incr_get(int *x)
{
int __retres;
int *tmp;
tmp = x;
x ++;
;
__retres = *x;
return __retres;
}
int get(int const *x)
{
int __retres;
__retres = *x;
return __retres;
}
int apply_const(int *x, int (*g_0)(int const *y))
{
int tmp;
tmp = (*g_0)((int const *)x);
return tmp;
}
int apply_non_const(int *x, int (*g_0)(int *y))
{
int tmp;
tmp = (*g_0)(x);
return tmp;
}
int main(void)
{
int __retres;
int x = 1;
apply_const(& x,(int (*)(int const *y))(& incr_get));
apply_non_const(& x,& incr_get);
apply_const(& x,& get);
apply_non_const(& x,(int (*)(int *y))(& get));
char c = f((char const *)(mutable_s));
char d = g((char const * const *)p);
__retres = 0;
return __retres;
}
|
