[Why3-club] [Q612-030] adapt SPARK to Why3 1.0.0

François Bobot francois.bobot at cea.fr
Wed Jul 25 18:59:07 CEST 2018


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




More information about the Why3-club mailing list