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