Merge branch 'fix/blanchard/wp/stmtcompiler-exits' into 'master'

[wp] fix statement compiler exits

See merge request frama-c/frama-c!4283

src/plugins/wp/StmtSemantics.ml

@@ -452,7 +452,7 @@ struct
                                     Clabels.post, post_normal_behavior] in
       let post_at_exit_behavior = Cfg.node () in
       let post_at_exit_env = env @* [Clabels.here, nassigns;
-                                     Clabels.post, post_at_exit_behavior] in
+                                     Clabels.exit, post_at_exit_behavior] in
       assume,
       sequence
         (fun env ip ->

src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle

@@ -3,7 +3,7 @@
 [kernel:CERT:MSC:37] stmtcompiler_test.i:136: Warning: 
   Body of function if_assert falls-through. Adding a return statement
 [wp] Running WP plugin...
-[kernel:annot:missing-spec] stmtcompiler_test.i:145: Warning: 
+[kernel:annot:missing-spec] stmtcompiler_test.i:167: Warning: 
   Neither code nor implicit assigns clause for function behavior1, generating default assigns from the prototype
 [wp] Warning: Missing RTE guards
 [wp] stmtcompiler_test.i:81: Warning: 
@@ -56,6 +56,19 @@ Prove: true.
 Goal Assertion (file stmtcompiler_test.i, line 6):
 Prove: true.
 
+------------------------------------------------------------
+------------------------------------------------------------
+  Function exits_and_ensures
+------------------------------------------------------------
+
+Goal Post-condition (file stmtcompiler_test.i, line 164) in 'exits_and_ensures':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Exit-condition (file stmtcompiler_test.i, line 165) in 'exits_and_ensures':
+Prove: true.
+
 ------------------------------------------------------------
 ------------------------------------------------------------
   Function if_assert
@@ -315,7 +328,7 @@ Prove: true.
 [Qed] Valid
 
 ------------------------------------------------------------
-[wp] stmtcompiler_test.i:145: Warning: void object
+[wp] stmtcompiler_test.i:167: Warning: void object
 new way
 main sequent: Assume { Have: foo_0 = 42. }
 Prove: foo_0 = 42.
@@ -325,7 +338,7 @@ Prove: true.
 [Qed] Valid
 
 ------------------------------------------------------------
-[wp] stmtcompiler_test.i:145: Warning: void object
+[wp] stmtcompiler_test.i:167: Warning: void object
 new way
 not_main sequent: Assume { Have: foo_1 = 42. }
 Prove: foo_0 = 42.
@@ -335,7 +348,7 @@ Prove: foo_0 = 42.
 [Qed] No Result
 
 ------------------------------------------------------------
-[wp] stmtcompiler_test.i:145: Warning: void object
+[wp] stmtcompiler_test.i:167: Warning: void object
 new way
 main_assigns_global sequent:
    Assume {
@@ -709,3 +722,21 @@ Prove: true.
 [Qed] Valid
 
 ------------------------------------------------------------
+[wp] stmtcompiler_test.i:167: Warning: void object
+[wp] stmtcompiler_test.i:167: Warning: void object
+new way
+exits_and_ensures sequent:
+   Assume {
+     Have: foo_1 = 42.
+     If foo_2 != 0
+     Then { Have: foo_2 = foo_3. Have: foo_0 = 0. }
+     If foo_2 = 0
+     Then { Have: foo_2 = foo_4. Have: foo_0 = 1. Have: foo_2 != 0. }
+   }
+Prove: foo_0 = 0.
+
+Goal Post-condition (file stmtcompiler_test.i, line 164) in 'exits_and_ensures':
+Prove: true.
+[Qed] Valid
+
+------------------------------------------------------------

src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle

@@ -3,12 +3,12 @@
 [kernel:CERT:MSC:37] stmtcompiler_test.i:136: Warning: 
   Body of function if_assert falls-through. Adding a return statement
 [wp] Running WP plugin...
-[kernel:annot:missing-spec] stmtcompiler_test.i:145: Warning: 
+[kernel:annot:missing-spec] stmtcompiler_test.i:167: Warning: 
   Neither code nor implicit assigns clause for function behavior1, generating default assigns from the prototype
 [wp] Warning: Missing RTE guards
 [wp] stmtcompiler_test.i:81: Warning: 
   Missing assigns clause (assigns 'everything' instead)
-[wp] 27 goals scheduled
+[wp] 29 goals scheduled
 [wp] [Valid] typed_empty_assert (Qed)
 [wp] [Valid] typed_one_assign_assert (Qed)
 [wp] [Valid] typed_one_if_assert (Qed)
@@ -36,8 +36,10 @@
 [wp] [Valid] typed_if_assert_assert_3 (Qed)
 [wp] [Unsuccess] typed_if_assert_assert_missing_return (Alt-Ergo) (Cached)
 [wp] [Valid] typed_compare_assert (Qed)
-[wp] Proved goals:   19 / 27
-  Qed:            18
+[wp] [Valid] typed_exits_and_ensures_ensures (Qed)
+[wp] [Valid] typed_exits_and_ensures_exits (Qed)
+[wp] Proved goals:   21 / 29
+  Qed:            20
   Alt-Ergo:        1
   Unsuccess:       8
 ------------------------------------------------------------
@@ -57,4 +59,5 @@
   behavior5                 -        -        1       0.0%
   if_assert                 1        1        4      50.0%
   compare                   1        -        1       100%
+  exits_and_ensures         2        -        2       100%
 ------------------------------------------------------------

src/plugins/wp/tests/wp/stmtcompiler_test.i

@@ -154,3 +154,22 @@ int compare(int a, int b, int c, int d) {
   /*@ assert (a < b) ==> r == 1; @*/
   return r;
 }
+
+/*@ exits \true ;
+    ensures \false ;
+    assigns \nothing ;
+*/
+void exit(int);
+
+/*@ ensures foo == 0 ;
+    exits   foo == 1 ;
+*/
+void exits_and_ensures(void){
+  if(foo){
+    foo = 0 ;
+    return ;
+  } else {
+    foo = 1 ;
+    exit(0) ;
+  }
+}