Thank you so much :)
I will take a lot at it during the week-end.
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:
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,
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 fail
On Fri, 12 Apr 2019, 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
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 b
On Fri, 12 Apr 2019, Mario Pereira wrote:
> Hi,
>
> Do you have a small example on which this happens?
No... Only a huge one. Do you have any suggestions of what to look for?
My functions return tuples that contain only ghost values, that I then
ignore, a was suggested earlier in this thread.
Hi,
Do you have a small example on which this happens?
Best regards
--
Mário
Le 12/04/19 à 16:43, Julia Lawall a écrit :
why3 extract is tripping on the assert in the following code (MaskGhost
case):
(* remove ghost components from tuple, using mask *)
(* TODO : completely remove this f
why3 extract is tripping on the assert in the following code (MaskGhost
case):
(* remove ghost components from tuple, using mask *)
(* TODO : completely remove this function *)
let visible_of_mask m sl = match m with
| MaskGhost-> assert false (* FIXME ? *)
| MaskVisible -> sl
