Commit bf35135e authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] Do not lose goal on call computation failure

parent ca9c296b
......@@ -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
......
char *m(void);
void foo() {
char** pages = (void*)0;
pages = m();
/*@ assert MUST_FAIL: pages == (void*) 0; */
}
# 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.
------------------------------------------------------------
# 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%
------------------------------------------------------------
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment