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

Claire Dross dross at adacore.com
Thu Jul 26 11:09:20 CEST 2018


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



More information about the Why3-club mailing list