--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on June 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C fails to build on Debian



Hello,

Le jeu. 4 juin 2020 à 18:43, John Scott <jscott at posteo.net> a écrit :

>
> I'm not the maintainer, just a prospective user taking a look, but Frama-C
> hasn't been building from source in a while [1] and I couldn't find a bug
> for
> it. It fails with
> File "src/plugins/wp/ProverWhy3.ml", line 131, characters 29-45:
> 131 |   Why3.(Term.t_const Number.(const_of_big_int (BigInt.of_string
> (Z.to_string z)))) Why3.Ty.ty_int
> Error: Unbound value const_of_big_int
>
>
Thanks for the report. There is indeed a compatibility issue between
Frama-C 20.0 and Why3 1.3, which is fixed in the upcoming Frama-C 21.0
(currently available in beta) On the other hand, Frama-C 21.0 won't be
compatible with Why3 < 1.3

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile
-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200604/858aced2/attachment.html>