Merge branch 'fix/wp/goal-loss-on-call-with-bad-cast' into 'master'

[wp] Do not lose goal on call computation failure

Closes #805

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

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

src/plugins/wp/tests/wp/bad_cast_call.i

+char *m(void);
+
+void foo() {
+	char** pages = (void*)0;
+	pages = m();
+	/*@ assert MUST_FAIL: pages == (void*) 0; */
+}

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

+# 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.
+
+------------------------------------------------------------

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

+# 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%
+------------------------------------------------------------