Commit 0c83ea5a authored by Andrei Paskevich's avatar Andrei Paskevich

invariants: projections for sum types are not safe

parent 4fdf05d5
......@@ -144,6 +144,12 @@ let mkR pjs =
(* TODO:
- do not collapse on Eif and Ecase in k_expr when the type is fragile
- projection application may require committing when the argument is
a C with unjoinable caps. We can and should detect such applications
inside specifications and produce appropriate commits. We should also
avoid creating such applications outside stop_split: Vc.name_regions
should NEVER use a projection with a fragile instantiated value type.
let add_var kn st v =
......@@ -888,12 +888,16 @@ let rec explore_paths kn aff regs t ity =
| Ityapp (s,tl,rl) -> explore_its kn aff regs t s tl rl
and explore_its kn aff regs t s tl rl =
let itd = find_its_defn kn s in
let sum = match itd.itd_constructors with
| _::_::_ -> true | _ -> false in
let isb = its_match_regs s tl rl in
let follow regs rs =
let ity = ity_full_inst isb rs.rs_cty.cty_result in
if sum && ity_fragile ity then regs (* danger *) else
let ls = ls_of_rs rs and ty = Some (ty_of_ity ity) in
explore_paths kn aff regs (t_app ls [t] ty) ity in
List.fold_left follow regs (find_its_defn kn s).itd_fields
List.fold_left follow regs itd.itd_fields
let name_regions kn wr dst =
let rec reg_aff_regs s r =
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