[Why3-club] [Q612-030] adapt SPARK to Why3 1.0.0
francois.bobot at cea.fr
Wed Jul 25 18:59:07 CEST 2018
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 ;).
More information about the Why3-club