Commit 472c9dab authored by Allan Blanchard's avatar Allan Blanchard

Merge branch 'feature/wp/precise-call-compilation-failure' into 'master'

More robust proof obligation generation

Closes #972

See merge request frama-c/frama-c!2904
parents 04fe5b44 2491f9b5
......@@ -755,11 +755,23 @@ struct
| Some exp ->
in_wenv wenv wp
begin fun env wp ->
let vr = L.result () in
let tr = L.return () in
let sigma = L.current env in
let returned = p_equal (C.result sigma tr vr) (C.return sigma tr exp) in
let vcs = gmap (assume_vc ~descr:"Return" ~stmt [returned]) wp.vcs in
let compile () =
let sigma = L.current env in
let vr = L.result () in
let tr = L.return () in
p_equal (C.result sigma tr vr) (C.return sigma tr exp) in
let outcome = Warning.catch
~severe:false ~effect:"Result value discarded (unknown)"
compile () in
let warn, condition =
match outcome with
| Warning.Failed warn ->
warn , p_true
| Warning.Result(warn,condition) ->
warn , condition in
let vcs = gmap (
assume_vc ~descr:"Return" ~stmt ~warn [condition]
) wp.vcs in
{ wp with vcs = vcs }
end
......@@ -1120,13 +1132,17 @@ struct
let cc_result call = match call.loc_result with
| None -> []
| Some(tr,obj,loc) ->
(* [LC,VP] : the C left unspecified where to compute the lv *)
(* [LC,BY] : lv computed before, like in Value Analysis *)
let vr = M.load call.seq_result.post obj loc in
let re = L.in_frame call.frame_post L.result () in
let te = L.in_frame call.frame_post L.return () in
let value = C.result call.sigma_pre tr re in
[ C.equal_typ tr vr (C.cast tr te (Val value)) ]
let handler () = [ p_true ] in
let compile () =
(* [LC,VP] : the C left unspecified where to compute the lv *)
(* [LC,BY] : lv computed before, like in Value Analysis *)
let vr = M.load call.seq_result.post obj loc in
let re = L.in_frame call.frame_post L.result () in
let te = L.in_frame call.frame_post L.return () in
let value = C.result call.sigma_pre tr re in
[ C.equal_typ tr vr (C.cast tr te (Val value)) ]
in
Warning.handle ~handler ~severe:false ~effect:"Hide \\result" compile ()
let cc_status f_caller f_callee =
p_equal
......
/*@ axiomatic Ax { predicate Kept reads \nothing ; } */
/*@ ensures Kept && \result == \null ; */
char *m(void);
void foo() {
char** pages = (void*)0;
pages = m();
/*@ assert MUST_FAIL: pages == (void*) 0; */
/*@ assert MUST_FAIL: pages == \null ; */
}
# 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
[kernel] tests/wp/bad_cast_call.i:6: Warning:
No code nor implicit assigns clause for function m, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] tests/wp/bad_cast_call.i:5: Warning:
[wp] tests/wp/bad_cast_call.i:8: 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):
Goal Assertion 'MUST_FAIL' (file tests/wp/bad_cast_call.i, line 9):
tests/wp/bad_cast_call.i:8: warning from Typed Model:
- Warning: Hide \result
Reason: Cast with incompatible pointers types (source: sint8*) (target: char**)
Assume { (* Call 'm' *) Have: P_Kept. }
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
[kernel] tests/wp/bad_cast_call.i:6: Warning:
No code nor implicit assigns clause for function m, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] tests/wp/bad_cast_call.i:5: Warning:
[wp] tests/wp/bad_cast_call.i:8: 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] [Alt-Ergo] Goal typed_foo_assert_MUST_FAIL : Unsuccess (Stronger)
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (unsuccess: 1)
------------------------------------------------------------
......
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