From bf35135ed076c5aef42e08fbf0dc9de7e041c893 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 14 Oct 2020 08:27:16 +0200
Subject: [PATCH] [wp] Do not lose goal on call computation failure
---
src/plugins/wp/cfgWP.ml | 2 +-
src/plugins/wp/tests/wp/bad_cast_call.i | 7 +++++++
.../wp/tests/wp/oracle/bad_cast_call.res.oracle | 16 ++++++++++++++++
.../wp/oracle_qualif/bad_cast_call.res.oracle | 16 ++++++++++++++++
4 files changed, 40 insertions(+), 1 deletion(-)
create mode 100644 src/plugins/wp/tests/wp/bad_cast_call.i
create mode 100644 src/plugins/wp/tests/wp/oracle/bad_cast_call.res.oracle
create mode 100644 src/plugins/wp/tests/wp/oracle_qualif/bad_cast_call.res.oracle
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index 93a00b75b28..f5006fd95ba 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -1187,7 +1187,7 @@ struct
match outcome with
| Warning.Result(warn , wp) -> { wp with vcs = add_warnings warn wp.vcs }
| Warning.Failed warn ->
- let v_post = do_assigns_everything ~stmt ~warn p_post.effects p_exit.vcs in
+ let v_post = do_assigns_everything ~stmt ~warn p_post.effects p_post.vcs in
let v_exit = do_assigns_everything ~stmt ~warn p_exit.effects p_exit.vcs in
let effects = Eset.union p_post.effects p_exit.effects in
let vcs = gmerge v_post v_exit in
diff --git a/src/plugins/wp/tests/wp/bad_cast_call.i b/src/plugins/wp/tests/wp/bad_cast_call.i
new file mode 100644
index 00000000000..96a0ef6a0e3
--- /dev/null
+++ b/src/plugins/wp/tests/wp/bad_cast_call.i
@@ -0,0 +1,7 @@
+char *m(void);
+
+void foo() {
+ char** pages = (void*)0;
+ pages = m();
+ /*@ assert MUST_FAIL: pages == (void*) 0; */
+}
diff --git a/src/plugins/wp/tests/wp/oracle/bad_cast_call.res.oracle b/src/plugins/wp/tests/wp/oracle/bad_cast_call.res.oracle
new file mode 100644
index 00000000000..a95bbd54e16
--- /dev/null
+++ b/src/plugins/wp/tests/wp/oracle/bad_cast_call.res.oracle
@@ -0,0 +1,16 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp/bad_cast_call.i (no preprocessing)
+[wp] Running WP plugin...
+[kernel:annot:missing-spec] tests/wp/bad_cast_call.i:3: Warning:
+ Neither code nor specification for function m, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
+[wp] tests/wp/bad_cast_call.i:5: Warning:
+ Cast with incompatible pointers types (source: sint8*) (target: char**)
+------------------------------------------------------------
+ Function foo
+------------------------------------------------------------
+
+Goal Assertion 'MUST_FAIL' (file tests/wp/bad_cast_call.i, line 6):
+Prove: null = pages_0.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/bad_cast_call.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/bad_cast_call.res.oracle
new file mode 100644
index 00000000000..b750c3303f5
--- /dev/null
+++ b/src/plugins/wp/tests/wp/oracle_qualif/bad_cast_call.res.oracle
@@ -0,0 +1,16 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp/bad_cast_call.i (no preprocessing)
+[wp] Running WP plugin...
+[kernel:annot:missing-spec] tests/wp/bad_cast_call.i:3: Warning:
+ Neither code nor specification for function m, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
+[wp] tests/wp/bad_cast_call.i:5: Warning:
+ Cast with incompatible pointers types (source: sint8*) (target: char**)
+[wp] 1 goal scheduled
+[wp] [Alt-Ergo] Goal typed_foo_assert_MUST_FAIL : Unsuccess
+[wp] Proved goals: 0 / 1
+ Alt-Ergo: 0 (unsuccess: 1)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ foo - - 1 0.0%
+------------------------------------------------------------
--
GitLab