Commit 16351b6f authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: fix Mlw_expr.eff_check

parent da42c225
......@@ -134,21 +134,17 @@ and vty_varmap = function
| VTvalue _ -> Mid.empty
let eff_check vars result e =
let check r =
if not (reg_occurs r vars) then
Loc.errorm "every external effect must be mentioned in specification"
in
let reset r u = match result with
(* FIXME: we must reset non-written subregions of written regions *)
| _ when u <> None -> Loc.errorm "abstract parameters cannot reset regions"
| VTvalue v when reg_occurs r v.vtv_vars -> ()
| _ -> check r
in
let check vars r = if not (reg_occurs r vars) then
Loc.errorm "every external effect must be mentioned in specification" in
let reset vars r u = check vars r; Util.option_iter (check vars) u in
let check = check vars in
Sreg.iter check e.eff_reads;
Sreg.iter check e.eff_writes;
Sreg.iter check e.eff_ghostr;
Sreg.iter check e.eff_ghostw;
Mreg.iter reset e.eff_resets
if not (Mreg.is_empty e.eff_resets) then
let reset = reset (vars_union vars (vty_vars result)) in
Mreg.iter reset e.eff_resets
let rec vta_check vars vta =
let add_arg vars pv = vars_union vars pv.pv_vtv.vtv_vars in
......
......@@ -881,12 +881,13 @@ let rec vta_filter varm vars vta =
(* reads and writes must come from the context,
resets may affect the regions in the result *)
let spec = spec_filter varm vars vta.vta_spec in
let vars = vars_union vars (vty_vars vty) in
let rst = vta.vta_spec.c_effect.eff_resets in
let rst = { eff_empty with eff_resets = rst } in
let rst = (eff_filter vars rst).eff_resets in
let eff = { spec.c_effect with eff_resets = rst } in
let spec = { spec with c_effect = eff } in
let spec = if Mreg.is_empty rst then spec else
let vars = vars_union vars (vty_vars vty) in
let rst = { eff_empty with eff_resets = rst } in
let rst = (eff_filter vars rst).eff_resets in
let eff = { spec.c_effect with eff_resets = rst } in
{ spec with c_effect = eff } in
vty_arrow_unsafe vta.vta_args ~ghost:vta.vta_ghost ~spec vty
let vta_filter varm vta =
......
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