Hi François,
Le 25/07/2018 à 18:59, François Bobot a écrit :
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.
Thanks, that's what I was looking for.
- 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 saw this one, indeed.
--
Claire
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
