shift_lemma.1.res.oracle 2.14 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing tests/wp_typed/shift_lemma.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
------------------------------------------------------------
  Function f
------------------------------------------------------------

Goal Assertion (file tests/wp_typed/shift_lemma.i, line 21):
Let x = Mint_0[shiftfield_F2_s_d(p)].
Let a = shiftfield_F2_s_u(p).
Assume {
  Type: is_sint32(x) /\ is_sint32(Mint_0[shiftfield_F2_s_e(p)]) /\
14
15
      is_sint32(Mint_0[shiftfield_F1_t_c(shift_S1_t(a, 0))]) /\
      is_sint32(Mint_0[shiftfield_F1_t_c(shift_S1_t(a, 1))]).
16
  (* Heap *)
17
  Type: region(p.base) <= 0.
18
19
20
21
22
23
24
25
26
27
28
  (* Pre-condition *)
  Have: P_inv(Mint_0, p).
}
Prove: x = 0.

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

Goal Assertion (file tests/wp_typed/shift_lemma.i, line 22):
Let a = shiftfield_F2_s_u(p).
Assume {
  Type: is_sint32(Mint_0[shiftfield_F2_s_e(p)]) /\
29
30
      is_sint32(Mint_0[shiftfield_F1_t_c(shift_S1_t(a, 0))]) /\
      is_sint32(Mint_0[shiftfield_F1_t_c(shift_S1_t(a, 1))]).
31
32
  (* Heap *)
  Type: region(p.base) <= 0.
33
34
35
36
37
38
39
  (* Goal *)
  When: (0 <= i) /\ (i <= 9) /\ is_sint32(i).
  (* Pre-condition *)
  Have: P_inv(Mint_0, p).
  (* Assertion *)
  Have: Mint_0[shiftfield_F2_s_d(p)] = 0.
}
40
Prove: Mint_0[shiftfield_F1_t_c(shift_S1_t(a, i))] = 0.
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58

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

Goal Assertion (file tests/wp_typed/shift_lemma.i, line 23):
Prove: true.

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

Goal Assertion (file tests/wp_typed/shift_lemma.i, line 24):
Prove: true.

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

Goal Assertion (file tests/wp_typed/shift_lemma.i, line 25):
Let x = Mint_0[shiftfield_F2_s_e(p)].
Assume {
  Type: is_sint32(x).
  (* Heap *)
59
  Type: region(p.base) <= 0.
60
61
62
63
64
65
  (* Pre-condition *)
  Have: P_inv(Mint_0, p).
  (* Assertion *)
  Have: Mint_0[shiftfield_F2_s_d(p)] = 0.
  (* Assertion *)
  Have: forall i : Z. ((0 <= i) -> ((i <= 9) ->
66
      (Mint_0[shiftfield_F1_t_c(shift_S1_t(shiftfield_F2_s_u(p), i))] = 0))).
67
68
69
70
}
Prove: x = 0.

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