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

Yannick Moy moy at adacore.com
Wed Jul 25 21:55:12 CEST 2018


-- 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.
--
Yannick Moy, Senior Software Engineer, AdaCore



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20180725/abe67b15/attachment-0001.html>


More information about the Why3-club mailing list