0002389: Failure to detect qed libraries when running wp

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0002389

Frama-C

Plug-in > wp

public

2018-07-17 16:41

2020-02-17 18:08

Reporter

timourf

Assigned To

correnson

Priority

normal

Severity

crash

Reproducibility

always

Status

closed

Resolution

fixed

Platform

x86_64

Linux

OS Version

Product Version

Target Version

Frama-C 17-Chlorine

Fixed in Version

Frama-C 20-Calcium

Summary

0002389: Failure to detect qed libraries when running wp

Description

This is not a problem with this particular code, but I will include it anyways for the sake of completeness and reproducibility.

With the following C code "average.c"
=============================================
/*@ ensures \result == \abs(x); */
double abs(double x) {
    if (x >= 0) return x;
    else return (-x);
}
/*@ requires 0x1p-967 <= C <= 0x1p970;
  @ ensures \result == \round_double(\NearestEven, (x+y)/2);
  @ */
double average(double C, double x, double y) {
    if (C <= abs(x)) return x/2+y/2;
    else return (x+y)/2;
}
=============================================
running the command
>frama-c -wp -wp-model +float -wp-prover "why3:coq" -wp-print average.c
produces the following output
=============================================
[kernel] Parsing average.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] average.c:9: Warning:
  Builtin \NearestEven not defined
[wp] 2 goals scheduled
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /home/timourf/.opam/default/share/frama-c/wp/why3/why3.conf
Fatal error while loading driver file '/home/timourf/.opam/default/share/why3/drivers/coq.drv':
File "/home/timourf/.opam/default/share/frama-c/wp/why3/coq.drv", line 24, characters 7-14:
Library file not found: qed
------------------------------------------------------------
------------------------------------------------------------
--- Why3 (stderr) :
------------------------------------------------------------
[Config] reading extra configuration file /home/timourf/.opam/default/share/frama-c/wp/why3/why3.conf
Fatal error while loading driver file '/home/timourf/.opam/default/share/why3/drivers/coq.drv':
File "/home/timourf/.opam/default/share/frama-c/wp/why3/coq.drv", line 24, characters 7-14:
Library file not found: qed

... (less relevant output) ...
=============================================
the line referenced in coq.drv is

"theory qed.Qed meta "realized_theory" "qed.Qed", "Qed" end

Steps To Reproduce

Installed the following via OPAM

coq 8.8.0 (because 8.8.1+ reports not supported by why3)
why3-coq 1.0.0
frama-c-chlorine-20180501

error persists after uninstalling and re-installing all of the above

Additional Information

Product Version: Frama-C-Chlorine-20180501 **not an option in reporting tool**

I reported this here because the error seems to be with the configurations files generated by frama-c in the frama-c/wp directory, but I can't be sure that the problem isn't with why3 itself. I'm still very new to using these tools.

Note: the "Builtin \NearestEven not defined" seems to be a separate bug, referenced here: https://lists.gforge.inria.fr/pipermail/frama-c-discuss/2016-July/005117.html

Tags

No tags attached.

Attached Files

coq.drv (2,452 bytes) 2018-07-24 17:13
wp.driver (6,392 bytes) 2018-07-24 17:13

Relationships

Relationships

Notes
~0006594 yakobowski (manager) 2018-07-17 17:26	I have added Chlorine in the list of versions.

~0006596 timourf (reporter) 2018-07-20 10:12	I've been experimenting with this a little bit more, and indeed the problem seems to be in the configuration file 'frama-c/wp/why3/why3.conf' It's not specific to coq, it seems to be an issue between why3 and wp (I tried using other provers with why3, like Z3 and Gappa, and still ran into issues reading the same configuration file). I removed why3-coq and reinstalled frama-c with only base why3. I am able to do basic proofs using why3 by itself, but I run into issues running it with wp every time. I will upload the output of an attempt to run a proof with Z3 as the why3 backend for wp as 'ErrorZ3.log'. This is why3 1.0.0 installed via OPAM, so it should be supported (according to wp documentation).

~0006604 correnson (manager) 2018-07-24 17:03	Thanks for the report. There is actually an error in the generated drivers for why3:coq.

~0006605 correnson (manager) 2018-07-24 17:15	I have: - deleted the ErrorZ3.log which is not useful - added a fix for [frama-c-share]/wp/why3/coq.drv - added a fix for [frama-c-share]/wp/wp.driver This should work better, sorry for the inconvenience.

~0006606 correnson (manager) 2018-07-24 17:16	Fixed in Frama-C/Trunk ; fixed configuration files uploaded.

~0006626 timourf (reporter) 2018-08-06 10:54	The fix for wp.driver works fine. The same driver file error persists when I try to run wp, however. The line from coq.drv which was referenced in the issue, line 24, was not changed in the patch and it is still unable to find the qed library file. line: theory qed.Qed meta "realized_theory" "qed.Qed", "Qed" end

~0006627 correnson (manager) 2018-08-06 11:23	I'm not sure why3 1.0.0 (released juste after Chlorine) is fully compatible with Frama-C. We sticked to version 0.88.3 at the time of releasing, and on the go for supporting last distribution of Why3 and Coq. Could you try with why3 0.88.3 and Coq 8.7.1 ?

~0006628 timourf (reporter) 2018-08-06 11:56 Last edited: 2018-08-06 11:57 View 2 revisions	I'm unable to install why3-base 0.88.3 with ocaml 4.06.1 because of an unbound module (Big_int). I will try with an older version of opam and/or compiling from source and post an update later, as this seems to be a known issue.

~0006629 timourf (reporter) 2018-08-06 12:29	I successfully compiled frama-c with ocaml 5.05.0, why3 0.88.3, and coq 8.7.1 as you suggested. Now there is a different fatal error when I try to run wp. [Config] reading extra configuration file /home/timourf/.opam/4.05.0/share/frama-c/wp/why3/why3.conf Fatal error while loading driver file '/home/timourf/.opam/4.05.0/share/why3/drivers/coq.drv': File "/home/timourf/.opam/4.05.0/share/why3/drivers/coq-common.gen", line 35, characters 7-16: Library file not found: bool

~0006633 timourf (reporter) 2018-08-09 16:16	I've verified the problem in a new linux VM with a different distribution. With frama-c chlorine, why3 0.88.3, and coq 8.7.1, with the above patches applied, I am still unable to find the qed library referenced in coq.drv

~0006634 timourf (reporter) 2018-08-10 10:40	The libraries referenced are defined in wp.driver, which is definitely being read by wp. The problem seems to be in why3 recognizing the libraries loaded by wp. I'm unfamiliar with the code base and the wp/prover interface, so I'm afraid I probably won't be of any more help.

~0006635 timourf (reporter) 2018-08-17 10:45 Last edited: 2018-08-17 15:08 View 2 revisions	I seem to get different errors using different versions of the ocaml compiler. I think it would help newcomers a lot if there were some kind of definitive list of versions for "the current working build", especially when wp and supported external provers are involved, because "install via opam" isn't always the solution. For example, I've tried doing the setup on two different linux distributions so far. Each system package manager defaulted to different opam switches, resulting in different errors/incompatibilities. I'll list some of the things I've noted so far: The page on frama-c.com for wp recommends different versions of the external provers than the current version of the wp manual (for instance, why3 0.87 and 0.88+ respectively). The manual lists coq 8.7 as the latest supported major version, but there is no information about minor versions (8.7.0 is the original, @correnson you mentioned 8.7.1 here, 8.7.2 is the latest). *The compilation instructions recommend opam >=1.2.2 and ocaml ">=4.02.3". Some versions of ocaml beyond 4.02.3 have compatibility issues with some of the provers and libraries (see above), so a more concrete "ocaml=4.xx.x is known to work with ..." would help.

