Commit 940608c0 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] Test local_init initialized + update oracles

parent 122a4bce
......@@ -352,7 +352,7 @@ new way
main_assigns_global sequent:
Assume {
Have: foo_1 = 42.
Have: (Init_r_0=false) /\ (ta_r_0=true) /\ (ta_r_1=false).
Have: (ta_r_0=true) /\ (ta_r_1=false).
Have: foo_2 = 1.
Have: x = result_0.
Have: x = foo_0.
......@@ -370,7 +370,7 @@ Prove: foo_0 = 1.
main_assigns_global sequent:
Assume {
Have: foo_1 = 42.
Have: (Init_r_0=false) /\ (ta_r_0=true) /\ (ta_r_1=false).
Have: (ta_r_0=true) /\ (ta_r_1=false).
Have: foo_2 = 1.
Have: x = result_0.
Have: x = foo_0.
......@@ -387,7 +387,7 @@ Prove: true.
main_assigns_global sequent:
Assume {
Have: foo_1 = 42.
Have: (Init_r_0=false) /\ (ta_r_0=true) /\ (ta_r_1=false).
Have: (ta_r_0=true) /\ (ta_r_1=false).
Have: foo_2 = 1.
Have: x = result_0.
Have: x = foo_0.
......@@ -405,8 +405,8 @@ zloop sequent:
Assume {
Have: foo_0 = 42.
Have: 0 <= x.
Have: (Init_i_0=false) /\ (ta_i_0=true) /\ (ta_i_1=false).
Have: i_1 = 0.
Have: (ta_i_0=true) /\ (ta_i_1=false).
Have: (Init_i_0=true) /\ (i_1 = 0).
Have: (Init_i_1=true) /\ ((1 + i_1) = i_2).
Have: i_2 <= 10.
Have: i <= 10.
......@@ -428,8 +428,8 @@ zloop sequent:
Assume {
Have: foo_0 = 42.
Have: 0 <= x.
Have: (Init_i_0=false) /\ (ta_i_0=true) /\ (ta_i_1=false).
Have: i = 0.
Have: (ta_i_0=true) /\ (ta_i_1=false).
Have: (Init_i_0=true) /\ (i = 0).
Have: (Init_i_1=true) /\ ((1 + i) = i_1).
Have: i_1 <= 10.
Have: i_2 <= 10.
......@@ -448,8 +448,8 @@ zloop sequent:
Assume {
Have: foo_0 = 42.
Have: 0 <= x.
Have: (Init_i_0=false) /\ (ta_i_0=true) /\ (ta_i_1=false).
Have: i_1 = 0.
Have: (ta_i_0=true) /\ (ta_i_1=false).
Have: (Init_i_0=true) /\ (i_1 = 0).
Have: (Init_i_1=true) /\ ((1 + i_1) = i_2).
Have: i_2 <= 10.
Have: i <= 10.
......@@ -467,8 +467,8 @@ zloop sequent:
Assume {
Have: foo_0 = 42.
Have: 0 <= x.
Have: (Init_i_0=false) /\ (ta_i_0=true) /\ (ta_i_1=false).
Have: i_1 = 0.
Have: (ta_i_0=true) /\ (ta_i_1=false).
Have: (Init_i_0=true) /\ (i_1 = 0).
Have: (Init_i_1=true) /\ ((1 + i_1) = i_2).
Have: i_2 <= 10.
Have: i <= 10.
......@@ -485,8 +485,8 @@ zloop sequent:
Assume {
Have: foo_0 = 42.
Have: 0 <= x.
Have: (Init_i_0=false) /\ (ta_i_0=true) /\ (ta_i_1=false).
Have: i_1 = 0.
Have: (ta_i_0=true) /\ (ta_i_1=false).
Have: (Init_i_0=true) /\ (i_1 = 0).
Have: (Init_i_1=true) /\ ((1 + i_1) = i).
}
Prove: i <= 10.
......@@ -500,8 +500,8 @@ zloop sequent:
Assume {
Have: foo_0 = 42.
Have: 0 <= x.
Have: (Init_i_0=false) /\ (ta_i_0=true) /\ (ta_i_1=false).
Have: i_1 = 0.
Have: (ta_i_0=true) /\ (ta_i_1=false).
Have: (Init_i_0=true) /\ (i_1 = 0).
Have: (Init_i_1=true) /\ ((1 + i_1) = i_2).
Have: i_2 <= 10.
Have: i_3 <= 10.
......@@ -520,8 +520,8 @@ zloop sequent:
Assume {
Have: foo_0 = 42.
Have: 0 <= x.
Have: (Init_i_0=false) /\ (ta_i_0=true) /\ (ta_i_1=false).
Have: i = 0.
Have: (ta_i_0=true) /\ (ta_i_1=false).
Have: (Init_i_0=true) /\ (i = 0).
Have: (Init_i_1=true) /\ ((1 + i) = i_1).
Have: i_1 <= 10.
Have: i_2 <= 10.
......
void l_int(void){
int x = 1 ;
//@ assert SUCCS: x == 1;
//@ assert SUCCS: \initialized(&x);
//@ check FAILS: \false ;
}
void l_array(void){
int x[3] = { 0 } ;
//@ assert SUCCS: x[0] == x[1] == x[2] == 0 ;
//@ assert SUCCS: \initialized(&x);
//@ check FAILS: \false ;
}
typedef struct { int x ; char t[2] ; } S;
void l_struct(void){
S s = { 0 };
//@ assert SUCCS: s.x == s.t[0] == s.t[1] == 0 ;
//@ assert SUCCS: \initialized(&s);
//@ check FAILS: \false ;
}
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/initialized_local_init.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function l_array
------------------------------------------------------------
Goal Assertion 'SUCCS' (file tests/wp_acsl/initialized_local_init.i, line 9):
Let x_1 = x[1].
Let x_2 = x[2].
Assume {
Type: is_sint32(x_1) /\ is_sint32(x_2).
(* Initializer *)
Init: x[0] = 0.
(* Initializer *)
Init: forall i : Z. ((0 < i) -> ((i <= 2) -> (x[i] = 0))).
}
Prove: (x_1 = 0) /\ (x_2 = 0) /\ (x_2 = x_1).
------------------------------------------------------------
Goal Assertion 'SUCCS' (file tests/wp_acsl/initialized_local_init.i, line 10):
Assume {
(* Goal *)
When: (0 <= i) /\ (i <= 2).
(* Initializer *)
Init: (Init_x_0[0]=true).
(* Initializer *)
Init: x[0] = 0.
(* Initializer *)
Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 2) -> (Init_x_0[i_1]=true))).
(* Initializer *)
Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 2) -> (x[i_1] = 0))).
(* Assertion 'SUCCS' *)
Have: (x[1] = 0) /\ (x[2] = 0).
}
Prove: (Init_x_0[i]=true).
------------------------------------------------------------
Goal Check 'FAILS' (file tests/wp_acsl/initialized_local_init.i, line 11):
Assume {
(* Initializer *)
Init: x[0] = 0.
(* Initializer *)
Init: forall i : Z. ((0 < i) -> ((i <= 2) -> (x[i] = 0))).
(* Assertion 'SUCCS' *)
Have: (x[1] = 0) /\ (x[2] = 0).
}
Prove: false.
------------------------------------------------------------
------------------------------------------------------------
Function l_int
------------------------------------------------------------
Goal Assertion 'SUCCS' (file tests/wp_acsl/initialized_local_init.i, line 3):
Prove: true.
------------------------------------------------------------
Goal Assertion 'SUCCS' (file tests/wp_acsl/initialized_local_init.i, line 4):
Prove: true.
------------------------------------------------------------
Goal Check 'FAILS' (file tests/wp_acsl/initialized_local_init.i, line 5):
Prove: false.
------------------------------------------------------------
------------------------------------------------------------
Function l_struct
------------------------------------------------------------
Goal Assertion 'SUCCS' (file tests/wp_acsl/initialized_local_init.i, line 16):
Prove: true.
------------------------------------------------------------
Goal Assertion 'SUCCS' (file tests/wp_acsl/initialized_local_init.i, line 17):
Prove: true.
------------------------------------------------------------
Goal Check 'FAILS' (file tests/wp_acsl/initialized_local_init.i, line 18):
Prove: false.
------------------------------------------------------------
......@@ -251,9 +251,6 @@ Assume {
is_sint8_chunk(Mchar_0).
Type: IsS1_X(r) /\ is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint8_chunk(Mchar_0).
(* Block In *)
Have: ({ Init_F1_X_a = false ; Init_F1_X_b = false ; Init_F1_X_c = false }) =
Init_r_0.
}
Prove: valid_rd(Malloc_0, p, 3).
......@@ -273,9 +270,6 @@ Assume {
is_sint8_chunk(Mchar_0).
Type: IsS1_X(r) /\ is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint8_chunk(Mchar_0).
(* Block In *)
Have: ({ Init_F1_X_a = false ; Init_F1_X_b = false ; Init_F1_X_c = false }) =
Init_r_0.
(* Assertion 'rte,mem_access' *)
Have: valid_rd(Malloc_0, p, 3).
(* Initializer *)
......
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/initialized_local_init.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 9 goals scheduled
[wp] [Qed] Goal typed_l_int_assert_SUCCS : Valid
[wp] [Qed] Goal typed_l_int_assert_SUCCS_2 : Valid
[wp] [Alt-Ergo] Goal typed_l_int_check_FAILS : Unsuccess
[wp] [Alt-Ergo] Goal typed_l_array_assert_SUCCS : Valid (missing cache)
[wp] [Alt-Ergo] Goal typed_l_array_assert_SUCCS_2 : Valid (missing cache)
[wp] [Alt-Ergo] Goal typed_l_array_check_FAILS : Unsuccess
[wp] [Qed] Goal typed_l_struct_assert_SUCCS : Valid
[wp] [Qed] Goal typed_l_struct_assert_SUCCS_2 : Valid
[wp] [Alt-Ergo] Goal typed_l_struct_check_FAILS : Unsuccess
[wp] Proved goals: 6 / 9
Qed: 4
Alt-Ergo: 2 (unsuccess: 3)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
l_int 2 - 3 66.7%
l_array - 2 3 66.7%
l_struct 2 - 3 66.7%
------------------------------------------------------------
Markdown is supported
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