issue_508.res.oracle 1.13 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/issue_508.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
------------------------------------------------------------
  Function add
------------------------------------------------------------

Goal Assigns (file tests/wp_bts/issue_508.c, line 17) in 'add' (1/3):
Effect at line 21
Let a = shiftfield_F2_data(tbl_0).
Let x = to_uint32(d).
Assume {
  Type: is_sint32(d).
15
16
  (* Heap *)
  Type: (region(tbl_0.base) <= 0) /\ linked(Malloc_0).
17
  (* Goal *)
18
  When: !invalid(Malloc_0, shiftfield_F1_size(shift_S1(a, x)), 1).
19
20
  (* Pre-condition *)
  Have: (0 <= d) /\ (d <= 16) /\ valid_rw(Malloc_0, tbl_0, 35) /\
21
      valid_rw(Malloc_0, shift_S1(a, 0), 34).
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
}
Prove: (x <= d) /\ (d <= x).

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

Goal Assigns (file tests/wp_bts/issue_508.c, line 17) in 'add' (2/3):
Effect at line 22
Prove: true.

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

Goal Assigns (file tests/wp_bts/issue_508.c, line 17) in 'add' (3/3):
Effect at line 23
Prove: true.

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