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 complet
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 inlini
On 25 July 2018 at 17:31, Claire Dross wrote:
> 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
-- Andrei Paskevich (2018-07-25)
> This is also on purpose: the tt'int operation is used for
> specification purposes, if you make it non-ghost, you would need to
> link the extracted code with an arbitrary-precision arithmetic
> library.
so type "int" is also ghost? we might need to mark all the
On 25 July 2018 at 21:55, Yannick Moy wrote:
>> This is also on purpose: the tt'int operation is used for
>> specification purposes, if you make it non-ghost, you would need to
>> link the extracted code with an arbitrary-precision arithmetic
>> library.
>
> so type "int" is also ghost? we might n
Thanks Andrei for your answers.
Le 25/07/2018 à 21:51, Andrei Paskevich a écrit :
On 25 July 2018 at 17:31, Claire Dross wrote:
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 qu
-- Claire Dross (2018-07-26)
> Unfortunately, it seems that the modifications, if they make whyml better for
> code extraction, and probably a better language to program with directly,
> seem to make it more complicated to use as an intermediate language...
That's not desirable. If indeed Why3
On 25/07/2018, Yannick Moy wrote:
-- Andrei Paskevich (2018-07-25)
This is also on purpose: the tt'int operation is used for
specification purposes, if you make it non-ghost, you would need to
link the extracted code with an arbitrary-precision arithmetic
library.
so type "int" is also ghost
On 26 July 2018 at 09:09, Claire Dross wrote:
> Thanks Andrei for your answers.
>
> Le 25/07/2018 à 21:51, Andrei Paskevich a écrit :
>>
>> On 25 July 2018 at 17:31, Claire Dross wrote:
>>>
>>> I have been trying to adapt the spark tool to use the new Why3 release. I
>>> cannot say how it is goin
On 25 July 2018 at 17:31, Claire Dross wrote:
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
-- Claire Dross (2018-07-26)
No, the polymorphism encoding didn't change at all, so everything
should still be there, see François' reply.
>
> I don't see his reply, were is it? On Why3 list?
yes to why3-club@
___
Why3-club mailing list
Why3-
It has been only (less than?) one day since the SPARK team tried to
use Why3 master: perhaps there should be more thinking about the
possible workarounds before trying to change anything in Why3.
I think everybody agrees with that, and no changes were asked. Thanks
for clarifying though.
-
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 g
13 matches
Mail list logo
