[wp] non-regression test for issue pub. 49

src/plugins/wp/tests/wp_bts/issue_pub_49.i

+/*
+  Postcondition postcs of function caller1 is proven (fixed value for codeCursor) while codeCursor may be updated in function is_class.
+  Similar issue for caller2.
+  Hint: proof not achieved when instruction at label_useless_cond is removed as in caller3.
+  Hint: proof not achieved when t3 is not declared in the block as in caller4.
+  Used command to run the proof:  
+    frama-c-gui assigns_postconditions.c -wp -wp-check-memory-model -wp-rte 
+*/
+
+
+
+int codeCursor;
+
+/*@ 
+  assigns codeCursor; 
+*/
+int is_class(void){
+  if (codeCursor < 10)
+    codeCursor++;
+  return 0;
+}
+
+
+/*@ 
+  assigns codeCursor; 
+  ensures postcs: codeCursor == \old(codeCursor);
+*/
+int caller1(void){
+  int t1=1;
+  int t2=0;
+  int t3;
+  
+  label_useless_cond: if (t1 == 7) return 1;
+  
+  label_cond_1: if (t2 == 0) {int t3 = is_class(); return t3;}
+  //label_cond_2:if (t2 == 0) {t3 = is_class(); return t3;} 
+  else return is_class();
+}
+
+
+/*@ 
+  assigns codeCursor; 
+  ensures postcs: codeCursor == \old(codeCursor);
+*/
+int caller2(void){
+  int t1=1;
+  int t2=0;
+  int t3;
+  
+  label_useless_cond: if (t1 == 7) return 1;
+  
+  label_cond_1: if (t2 == 0) {return is_class();}
+  //label_cond_2:if (t2 == 0) {t3 = is_class(); return t3;} 
+  else return is_class();
+}
+
+
+/*@ 
+  assigns codeCursor; 
+  ensures postcs: codeCursor == \old(codeCursor);
+*/
+int caller3(void){
+  int t1=1;
+  int t2=0;
+  int t3;
+
+  //label_useless_cond: if (t1 == 7) return 1;
+   
+  label_cond_1: if (t2 == 0) {int t3 = is_class(); return t3;}
+  //label_cond_2:if (t2 == 0) {t3 = is_class(); return t3;} 
+  else return is_class();
+}
+
+
+/*@ 
+  assigns codeCursor; 
+  ensures postcs: codeCursor == \old(codeCursor);
+*/
+int caller4(void){
+  int t1=1;
+  int t2=0;
+  int t3;
+  
+  label_useless_cond: if (t1 == 7) return 1;
+  
+  //label_cond_1: if (t2 == 0) {int t3 = is_class(); return t3;}
+  label_cond_2:if (t2 == 0) {t3 = is_class(); return t3;} 
+  else return is_class();
+}
+

src/plugins/wp/tests/wp_bts/oracle/issue_pub_49.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_pub_49.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function caller1
+------------------------------------------------------------
+
+Goal Post-condition 'postcs' in 'caller1':
+Assume { Type: is_sint32(codeCursor_1) /\ is_sint32(codeCursor_0). }
+Prove: codeCursor_0 = codeCursor_1.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 25) in 'caller1':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 25) in 'caller1' (1/6):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 25) in 'caller1' (2/6):
+Effect at line 33
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 25) in 'caller1' (3/6):
+Call Result at line 35
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 25) in 'caller1' (4/6):
+Effect at line 35
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 25) in 'caller1' (5/6):
+Call Result at line 37
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 25) in 'caller1' (6/6):
+Effect at line 37
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function caller2
+------------------------------------------------------------
+
+Goal Post-condition 'postcs' in 'caller2':
+Assume { Type: is_sint32(codeCursor_1) /\ is_sint32(codeCursor_0). }
+Prove: codeCursor_0 = codeCursor_1.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 42) in 'caller2':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 42) in 'caller2' (1/6):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 42) in 'caller2' (2/6):
+Effect at line 50
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 42) in 'caller2' (3/6):
+Call Result at line 52
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 42) in 'caller2' (4/6):
+Effect at line 52
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 42) in 'caller2' (5/6):
+Call Result at line 54
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 42) in 'caller2' (6/6):
+Effect at line 54
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function caller3
+------------------------------------------------------------
+
+Goal Post-condition 'postcs' in 'caller3':
+Assume { Type: is_sint32(codeCursor_1) /\ is_sint32(codeCursor_0). }
+Prove: codeCursor_0 = codeCursor_1.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 59) in 'caller3':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 59) in 'caller3' (1/5):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 59) in 'caller3' (2/5):
+Call Result at line 69
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 59) in 'caller3' (3/5):
+Effect at line 69
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 59) in 'caller3' (4/5):
+Call Result at line 71
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 59) in 'caller3' (5/5):
+Effect at line 71
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function caller4
+------------------------------------------------------------
+
+Goal Post-condition 'postcs' in 'caller4':
+Assume { Type: is_sint32(codeCursor_1) /\ is_sint32(codeCursor_0). }
+Prove: codeCursor_0 = codeCursor_1.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 76) in 'caller4':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 76) in 'caller4' (1/6):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 76) in 'caller4' (2/6):
+Effect at line 84
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 76) in 'caller4' (3/6):
+Call Result at line 87
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 76) in 'caller4' (4/6):
+Effect at line 87
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 76) in 'caller4' (5/6):
+Call Result at line 88
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 76) in 'caller4' (6/6):
+Effect at line 88
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function is_class
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 15) in 'is_class' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_bts/issue_pub_49.i, line 15) in 'is_class' (2/2):
+Effect at line 20
+Prove: true.
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_bts/oracle_qualif/issue_pub_49.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_pub_49.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 33 goals scheduled
+[wp] [Qed] Goal typed_is_class_assigns_part1 : Valid
+[wp] [Qed] Goal typed_is_class_assigns_part2 : Valid
+[wp] [Alt-Ergo] Goal typed_caller1_ensures_postcs : Unsuccess
+[wp] [Qed] Goal typed_caller1_assigns_exit : Valid
+[wp] [Qed] Goal typed_caller1_assigns_normal_part1 : Valid
+[wp] [Qed] Goal typed_caller1_assigns_normal_part2 : Valid
+[wp] [Qed] Goal typed_caller1_assigns_normal_part3 : Valid
+[wp] [Qed] Goal typed_caller1_assigns_normal_part4 : Valid
+[wp] [Qed] Goal typed_caller1_assigns_normal_part5 : Valid
+[wp] [Qed] Goal typed_caller1_assigns_normal_part6 : Valid
+[wp] [Alt-Ergo] Goal typed_caller2_ensures_postcs : Unsuccess
+[wp] [Qed] Goal typed_caller2_assigns_exit : Valid
+[wp] [Qed] Goal typed_caller2_assigns_normal_part1 : Valid
+[wp] [Qed] Goal typed_caller2_assigns_normal_part2 : Valid
+[wp] [Qed] Goal typed_caller2_assigns_normal_part3 : Valid
+[wp] [Qed] Goal typed_caller2_assigns_normal_part4 : Valid
+[wp] [Qed] Goal typed_caller2_assigns_normal_part5 : Valid
+[wp] [Qed] Goal typed_caller2_assigns_normal_part6 : Valid
+[wp] [Alt-Ergo] Goal typed_caller3_ensures_postcs : Unsuccess
+[wp] [Qed] Goal typed_caller3_assigns_exit : Valid
+[wp] [Qed] Goal typed_caller3_assigns_normal_part1 : Valid
+[wp] [Qed] Goal typed_caller3_assigns_normal_part2 : Valid
+[wp] [Qed] Goal typed_caller3_assigns_normal_part3 : Valid
+[wp] [Qed] Goal typed_caller3_assigns_normal_part4 : Valid
+[wp] [Qed] Goal typed_caller3_assigns_normal_part5 : Valid
+[wp] [Alt-Ergo] Goal typed_caller4_ensures_postcs : Unsuccess
+[wp] [Qed] Goal typed_caller4_assigns_exit : Valid
+[wp] [Qed] Goal typed_caller4_assigns_normal_part1 : Valid
+[wp] [Qed] Goal typed_caller4_assigns_normal_part2 : Valid
+[wp] [Qed] Goal typed_caller4_assigns_normal_part3 : Valid
+[wp] [Qed] Goal typed_caller4_assigns_normal_part4 : Valid
+[wp] [Qed] Goal typed_caller4_assigns_normal_part5 : Valid
+[wp] [Qed] Goal typed_caller4_assigns_normal_part6 : Valid
+[wp] Proved goals:   29 / 33
+  Qed:            29 
+  Alt-Ergo:        0  (unsuccess: 4)
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  is_class                  2        -        2       100%
+  caller1                   7        -        8      87.5%
+  caller2                   7        -        8      87.5%
+  caller3                   6        -        7      85.7%
+  caller4                   7        -        8      87.5%
+------------------------------------------------------------