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-05-21 17:37
Reporterbpc 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusresolvedResolutionfixed 
Platformx86_64 GNU/LinuxOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in Version 
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

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker