[Why3-club] [Q612-030] adapt SPARK to Why3 1.0.0
dross at adacore.com
Wed Jul 25 17:31:08 CEST 2018
Hi Why3 team,
I have been trying to adapt the spark tool to use the new Why3 release.
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?
- 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?)
I also found 2 cases of constructs which were accepted before but are
- 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?
Thanks for your help,
More information about the Why3-club