View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0002437 | Frama-C | Kernel | public | 2019-05-20 18:32 | 2019-07-05 11:41 | ||||
Reporter | bpc | ||||||||
Assigned To | correnson | ||||||||
Priority | normal | Severity | major | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
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 | |||||||
Summary | 0002437: External provers broken with 19.0-beta1 | ||||||||
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 | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
correnson (manager) 2019-05-21 10:12 |
This is really strange, here is my Why3-config: $ why3 config --detect-provers Found prover Alt-Ergo version 2.0.0, OK. Found prover CVC4 version 1.6 (alternative: counterexamples) Found prover CVC4 version 1.6, OK. Found prover Z3 version 4.6.0 (alternative: counterexamples) Found prover Z3 version 4.6.0, OK. Found prover Z3 version 4.6.0 (alternative: noBV) Found prover Coq version 8.9.0, OK. 7 prover(s) added Generating strategies: Prover Z3 4.6.0 will be used in Auto level >= 1 Prover Alt-Ergo 2.0.0 will be used in Auto level >= 1 Prover CVC4 1.6 will be used in Auto level >= 1 Save config to /Users/correnson/.why3.conf And every works fine with why3:cvc4, why3:z3 add why3:alt-ergo versions. Can you re-run your example with -wp-msg-key=prover option to collect the output of solvers ? |
bpc (reporter) 2019-05-21 16:00 |
Removing ~/.why3.conf and re-running "why3 config --detect-provers" appears to solve the problem with swap.c but not with my real source file. I will strip it down. Stay tuned... |
bpc (reporter) 2019-05-21 17:04 |
With the attached tst.c, running "frama-c -wp tst.c -wp-prover z3 -wp-msg-key=prover" produces : [kernel] Parsing tst.c (with preprocessing) [wp] Warning: Missing RTE guards [wp] 2 goals scheduled [wp] [Qed] Goal typed_bar_call_foo_requires preprocessing [wp:prover] Simplify goal [wp:prover] Simplification time: 0.57ms [wp] [Qed] Goal typed_foo_ensures preprocessing [wp:prover] Simplify goal [wp:prover] Simplification time: 0.05ms [wp:prover] Created temporary directory '/tmp/wpd73d9c.dir' [wp:prover] Created output directory '/tmp/wpd73d9c.dir/typed' [wp:prover] Generate '/tmp/wpd73d9c.dir/typed/Axiomatic.why' RUN 'why3 "prove" --extra-config "/home/agaha/.opam/default/share/frama-c/wp/why3/why3.conf" "/tmp/wpd73d9c.dir/typed/bar_Why3_ide.why" -P "z3" -T "VCbar_call_foo_requires" -G "WP" -t "10" -L "/tmp/wpd73d9c.dir/typed" -L "/home/agaha/.opam/default/share/frama-c/wp/why3"' RESULT result 1 OUT: ERR: [Config] reading extra configuration file /home/agaha/.opam/default/share/frama-c/wp/why3/why3.conf File "/tmp/wpd73d9c.dir/typed/bar_Why3_ide.why", line 16, characters 7-8: syntax error END [wp] WPOUT/typed/bar_Why3_ide.why:16: User Error: why3 syntax error [wp] [z3] Goal typed_bar_call_foo_requires : Failed why3 syntax error [wp] Proved goals: 1 / 2 Qed: 1 Z3: 0 (failed: 1) [wp] User Error: Deferred error message was emitted during execution. See above messages for more information. [kernel] Plug-in wp aborted: invalid user input. There are also "syntax errors" with why3:cvc4 and why3:alt-ergo Is it a why3 problem ? opam wants to use "why 1.2.0" |
correnson (manager) 2019-05-21 17:33 Last edited: 2019-05-21 17:34 |
No, it is supposed to be the preferred version. Could you please : 1. run your example with -wp-out ./logs (or any directory of your choice) 2. send us back the generated output file, that will be, eg: ./logs/typed/bar_Why3_ide.why If you need obfuscation, please do, but keep intact the line(s) that produce the syntax errors. Thanks a lot for reporting ! ****EDIT**** I did't see you have attached the file. That's perfect. |
correnson (manager) 2019-05-21 17:37 |
Fixed error in generated [@expl.] tag for Why3 output |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2019-05-20 18:32 | bpc | New Issue | |
2019-05-20 18:32 | bpc | File Added: swap.c | |
2019-05-21 10:12 | correnson | Note Added: 0006764 | |
2019-05-21 16:00 | bpc | Note Added: 0006765 | |
2019-05-21 16:54 | bpc | File Added: tst.c | |
2019-05-21 17:04 | bpc | Note Added: 0006766 | |
2019-05-21 17:33 | correnson | Note Added: 0006767 | |
2019-05-21 17:33 | correnson | Assigned To | => correnson |
2019-05-21 17:33 | correnson | Status | new => acknowledged |
2019-05-21 17:34 | correnson | Note Edited: 0006767 | View Revisions |
2019-05-21 17:37 | correnson | Note Added: 0006769 | |
2019-05-21 17:37 | correnson | Status | acknowledged => resolved |
2019-05-21 17:37 | correnson | Resolution | open => fixed |
2019-07-05 11:40 | signoles | Fixed in Version | => Frama-C 19-Potassium |
2019-07-05 11:41 | signoles | Status | resolved => closed |