On Mon, 8 Apr 2019, Raphael Rieu-Helft wrote:
> This should go well in the extracted code. "let x = f () in e", where x
> is ghost and f has observable side effects and return type "ghost int",
> will be extracted as "ignore f(); e".
OK, thanks for all the feedback.
julia
>
> Best,
> Raphaël
>
> On 08/04/2019 08:56, Julia Lawall wrote:
> > Actually, in my case, there is no real return value. So I kind of balk at
> > having to put a let, where there is no real return value. The calling
> > context doesn't care about the ghost, only the ensures. But in the
> > interest of progressing, I'll go with the let.
> _______________________________________________
> 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
