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

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



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? we might need to mark all the generated 
> Why3 code as ghost then.
>
>
I like the idea of marking all our generated code as ghost. Maybe it 
would solve some of our problems. To be investigated.

-- 
Claire

-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20180726/d2ee2024/attachment-0001.html>


More information about the Why3-club mailing list