Commit 13585337 authored by Andrei Paskevich's avatar Andrei Paskevich

Mlw_ty: add a missing check to eff_full_inst

This fixes a soundness bug in WhyML typechecking.
See bench/programs/bad-typing/alias6.mlw for an example
of illegal alias that would go uncatched until now.
parent 693db5a7
module Bad
use import ref.Ref
let f (r: ref int) (x: 'a) : unit
ensures { x = old x /\ !r = 0 }
= r := 0
let bad ()
ensures { false }
= let r = ref 1 in
f r r
end
......@@ -703,6 +703,10 @@ let eff_full_inst sbs e =
let add_readonly r =
let r = Mreg.find r s in if Sreg.mem r wr then raise (IllegalAlias r) in
Sreg.iter add_readonly ro;
(* all type variables are instantiated outside wr *)
let check_tv _ ity = Sreg.iter (fun r ->
if reg_occurs r ity.ity_vars then raise (IllegalAlias r)) wr in
Mtv.iter check_tv sbs.ity_subst_tv;
(* calculate instantiated effect *)
let add_sreg r acc = Sreg.add (Mreg.find r s) acc in
let add_mreg r v acc =
......
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