Control: forwarded -1 https://lists.gforge.inria.fr/pipermail/frama-c-discuss/2020-June/005823.html Control: tags -1 fixed-upstream > 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
I'm having trouble finding their VCS and what commit fixed this, but updating Frama-C to the beta should be sufficient. Unstable and testing already have Why3 >= 1.3.
signature.asc
Description: This is a digitally signed message part.
