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 ocurrence of [random_int63 x] to be mapped to
[Random.int x] in the final extracted code.
On the other hand, why not using one of the [random_int] functions from
the Why3 standard library? You would benefit from the existing
extraction drivers.
Best regards
--
Mário
Le 14/04/19 à 18:51, Julia Lawall a écrit :
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 previously.
julia
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 input file:
--------------------------------------------------
use int.Int
let f (x: int) : (ghost a: int, ghost b: int) =
x+1, x+2
let g (x: int) =
let a, b = f x in
()
--------------------------------------------------
It fails on the same assertion.
Thanks. My code has ghost on the let variables as well, but probbaly that
is not necessary.
julia
--
Jean-Christophe
On 4/12/19 6:24 PM, Mario Pereira wrote:
Do you have any suggestions of what to look for?
It would maybe be helpful for me to debug the problem to know if this
comes from pattern or type extraction.
When you are calling the extraction engine, could you please add to your
command line the following: "--debug stack_trace". We might be able to
track down which function is calling the [visible_of_mask] function.
Bests
--
Mário
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
