search

Frama-C / Frama-C-snapshot

Release snapshots of the Frama-C platform for source code analysis
http://frama-c.com
168 stars 38 forks source link

Have you ever tried Frama-C 20.0 #35

Closed aogrcs closed 4 years ago

aogrcs commented 4 years ago

I used Ubuntu 18.04.3 LTS for x86_64, opam 2.0.5, ocaml 4.05.0, why3 1.2.0, I found those problems: 1 Must install num, but it needs ocaml > 4.05 2 Which version of Coq should be used? Could anyone can give some help? Thanks

maroneze commented 4 years ago

There is unfortunately an issue with the num package in OCaml 4.05 (https://github.com/ocaml/opam-repository/issues/15441) and some specific versions of ocamlfind. For instance, ocamlfind 1.8.0 should work, ocamlfind 1.8.1 will not. If this is your ocamlfind version, you should normally be able to downgrade it to 1.8.0 without many issues. Note that num does not require OCaml > 4.05, it's just that the "pseudo-package" available in 4.05 has some quirks which cause issues with ocamlfind (at least that's how it's supposed to work, if there are no other issues we are unaware of).

Coq is officially deprecated in Frama-C 20 (hence why it is no longer listed on the known working configuration), but it should still work, roughly versions between 8.7 and 8.10.

aogrcs commented 4 years ago

"Coq is officially deprecated" means that Frama-C 20 uses why3 instead of Coq? Thanks

AllanBlanchard commented 4 years ago

In Frama-C 20, the default backend of WP for discharging the proof obligations is Why3. Native backends to Alt-Ergo and Coq are still there but deprecated as indicated in : http://frama-c.com/Changelog.html#Calcium-20.0 .

maroneze commented 4 years ago

It seems the issue is no longer active, so I'm closing it. If you have other issues just tell us.