GitLab

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.