0002437: External provers broken with 19.0-beta1

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

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 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

swap.c (226 bytes) 2019-05-20 18:32

// File swap.c:

/*@ requires \valid(a) && \valid(b);
  @ ensures A: *a == \old(*b) ;
  @ ensures B: *b == \old(*a) ;
  @ assigns *a,*b ;
  @*/
void swap(int *a,int *b)
{
  int tmp = *a ;
  *a = *b ;
  *b = tmp ;
  return ;
}

swap.c (226 bytes) 2019-05-20 18:32

tst.c (144 bytes) 2019-05-21 16:54

/*@
  predicate Invariant{L} = 1 == 1;
*/

/*@
  requires Invariant;
  ensures Invariant;
*/
void foo(void)
{
}

void bar(void)
{
     foo();
}

tst.c (144 bytes) 2019-05-21 16:54

Relationships

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 Last edited: 2019-05-21 17:34 View 2 revisions	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

Notes

Date Modified	Username	Field	Change
Issue History
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

Issue History