[Why3-club] [Q612-030] adapt SPARK to Why3 1.0.0
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
> 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.
-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
More information about the Why3-club