From fac2f5a8a18014251bbd7e7609c1eb588e91d829 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 4 Aug 2023 08:37:34 +0200
Subject: [PATCH] [wp] fix statement compiler exits
---
src/plugins/wp/StmtSemantics.ml | 2 +-
.../wp/oracle/stmtcompiler_test.res.oracle | 39 +++++++++++++++++--
.../stmtcompiler_test.res.oracle | 11 ++++--
src/plugins/wp/tests/wp/stmtcompiler_test.i | 19 +++++++++
4 files changed, 62 insertions(+), 9 deletions(-)
diff --git a/src/plugins/wp/StmtSemantics.ml b/src/plugins/wp/StmtSemantics.ml
index 91ea7945003..1ba5d765187 100644
--- a/src/plugins/wp/StmtSemantics.ml
+++ b/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 ->
diff --git a/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle b/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
index 91cb6e824e2..28c7c1c4f8a 100644
--- a/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
+++ b/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
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle
index ff79bc41656..d02ff1630dc 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle
+++ b/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%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test.i b/src/plugins/wp/tests/wp/stmtcompiler_test.i
index 35dda974887..13df6892a43 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test.i
+++ b/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) ;
+ }
+}
--
GitLab