Clone, writes and resets
The typing of this code raises Invalid_argument("Ity.eff_reset")
theory Effect
use ref.Ref
type t = { mutable a: ref int }
let resize (h: t) : unit
=
let r = ! (h.a) in
h.a <- ref r
let set (h: t) : unit
=
resize h;
h.a := 0
end
theory Clone
clone Effect
end
By looking at the code it seems that an invariant is broken (writes and resets are not disjoint?). The cty that fails:
(h:t) : ()
writes { (h.a:ref int @rho).contents, (h:t <ref int @rho> @rho1).a }
covers { h:t <ref int @rho> @rho1 }
resets { h.a:ref int @rho }