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

Claire Dross 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 
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?
Thanks for your help,


More information about the Why3-club mailing list