extraction of references
An update to a reference x <- e
is extracted (ocaml64) in two
different ways: Without using --modular
, the result is simply
x.contents <- e
. But when using --modular
, the field of the
reference is qualified as x.Why3__Ref.contents <- e
.
Is the latter intended, and is there a library that defines the module Why3__Ref? Or does somebody have a pointer where the builtin reference is substituted in the Why3 codebase?
(I am using the last week’s master branch of Why3.)
$ cat test.mlw
module Test
let ref x = ()
let f (y:unit) = x <- y
end
$ why3 extract -D ocaml64 -L . test.Test
let x = ref ()
let f (y: unit) : unit = x.contents <- y
$ why3 extract --modular -D ocaml64 -L . test.Test -o .
$ cat test__Test.ml
let x = ref ()
let f (y: unit) : unit = x.Why3__Ref.contents <- y