diff --git a/src/plugins/wp/LogicCompiler.ml b/src/plugins/wp/LogicCompiler.ml
index d2689aaefd605a6f52d8158f6d0807766fa581a4..238250786e76b477634e4d5700ceee7c10bf460a 100644
--- a/src/plugins/wp/LogicCompiler.ml
+++ b/src/plugins/wp/LogicCompiler.ml
@@ -220,6 +220,7 @@ struct
Clabels.init , init ;
Clabels.pre , seq.pre ;
Clabels.post , seq.post ;
+ Clabels.exit , seq.post ;
] ;
}
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index baa2652d9193dc016225f83dc1b0ee1533b09509..07f1496d8129ab4cc3a91ab30906151be9a540d0 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -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
diff --git a/src/plugins/wp/tests/wp_acsl/assigned_initialized_memvar.i b/src/plugins/wp/tests/wp_acsl/assigned_initialized_memvar.i
index c320c1273b969100934bdd4de54c5557ce74fe3c..7fc06531a4a98bdc28c75c9bf07b40e0dd9a1f33 100644
--- a/src/plugins/wp/tests/wp_acsl/assigned_initialized_memvar.i
+++ b/src/plugins/wp/tests/wp_acsl/assigned_initialized_memvar.i
@@ -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 ;
}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle
index a095737754b14ad8f09099416bd8bcf7bf91aa96..846c03241554a4f8ac8844069c0832abe60d4d8b 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle
@@ -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.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/postassigns2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/postassigns2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..53e8b93a4eb19154655eac272508d2554e39a0e8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/postassigns2.res.oracle
@@ -0,0 +1,24 @@
+# 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.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle
index de07c211f1cadf0a54fcd5e23b3f345692bdd7cb..756f8f52f89bb4a6eef18e377b0eb803cb2f6922 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle
@@ -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%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/postassigns2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/postassigns2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e6a7ddd408dd3858206a0e01bc153794d6b812d2
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/postassigns2.res.oracle
@@ -0,0 +1,14 @@
+# 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%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/postassigns2.c b/src/plugins/wp/tests/wp_acsl/postassigns2.c
new file mode 100644
index 0000000000000000000000000000000000000000..eedaa11f4c32e8ccf3f4e22881f01d2ea4cca500
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/postassigns2.c
@@ -0,0 +1,11 @@
+/*@ 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);
+}
diff --git a/src/plugins/wp/wpStrategy.ml b/src/plugins/wp/wpStrategy.ml
index 1385c9083189e6c15547c5e1bf5ca864367c5012..b4a4080208a94c700335156e1bf9ff75c49dee55 100644
--- a/src/plugins/wp/wpStrategy.ml
+++ b/src/plugins/wp/wpStrategy.ml
@@ -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