--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on June 2020 ---
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>