Commit 1a72ad9e authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Merge branch 'feature/wp/test-cfg' into 'master'

[wp] updated oracles

See merge request frama-c/meta!41
parents 684577c8 7eff5178
......@@ -3,9 +3,6 @@
[meta] Will process 4 properties
[meta] Successful translation
[wp] Running WP plugin...
[wp] tests/meta-wp/invariant.c:74: Warning:
Ignored 'terminates' specification:
c ≢ 0
[wp] Warning: Missing RTE guards
[wp] 27 goals scheduled
[wp] [Qed] Goal typed_requiresInv_ensures_invariant_2_meta : Valid
......
......@@ -17,15 +17,15 @@
Goal Assertion 'test,meta' (file tests/meta-wp/typing.c, line 22):
Assume {
(* Heap *)
Type: (region(s_1.base) <= 0) /\ (region(t_1.base) <= 0) /\
Type: (region(s_1.base) <= 0) /\ (region(t.base) <= 0) /\
linked(Malloc_0) /\ cinits(Init_0).
(* Goal *)
When: is_uint32(i).
Have: (s = s_1) /\ (t_1 = t).
Have: s = s_1.
(* Pre-condition *)
Have: (shift_S4_S(t_1, i_1) = s_1) /\ is_sint32(i_1).
Have: (shift_S4_S(t, i_1) = s) /\ is_sint32(i_1).
(* Pre-condition *)
Have: (shift_S4_S(t_1, i_2) = s_1) /\ is_sint32(i_2).
Have: (shift_S4_S(t, i_2) = s) /\ is_sint32(i_2).
}
Prove: shiftfield_F4_S_b(shift_S4_S(t, i)) != shiftfield_F4_S_a(s).
Prover Alt-Ergo returns Valid
......@@ -41,14 +41,14 @@ Assume {
linked(Malloc_0) /\ cinits(Init_0).
(* Goal *)
When: !invalid(Malloc_0, a, 1).
Have: (s = s_1) /\ (t = t_1).
Have: s = s_1.
(* Pre-condition *)
Have: (shift_S4_S(t, i) = s_1) /\ is_sint32(i).
Have: (shift_S4_S(t, i) = s) /\ is_sint32(i).
(* Pre-condition *)
Have: (shift_S4_S(t, i_1) = s_1) /\ is_sint32(i_1).
Have: (shift_S4_S(t, i_1) = s) /\ is_sint32(i_1).
(* Assertion 'test,meta' *)
Have: forall i_2 : Z. (is_uint32(i_2) ->
(shiftfield_F4_S_b(shift_S4_S(t_1, i_2)) != a)).
(shiftfield_F4_S_b(shift_S4_S(t, i_2)) != a)).
}
Prove: a = shiftfield_F4_S_a(s_1).
Prover Qed returns Valid
......
......@@ -4,7 +4,6 @@
[meta] Warning: \called_arg cannot be used with indirect calls
[meta] Successful translation
[wp] Running WP plugin...
[wp] tests/meta-wp/uncalled.c:21: Warning: Missing 'calls' for default behavior
[wp] Warning: Missing RTE guards
[wp] Warning: No goal generated
[eva] Analyzing a complete application starting at main
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment