Clone problem when type has nested regions
Consider the following example:
module A
use seq.Seq, int.Int
type t = private { ghost mutable view: seq int }
val set (a: t) : unit
writes { a.view }
end
module B
use array.Array, int.Int, seq.Seq
type t = {
mutable data: A.array int;
ghost mutable view: seq int;
}
let set (a: t) : unit
= a.data[0] <- 42; a.view <- empty
end
module C
use B
clone A with type t, val set
end
I get an
Illegal instantiation for program function set:
unreferenced write effects in variables: a
error message because of the clone
in module C
.
I believe this is due to the fact that I am changing the elements of data
, hence touching the region of the array. In fact, if I change data
directly
let set (a: t) : unit
= a.data <- make 0 42; a.view <- empty
Why3 is happy.
Apparently, the problem is being detected at line 1179 of pmodule.ml
.
Given the recent updates on Why3 clone
mechanism, am I missing something here? Is there a proper way to specify the effect of set
in module A
in order to to pass this clone
, even when touching an inner region?
Note: this is a simplified example taken from the VOCaL library (cf, https://github.com/vocal-project/vocal/blob/master/vocal/proofs/why3/Vector_impl.mlw). Before merge request !347 (merged) we were able to clone function set
as is.