# 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).
  (* Heap *)
  Type: (region(tbl_0.base) <= 0) /\ linked(Malloc_0).
  (* Goal *)
  When: !invalid(Malloc_0, shiftfield_F1_size(shift_S1(a, x)), 1).
  (* Pre-condition *)
  Have: (0 <= d) /\ (d <= 16) /\ valid_rw(Malloc_0, tbl_0, 35) /\
      valid_rw(Malloc_0, shift_S1(a, 0), 34).
}
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.

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