On Mon, 15 Apr 2019, Jean-Christophe Filliatre wrote:
> Hi Julia,
>
> > Couldn't the extraction just leave undefined things as undefined?
>
> You can use the --modular option of Why3's extraction for this purpose.
>
> Move your undefined function(s) to a separate module, say module X in
> file a
Hi Julia,
> Couldn't the extraction just leave undefined things as undefined?
You can use the --modular option of Why3's extraction for this purpose.
Move your undefined function(s) to a separate module, say module X in
file a.mlw, and then extract whatever other file/modules using A, say
b.mlw,
On Sun, 14 Apr 2019, Mario Pereira wrote:
>
> Hi,
>
> In that case, I believe you need a custom driver to map your [random_int]
> function to some OCaml code. In the case of function [random_int63] from the
> Why3 standard library, we have the following line in the ocaml64 driver:
>
> syntax
Hi,
In that case, I believe you need a custom driver to map your
[random_int] function to some OCaml code. In the case of function
[random_int63] from the Why3 standard library, we have the following
line in the ocaml64 driver:
syntax val random_int63 "Random.int %1"
This makes every o
On Sun, 14 Apr 2019, Mario Pereira wrote:
>
> Hi Julia,
>
> Can you please check if last commit (62c99f) fixes your extraction problem?
I think it is ok. It doesn't actually work, because I have a function
random_int that has no definition, but it doesn't give the error I was
getting previousl
Hi Julia,
Can you please check if last commit (62c99f) fixes your extraction problem?
Thank you in advance.
Best regards
--
Mário
Le 12/04/19 à 22:34, Julia Lawall a écrit :
On Fri, 12 Apr 2019, Jean-Christophe Filliatre wrote:
I think I managed to reproduce Julia's problem with a small in