~0006685 visq (reporter) 2018-12-01 07:21	Same problem here, on a fresh install of frama-c via opam; I kind of fixed the problem for me, but not in a clean way. In why3ide, coq.drv does not work and why3 crashes with: > Library file not found: qed Apparently, why3 looks for 'qed.why' when interpreting coq.drv, but frama-c defines 'Qed.why' (lower vs. upper case letter). Renaming the *.why files to lowercase, and removing arctrigo from coq.drv (has no .why file) got rid of this error. Next problem in the Coq prover output: > Error: Unable to locate library BuiltIn All the coq libs seem to be placed in frama-c/wp/coqwp. So I compiled the libraries there, with -Q coqwp '', and added this -Q option also to coq and coqide in why3.conf. Now I can work with frama-c, why3 and coq, though I still get warnings. It would be nice if the maintainer could look at this, and provide a proper fix. I'm happy to provide further information regarding the problems. Versions: frama-c: Chlorine-20180502 why3: 0.88.3 coq: 8.6 (ocaml 4.05.0)

~0006686 correnson (manager) 2018-12-03 11:21	You shall now upgrade to Frama-C 18.0 (Argon) which has been just released last week.

~0006689 visq (reporter) 2018-12-05 06:56	I had a look in the source repository of Argon: ArcTrigo.why is now present, but the import names in coq.drv are still lowercase, and the filenames CamelCase. So I do not think this is fixed, but I'm happy to check as soon as Argon is available via OPAM.

~0006691 visq (reporter) 2018-12-06 06:39	I can confirm that the issue is still present in Frama-c 18 (Argon). > [...] > Library file not found: qed > [...] > frama-c --version > 18.0 (Argon)

~0006898 correnson (manager) 2019-10-17 16:30	Fixed in upcomping Calcium version

~0006952 signoles (manager) 2020-02-17 18:08	Fixed in Frama-C 20.0 (Calcium).

Notes

Date Modified	Username	Field	Change
Issue History
2018-07-17 16:41	timourf	New Issue
2018-07-17 16:41	timourf	Status	new => assigned
2018-07-17 16:41	timourf	Assigned To	=> correnson
2018-07-17 17:26	yakobowski	Note Added: 0006594
2018-07-17 17:26	yakobowski	Target Version	=> Frama-C 17-Chlorine
2018-07-20 10:12	timourf	Note Added: 0006596
2018-07-20 10:12	timourf	File Added: ErrorZ3.log
2018-07-24 17:03	correnson	Note Added: 0006604
2018-07-24 17:13	correnson	File Added: coq.drv
2018-07-24 17:13	correnson	File Added: wp.driver
2018-07-24 17:13	correnson	File Deleted: ErrorZ3.log
2018-07-24 17:15	correnson	Note Added: 0006605
2018-07-24 17:16	correnson	Note Added: 0006606
2018-07-24 17:16	correnson	Status	assigned => resolved
2018-07-24 17:16	correnson	Resolution	open => fixed
2018-08-06 10:54	timourf	Note Added: 0006626
2018-08-06 10:54	timourf	Status	resolved => feedback
2018-08-06 10:54	timourf	Resolution	fixed => reopened
2018-08-06 11:23	correnson	Note Added: 0006627
2018-08-06 11:56	timourf	Note Added: 0006628
2018-08-06 11:56	timourf	Status	feedback => assigned
2018-08-06 11:57	timourf	Note Edited: 0006628	View Revisions
2018-08-06 12:29	timourf	Note Added: 0006629
2018-08-09 16:16	timourf	Note Added: 0006633
2018-08-10 10:40	timourf	Note Added: 0006634
2018-08-17 10:45	timourf	Note Added: 0006635
2018-08-17 15:08	timourf	Note Edited: 0006635	View Revisions
2018-12-01 07:21	visq	Note Added: 0006685
2018-12-03 11:21	correnson	Note Added: 0006686
2018-12-05 06:56	visq	Note Added: 0006689
2018-12-06 06:39	visq	Note Added: 0006691
2019-10-17 16:30	correnson	Note Added: 0006898
2019-10-17 16:30	correnson	Status	assigned => resolved
2019-10-17 16:30	correnson	Fixed in Version	=> Frama-C 20-Calcium
2019-10-17 16:30	correnson	Resolution	reopened => fixed
2020-02-17 18:08	signoles	Status	resolved => closed
2020-02-17 18:08	signoles	Note Added: 0006952

Issue History