Skip to content
Snippets Groups Projects
Commit 8b6427f8 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Merge branch 'fix/wp/post-assigns' into 'master' 

[wp] fix post assigns

See merge request frama-c/frama-c!3100
parents d695bbbe f7f5aeda
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 190 additions and 40 deletions
src/plugins/wp/LogicCompiler.ml
+ 1
− 0
View file @ 8b6427f8
......@@ -220,6 +220,7 @@ struct
Clabels.init , init ;
Clabels.pre , seq.pre ;
Clabels.post , seq.post ;
Clabels.exit , seq.post ;
] ;
}
......
src/plugins/wp/cfgWP.ml
+ 16
− 6
View file @ 8b6427f8
......@@ -152,8 +152,15 @@ struct
(* -------------------------------------------------------------------------- *)
let pp_vc fmt vc =
Format.fprintf fmt "%a"
(Pcond.dump_bundle ~clause:"Context" ~goal:vc.goal) vc.hyps
if Wp_parameters.debug_atleast 2 then
begin
List.iter
(Format.fprintf fmt "Have @[<hov 2>%a@]@." F.pp_pred)
(Conditions.extract vc.hyps) ;
Format.fprintf fmt "Goal @[<hov 2>%a@]@]@." F.pp_pred vc.goal ;
end
else
Pcond.dump_bundle ~clause:"Context" ~goal:vc.goal fmt vc.hyps
let pp_vcs fmt vcs =
let k = ref 0 in
......@@ -1099,11 +1106,14 @@ struct
}
| Writes froms ->
let env = L.move_at env0 cenv.sigma_pre in
let assigned = L.in_frame cenv.frame_pre
(L.assigned_of_froms env) froms in
let vcs_post = do_assigns ~descr:"Call Effects" ~source:FromCall
let cc_region = L.assigned_of_froms env in
let vcs_post =
let assigned = L.in_frame cenv.frame_post cc_region froms in
do_assigns ~descr:"Call Effects" ~source:FromCall
~stmt cenv.seq_post ~assigned wpost.effects wpost.vcs in
let vcs_exit = do_assigns ~descr:"Exit Effects" ~source:FromCall
let vcs_exit =
let assigned = L.in_frame cenv.frame_exit cc_region froms in
do_assigns ~descr:"Exit Effects" ~source:FromCall
~stmt cenv.seq_exit ~assigned wexit.effects wexit.vcs in
let vcs_result =
match cenv.loc_result with
......
src/plugins/wp/tests/wp_acsl/assigned_initialized_memvar.i
+ 8
− 2
View file @ 8b6427f8
......@@ -31,7 +31,10 @@ void range(void){
*/
for(int i = 0; i < 10; ++i) s.a[i] = 0;
/*@ loop assigns CHECK: i, s.a[1 .. 4]; */
/*@
loop invariant CHECK: \initialized(&s);
loop assigns CHECK: i, s.a[1 .. 4];
*/
for(int i = 0; i < 10; ++i){
if(1 <= i && i <= 4) s.a[i] = 1 ;
}
......@@ -98,7 +101,10 @@ void descr(void){
*/
for(int i = 0; i < 10; ++i) s.a[i] = 0;
/*@ loop assigns CHECK: i, { s.a[i] | integer i ; i \in { 0, 2, 4 } }; */
/*@
loop invariant CHECK: \initialized(&s);
loop assigns CHECK: i, { s.a[i] | integer i ; i \in { 0, 2, 4 } };
*/
for(int i = 0; i < 10; ++i){
if(i == 0 || i == 2 || i == 4) s.a[i] = 1 ;
}
......
src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle
+ 101
− 22
View file @ 8b6427f8
......@@ -6,7 +6,7 @@
Function array
------------------------------------------------------------
Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 73):
Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 76):
Assume {
Have: 0 <= i.
Have: i <= 9.
......@@ -37,7 +37,7 @@ Prove: true.
Function comp
------------------------------------------------------------
Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 125):
Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 131):
Let a = Init_s_0.Init_F1_S_a.
Assume {
Have: 0 <= i.
......@@ -70,7 +70,7 @@ Prove: true.
Function descr
------------------------------------------------------------
Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 105):
Goal Preservation of Invariant 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 105):
Assume {
Type: is_sint32(i) /\ is_sint32(i_1).
(* Invariant *)
......@@ -83,8 +83,38 @@ Assume {
Have: ((s.F1_S_i) = 0) /\
(forall i_2 : Z. ((i_2 != 0) -> ((i_2 != 2) -> ((i_2 != 4) ->
((0 <= i_2) -> ((i_2 <= 9) -> ((s.F1_S_a)[i_2] = v_1[i_2]))))))).
(* Else *)
Have: 10 <= i_1.
(* Invariant 'CHECK' *)
Have: ((Init_s_1.Init_F1_S_i)=true) /\
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
((Init_s_1.Init_F1_S_a)[i_2]=true)))).
(* Then *)
Have: i_1 <= 9.
If i_1 = 0
Then {
Have: Init_s_1 = Init_s_2.
Have: ({ Init_s_2 with Init_F1_S_a = (Init_s_2.Init_F1_S_a)[0 <- true] }) =
Init_s_0.
}
Else {
Have: (Init_s_1 = Init_s_3) /\ (s = s_1).
If i_1 = 2
Then {
Have: (Init_s_3 = Init_s_4) /\ (s_1 = s_2).
Have: ({ Init_s_4 with Init_F1_S_a = (Init_s_4.Init_F1_S_a)[2 <- true]
}) = Init_s_0.
}
Else {
Have: (Init_s_3 = Init_s_5) /\ (s_1 = s_3).
If i_1 = 4
Then {
Have: Init_s_5 = Init_s_6.
Have: ({ Init_s_6 with
Init_F1_S_a = (Init_s_6.Init_F1_S_a)[4 <- true] }) =
Init_s_0.
}
Else { Have: Init_s_5 = Init_s_0. }
}
}
}
Prove: ((Init_s_0.Init_F1_S_i)=true) /\
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
......@@ -92,13 +122,34 @@ Prove: ((Init_s_0.Init_F1_S_i)=true) /\
------------------------------------------------------------
Goal Establishment of Invariant 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 105):
Assume {
Have: 0 <= i.
Have: i <= 9.
Type: is_sint32(i_1).
(* Invariant *)
Have: (0 <= i_1) /\ (i_1 <= 10) /\
(((0 < i_1) ->
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) -> (v[i_2]=true)))))).
(* Else *)
Have: 10 <= i_1.
}
Prove: (v[i]=true).
------------------------------------------------------------
Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 111):
Prove: true.
------------------------------------------------------------
Goal Loop assigns 'CHECK' (1/5):
Prove: true.
------------------------------------------------------------
Goal Loop assigns 'CHECK' (2/5):
Effect at line 102
Effect at line 108
Assume {
Type: is_sint32(i_2) /\ is_sint32(i_3).
(* Goal *)
......@@ -124,19 +175,19 @@ Prove: ((i != 0) /\ (i != 2) /\ (i != 4)) \/
------------------------------------------------------------
Goal Loop assigns 'CHECK' (3/5):
Effect at line 103
Effect at line 109
Prove: true.
------------------------------------------------------------
Goal Loop assigns 'CHECK' (4/5):
Effect at line 103
Effect at line 109
Prove: true.
------------------------------------------------------------
Goal Loop assigns 'CHECK' (5/5):
Effect at line 103
Effect at line 109
Prove: true.
------------------------------------------------------------
......@@ -144,7 +195,7 @@ Prove: true.
Function field
------------------------------------------------------------
Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 54):
Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 57):
Assume {
Have: 0 <= i.
Have: i <= 9.
......@@ -170,7 +221,7 @@ Prove: true.
Function index
------------------------------------------------------------
Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 89):
Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 92):
Assume {
Have: 0 <= i.
Have: i <= 9.
......@@ -196,7 +247,7 @@ Prove: true.
------------------------------------------------------------
Goal Loop assigns 'CHECK' (2/2):
Effect at line 87
Effect at line 90
Prove: true.
------------------------------------------------------------
......@@ -249,25 +300,53 @@ Prove: true.
Function range
------------------------------------------------------------
Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 38):
Goal Preservation of Invariant 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 35):
Let a = Init_s_0.Init_F1_S_a.
Assume {
Type: is_sint32(i) /\ is_sint32(i_1).
Type: is_sint32(i_1) /\ is_sint32(i).
(* Residual *)
When: i <= 4.
(* Residual *)
When: 0 < i.
(* Invariant *)
Have: (0 <= i) /\ (i <= 10) /\
(((0 < i) ->
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) -> (v[i_2]=true)))))).
Have: (0 <= i_1) /\ (i_1 <= 10) /\
(((0 < i_1) ->
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) -> (v[i_2]=true)))))).
(* Else *)
Have: 10 <= i.
Have: 10 <= i_1.
(* Loop assigns 'CHECK' *)
Have: ((s.F1_S_i) = 0) /\
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
(((i_2 <= 0) \/ (5 <= i_2)) -> ((s.F1_S_a)[i_2] = v_1[i_2]))))).
(* Invariant 'CHECK' *)
Have: ((Init_s_0.Init_F1_S_i)=true) /\
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) -> (a[i_2]=true)))).
(* Then *)
Have: i <= 9.
}
Prove: forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
(a[i <- true][i_2]=true))).
------------------------------------------------------------
Goal Establishment of Invariant 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 35):
Assume {
Have: 0 <= i.
Have: i <= 9.
Type: is_sint32(i_1).
(* Invariant *)
Have: (0 <= i_1) /\ (i_1 <= 10) /\
(((0 < i_1) ->
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) -> (v[i_2]=true)))))).
(* Else *)
Have: 10 <= i_1.
}
Prove: ((Init_s_0.Init_F1_S_i)=true) /\
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
((Init_s_0.Init_F1_S_a)[i_2]=true)))).
Prove: (v[i]=true).
------------------------------------------------------------
Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 41):
Prove: true.
------------------------------------------------------------
......@@ -277,7 +356,7 @@ Prove: true.
------------------------------------------------------------
Goal Loop assigns 'CHECK' (2/2):
Effect at line 36
Effect at line 39
Prove: true.
------------------------------------------------------------
src/plugins/wp/tests/wp_acsl/oracle/postassigns2.res.oracle 0 → 100644
+ 24
− 0
View file @ 8b6427f8
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/postassigns2.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function mess1
------------------------------------------------------------
Goal Exit-condition (file tests/wp_acsl/postassigns2.c, line 6) in 'mess1':
Prove: true.
------------------------------------------------------------
Goal Assigns (file tests/wp_acsl/postassigns2.c, line 7) in 'mess1':
Call Effect at line 10
Prove: true.
------------------------------------------------------------
Goal Assigns (file tests/wp_acsl/postassigns2.c, line 7) in 'mess1':
Call Effect at line 10
Prove: true.
------------------------------------------------------------
src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle
+ 12
− 8
View file @ 8b6427f8
......@@ -2,12 +2,14 @@
[kernel] Parsing tests/wp_acsl/assigned_initialized_memvar.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 22 goals scheduled
[wp] 26 goals scheduled
[wp] [Alt-Ergo] Goal typed_initialize_loop_invariant_CHECK_preserved : Valid
[wp] [Qed] Goal typed_initialize_loop_invariant_CHECK_established : Valid
[wp] [Alt-Ergo] Goal typed_initialize_check_CHECK : Valid
[wp] [Qed] Goal typed_initialize_loop_assigns : Valid
[wp] [Alt-Ergo] Goal typed_range_check_CHECK : Unsuccess
[wp] [Alt-Ergo] Goal typed_range_loop_invariant_CHECK_preserved : Valid
[wp] [Alt-Ergo] Goal typed_range_loop_invariant_CHECK_established : Valid
[wp] [Qed] Goal typed_range_check_CHECK : Valid
[wp] [Qed] Goal typed_range_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_range_loop_assigns_part2 : Valid
[wp] [Alt-Ergo] Goal typed_field_check_CHECK : Valid
......@@ -17,7 +19,9 @@
[wp] [Alt-Ergo] Goal typed_index_check_CHECK : Valid
[wp] [Qed] Goal typed_index_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_index_loop_assigns_part2 : Valid
[wp] [Alt-Ergo] Goal typed_descr_check_CHECK : Unsuccess
[wp] [Alt-Ergo] Goal typed_descr_loop_invariant_CHECK_preserved : Valid
[wp] [Alt-Ergo] Goal typed_descr_loop_invariant_CHECK_established : Valid
[wp] [Qed] Goal typed_descr_check_CHECK : Valid
[wp] [Qed] Goal typed_descr_loop_assigns_part1 : Valid
[wp] [Alt-Ergo] Goal typed_descr_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_descr_loop_assigns_part3 : Valid
......@@ -25,16 +29,16 @@
[wp] [Qed] Goal typed_descr_loop_assigns_part5 : Valid
[wp] [Alt-Ergo] Goal typed_comp_check_CHECK : Valid
[wp] [Qed] Goal typed_comp_loop_assigns : Valid
[wp] Proved goals: 20 / 22
Qed: 13
Alt-Ergo: 7 (unsuccess: 2)
[wp] Proved goals: 26 / 26
Qed: 15
Alt-Ergo: 11
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
initialize 2 2 4 100%
range 2 - 3 66.7%
range 3 2 5 100%
field 1 1 2 100%
array 1 1 2 100%
index 2 1 3 100%
descr 4 1 6 83.3%
descr 5 3 8 100%
comp 1 1 2 100%
------------------------------------------------------------
src/plugins/wp/tests/wp_acsl/oracle_qualif/postassigns2.res.oracle 0 → 100644
+ 14
− 0
View file @ 8b6427f8
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/postassigns2.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
[wp] [Qed] Goal typed_mess1_exits : Valid
[wp] [Qed] Goal typed_mess1_assigns_exit : Valid
[wp] [Qed] Goal typed_mess1_assigns_normal : Valid
[wp] Proved goals: 3 / 3
Qed: 3
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
mess1 3 - 3 100%
------------------------------------------------------------
src/plugins/wp/tests/wp_acsl/postassigns2.c 0 → 100644
+ 11
− 0
View file @ 8b6427f8
/*@ exits \false;
@ assigns *(message + (0 .. \at(*\old(size),Post) - 1)), *size;
*/
void receive1(unsigned char *message, unsigned int *size);
/*@ exits \false;
@ assigns *(message + (0 .. \at(*\old(size),Post) - 1)), *size;
*/
void mess1(unsigned char *message, unsigned int *size) {
receive1(message, size);
}
src/plugins/wp/wpStrategy.ml
+ 3
− 2
View file @ 8b6427f8
......@@ -438,8 +438,9 @@ let add_call_assigns_hyp acc kf_caller s ~called_kf l_post spec_opt =
let asgn = WpPropId.mk_stmt_any_assigns_info s in
add_assigns_any acc (AcallHyp called_kf) asgn
| Some pid ->
let kf = kf_caller in
let labels = NormAtLabels.labels_stmt_assigns_l ~kf s l_post in
ignore l_post ;
(* let kf = kf_caller in *)
let labels = NormAtLabels.labels_fct_assigns ~exit:false (* ~kf s l_post *) in
let assigns = NormAtLabels.preproc_assigns labels assigns in
let a_desc = WpPropId.mk_stmt_assigns_desc s assigns in
add_assigns acc (AcallHyp called_kf) pid a_desc
......
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