Hi Claire, Le 25/07/2018 à 17:31, Claire Dross a écrit : > I have been trying to adapt the spark tool to use the new Why3 release. I just finished doing it for Frama-c.
> I cannot say how it is going yet, I still have a long way to go, but I > already have some questions: > > - the "no inlining" and "lskept" metas seem to have disappear, did > they changed names or are they completely removed? - The "inline : no" became "inline:no". - I think, not sure, "lskept" is now "encoding:lskept". - The command `bin/why3 --list-metas` is handy for finding the new name. - I use also `git log --patch -S "inline : no"` to find when it has been modified. > - labels "..." are not accepted anymore. By looking at the parser, I > have replaced them with [@...], is this correct? (BTW, I am really > missing the Language Reference section of the LRM, any chance there is a > draft I can use somewhere?) It is correct. Appendix A.1.1 lists some syntax changes. > > I also found 2 cases of constructs which were accepted before but are > not anymore: > > - We can no longer ignore a non unit value: > let main () = 15; () > >> Cannot cast an integer literal to type unit > - Conversion to int of range types is ghost: > type tt = < range 1 5 > > let function to_rep (x : tt) : int = (tt'int x) > >> Function to_rep must be explicitly marked ghost > > Is it an oversight or were they removed on purpose? I will let someone else answer this part ;). Best, -- François _______________________________________________ Why3-club mailing list [email protected] https://lists.gforge.inria.fr/mailman/listinfo/why3-club
