From c3b5cd6aa002957e35a9c047ddaa0ce6c0f53afb Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 23 Nov 2021 09:31:26 +0100
Subject: [PATCH] [wp] Fixes stmt assigns handling in CFG
---
src/plugins/wp/cfgAnnot.ml | 2 +-
src/plugins/wp/tests/wp/default-stmt-assigns.i | 4 ++++
.../wp/oracle/default-stmt-assigns.res.oracle | 14 ++++++++++++++
.../oracle_qualif/default-stmt-assigns.res.oracle | 14 ++++++++++++++
4 files changed, 33 insertions(+), 1 deletion(-)
create mode 100644 src/plugins/wp/tests/wp/default-stmt-assigns.i
create mode 100644 src/plugins/wp/tests/wp/oracle/default-stmt-assigns.res.oracle
create mode 100644 src/plugins/wp/tests/wp/oracle_qualif/default-stmt-assigns.res.oracle
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 930f3e43906..fd5b6e5a5c3 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -392,7 +392,7 @@ let get_stmt_assigns kf stmt =
) l s.spec_behavior
| _ -> l
end stmt []
- in if asgn = [] then [WpPropId.empty_assigns_info] else asgn
+ in if asgn = [] then [WpPropId.mk_stmt_any_assigns_info stmt] else asgn
(* -------------------------------------------------------------------------- *)
(* --- Code Assertions --- *)
diff --git a/src/plugins/wp/tests/wp/default-stmt-assigns.i b/src/plugins/wp/tests/wp/default-stmt-assigns.i
new file mode 100644
index 00000000000..e18bff86ffc
--- /dev/null
+++ b/src/plugins/wp/tests/wp/default-stmt-assigns.i
@@ -0,0 +1,4 @@
+void automaton_state_accessor() {
+ __asm__("");
+ //@ assert \false ;
+}
diff --git a/src/plugins/wp/tests/wp/oracle/default-stmt-assigns.res.oracle b/src/plugins/wp/tests/wp/oracle/default-stmt-assigns.res.oracle
new file mode 100644
index 00000000000..eed81d759ff
--- /dev/null
+++ b/src/plugins/wp/tests/wp/oracle/default-stmt-assigns.res.oracle
@@ -0,0 +1,14 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp/default-stmt-assigns.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] tests/wp/default-stmt-assigns.i:2: Warning:
+ Missing assigns clause (assigns 'everything' instead)
+------------------------------------------------------------
+ Function automaton_state_accessor
+------------------------------------------------------------
+
+Goal Assertion (file tests/wp/default-stmt-assigns.i, line 3):
+Prove: false.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/default-stmt-assigns.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/default-stmt-assigns.res.oracle
new file mode 100644
index 00000000000..67146a0bc6c
--- /dev/null
+++ b/src/plugins/wp/tests/wp/oracle_qualif/default-stmt-assigns.res.oracle
@@ -0,0 +1,14 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp/default-stmt-assigns.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] tests/wp/default-stmt-assigns.i:2: Warning:
+ Missing assigns clause (assigns 'everything' instead)
+[wp] 1 goal scheduled
+[wp] [Alt-Ergo] Goal typed_automaton_state_accessor_assert : Unsuccess
+[wp] Proved goals: 0 / 1
+ Alt-Ergo: 0 (unsuccess: 1)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ automaton_state_accessor - - 1 0.0%
+------------------------------------------------------------
--
GitLab