Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002437Frama-CKernelpublic2019-05-20 18:322019-07-05 11:41
Reporterbpc 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
Platformx86_64 GNU/LinuxOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C 19-Potassium 
Summary0002437: External provers broken with 19.0-beta1
DescriptionExternal 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
TagsNo tags attached.
Attached Filesc file icon swap.c [^] (226 bytes) 2019-05-20 18:32 [Show Content]
c file icon tst.c [^] (144 bytes) 2019-05-21 16:54 [Show Content]

- Relationships

-  Notes
(0006764)
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 ?
(0006765)
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...
(0006766)
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"
(0006767)
correnson (manager)
2019-05-21 17:33
edited on: 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.
(0006769)
correnson (manager)
2019-05-21 17:37

 Fixed error in generated [@expl.] tag for Why3 output

- Issue History
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 Note Added: 0006768
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-05-21 17:39 correnson Note Deleted: 0006768
2019-07-05 11:40 signoles Fixed in Version => Frama-C 19-Potassium
2019-07-05 11:41 signoles Status resolved => closed

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker