External provers broken with 19.0-beta1
ID0002437: This issue was created automatically from Mantis Issue 2437. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002437 | Frama-C | Kernel | public | 2019-05-20 | 2019-07-05 |
| Reporter | bpc | Assigned To | correnson | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | x86_64 GNU/Linux | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | Frama-C 19-Potassium |
Description :
External provers, with why3, look broken with 19.0-beta1 :
$ frama-c -wp -wp-prover why3:z3 swap.c [kernel] Parsing swap.c (with preprocessing) [wp] Warning: Missing RTE guards [wp] 4 goals scheduled [wp] [z3] Goal typed_swap_ensures_A : Unknown (Qed:3ms) (51ms) [wp] Proved goals: 3 / 4 Qed: 3 (0.38ms-0.63ms-0.77ms) Z3: 0 (unknown: 1)
Same problem using why3:cvc4-15 and why3:alt-ergo. With the "native" alt-ergo, no problem :
$ frama-c -wp -wp-prover alt-ergo swap.c [kernel] Parsing swap.c (with preprocessing) [wp] Warning: Missing RTE guards [wp] 4 goals scheduled [wp] Proved goals: 4 / 4 Qed: 3 (0.60ms-1ms-3ms) Alt-Ergo: 1 (11ms) (40)
Additional Information :
$ opam list
Packages matching: installed
Name # Installed # Synopsis
alt-ergo 2.3.0 The Alt-Ergo SMT prover alt-ergo-lib 2.3.0 The Alt-Ergo SMT prover library alt-ergo-parsers 2.3.0 The Alt-Ergo SMT prover parser library base-bigarray base base-num base Num library distributed with the OCaml compiler base-threads base base-unix base biniou 1.2.0 Binary data format designed for speed, safety, ease of use and backward compatibility as protocols evolve camlp5 7.06.10-g84ce6cc4 Preprocessor-pretty-printer of OCaml camlzip 1.07 Provides easy access to compressed files in ZIP, GZIP and JAR format conf-autoconf 0.1 Virtual package relying on autoconf installation conf-gmp 1 Virtual package relying on a GMP lib system installation conf-gnomecanvas 2 Virtual package relying on a Gnomecanvas system installation conf-graphviz 0.1 Virtual package relying on graphviz installation conf-gtksourceview 2 Virtual package relying on a GtkSourceView system installation conf-m4 1 Virtual package relying on m4 conf-perl 1 Virtual package relying on perl conf-pkg-config 1.1 Virtual package relying on pkg-config installation conf-python-2-7 1.0 Virtual package relying on Python-2.7 installation conf-which 1 Virtual package relying on which coq 8.9.0 Formal proof management system cppo 1.6.5 Equivalent of the C preprocessor for OCaml programs dune 1.9.3 Fast, portable and opinionated build system easy-format 1.3.1 High-level and functional interface to the Format module of the OCaml standard library frama-c 19.0.beta1 pinned to version 19.0.beta1 at git+https://github.com/Frama-C/Frama-C-snapshot.git#latest jbuilder transition This is a transition package, jbuilder is now named dune. Use the dune lablgtk 2.18.8 OCaml interface to GTK+ menhir 20181113 An LR(1) parser generator num 0 The Num library for arbitrary-precision integer and rational arithmetic ocaml 4.05.0 The OCaml compiler (virtual package) ocaml-config 1 OCaml Switch Configuration ocaml-system 4.05.0 The OCaml compiler (system version, from outside of opam) ocamlbuild 0.14.0 OCamlbuild is a build system with builtin rules to easily build most OCaml projects. ocamlfind 1.8.0 A library manager for OCaml ocamlgraph 1.8.8 A generic graph library for OCaml ocplib-simplex 0.4 A library implementing a simplex algorithm, in a functional style, for solving systems of linear inequalities and optimizing linear objective functions psmt2-frontend 0.2 A library to parse and type-check a conservative extension of the SMT-LIB 2 standard with prenex polymorphism seq 0.1 Compatibility package for OCaml's standard iterator type starting from 4.07. why3 1.2.0 Why3 environment for deductive program verification yojson 1.7.0 Yojson is an optimized parsing and printing library for the JSON format z3 4.8.4 Z3 solver zarith 1.7 Implements arithmetic and logical operations over arbitrary-precision integers