cast_fits.1.res.oracle 4.81 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_typed/cast_fits.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] tests/wp_typed/cast_fits.i:13: Warning: 
  Cast with incompatible pointers types (source: __anonstruct_L2_2*)
     (target: sint32*)
[wp] tests/wp_typed/cast_fits.i:54: Warning: 
  Cast with incompatible pointers types (source: __anonunion_L8_8*)
     (target: sint32*)
[wp] tests/wp_typed/cast_fits.i:60: Warning: 
  Cast with incompatible pointers types (source: sint32*)
     (target: __anonunion_L8_8*)
------------------------------------------------------------
  Function fits1
------------------------------------------------------------

Goal Post-condition (file tests/wp_typed/cast_fits.i, line 3) in 'fits1':
Let x = Mint_0[p].
Let x_1 = Mint_0[shiftfield_F1_i1(p)].
Assume {
  Type: is_sint32(x) /\ is_sint32(x_1).
  (* Heap *)
24
  Type: region(p.base) <= 0.
25
26
27
28
29
30
31
32
33
34
35
36
37
38
}
Prove: x_1 = x.

------------------------------------------------------------
------------------------------------------------------------
  Function fits2
------------------------------------------------------------

Goal Post-condition (file tests/wp_typed/cast_fits.i, line 19) in 'fits2':
Let x = Mint_0[shiftfield_F2_i2(p)].
Let x_1 = Mint_0[shiftfield_F1_i1(shiftfield_F3_ic3(p))].
Assume {
  Type: is_sint32(x) /\ is_sint32(x_1).
  (* Heap *)
39
  Type: region(p.base) <= 0.
40
41
42
43
44
45
46
47
48
49
}
Prove: x_1 = x.

------------------------------------------------------------
------------------------------------------------------------
  Function fits3
------------------------------------------------------------

Goal Post-condition (file tests/wp_typed/cast_fits.i, line 27) in 'fits3':
Let x = Mint_0[shiftfield_F2_i2(p)].
50
Let x_1 = Mint_0[shiftfield_F1_i1(shift_S1(shiftfield_F4_ic4(p), 0))].
51
52
53
Assume {
  Type: is_sint32(x) /\ is_sint32(x_1).
  (* Heap *)
54
  Type: region(p.base) <= 0.
55
56
57
58
59
60
61
62
63
}
Prove: x_1 = x.

------------------------------------------------------------
------------------------------------------------------------
  Function fits4
------------------------------------------------------------

Goal Post-condition (file tests/wp_typed/cast_fits.i, line 37) in 'fits4':
64
Let x = Mchar_0[shiftfield_F6_c6(p)].
65
Let x_1 = Mchar_0[shiftfield_F3_c3(shift_S3(shiftfield_F5_ci5(p), 1))].
66
67
68
Assume {
  Type: is_sint8(x) /\ is_sint32(x) /\ is_sint8(x_1).
  (* Heap *)
69
  Type: (region(p.base) <= 0) /\ sconst(Mchar_0).
70
71
72
73
74
75
76
77
78
}
Prove: x_1 = x.

------------------------------------------------------------
------------------------------------------------------------
  Function fits5
------------------------------------------------------------

Goal Post-condition (file tests/wp_typed/cast_fits.i, line 45) in 'fits5':
79
Let x = Mint_0[p].
80
81
82
83
Let x_1 = Mint_0[shiftfield_F7_u7(p)].
Assume {
  Type: is_sint32(x) /\ is_sint32(x_1).
  (* Heap *)
84
  Type: region(p.base) <= 0.
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
}
Prove: x_1 = x.

------------------------------------------------------------
------------------------------------------------------------
  Function mismatch1
------------------------------------------------------------

Goal Post-condition (file tests/wp_typed/cast_fits.i, line 11) in 'mismatch1':
tests/wp_typed/cast_fits.i:13: warning from Typed Model:
 - Warning: Hide sub-term definition
   Reason: Cast with incompatible pointers types (source: __anonstruct_L2_2*)
   (target: sint32*)
Let x = Mint_0[q].
Let x_1 = Mchar_0[shiftfield_F2_c2(p)].
Assume {
  Type: is_sint32(x) /\ is_sint8(x_1).
  (* Heap *)
103
  Type: (region(p.base) <= 0) /\ sconst(Mchar_0).
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
}
Prove: x_1 = x.

------------------------------------------------------------
------------------------------------------------------------
  Function mismatch2
------------------------------------------------------------

Goal Post-condition (file tests/wp_typed/cast_fits.i, line 52) in 'mismatch2':
tests/wp_typed/cast_fits.i:54: warning from Typed Model:
 - Warning: Hide sub-term definition
   Reason: Cast with incompatible pointers types (source: __anonunion_L8_8*)
   (target: sint32*)
Let x = Mint_0[q].
Let x_1 = Mint_0[shiftfield_F8_i8(p)].
Assume {
  Type: is_sint32(x) /\ is_sint32(x_1).
  (* Heap *)
122
  Type: region(p.base) <= 0.
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
}
Prove: x_1 = x.

------------------------------------------------------------
------------------------------------------------------------
  Function mismatch3
------------------------------------------------------------

Goal Post-condition (file tests/wp_typed/cast_fits.i, line 58) in 'mismatch3':
tests/wp_typed/cast_fits.i:60: warning from Typed Model:
 - Warning: Hide sub-term definition
   Reason: Cast with incompatible pointers types (source: sint32*)
   (target: __anonunion_L8_8*)
Let x = Mint_0[p].
Let x_1 = Mint_0[shiftfield_F8_i8(q)].
Assume {
  Type: is_sint32(x) /\ is_sint32(x_1).
  (* Heap *)
141
  Type: region(p.base) <= 0.
142
143
144
145
}
Prove: x_1 = x.

------------------------------------------------------------