Commit 263043a0 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

fastwp: handle incomplete exceptional postcondition in "abstract"

Submitted by Johannes Kanig
parent 88d57a55
...@@ -1522,6 +1522,17 @@ and fast_wp_desc (env : wp_env) (s : Subst.t) (r : res_type) (e : expr) ...@@ -1522,6 +1522,17 @@ and fast_wp_desc (env : wp_env) (s : Subst.t) (r : res_type) (e : expr)
let xpost = Mexn.map (fun p -> let xpost = Mexn.map (fun p ->
{ s = wp1.post.s; { s = wp1.post.s;
ne = p }) spec.c_xpost in ne = p }) spec.c_xpost in
(* We allow the xpost of the "abstract" to be incomplete; we fill in the
holes here *)
let xpost =
Mexn.fold (fun ex { ne = post; s = s } acc ->
if Mexn.mem ex acc then acc
else
let post =
{ ne = create_post (Mexn.find ex xresult) post;
s = s } in
Mexn.add ex post acc)
wp1.exn xpost in
let abstr_post = { s = wp1.post.s; ne = spec.c_post } in let abstr_post = { s = wp1.post.s; ne = spec.c_post } in
let post, xpost = let post, xpost =
adapt_post_to_state_pair env s r abstr_post xpost in adapt_post_to_state_pair env s r abstr_post xpost in
......
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