Frama-C Bug Tracking System - Frama-C
View Issue Details
0002389Frama-CPlug-in > wppublic2018-07-17 16:412018-12-06 06:39
timourf 
correnson 
normalcrashalways
assignedreopened 
x86_64Linux
 
Frama-C 17-Chlorine 
0002389: Failure to detect qed libraries when running wp
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
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
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 [^]
No tags attached.
? coq.drv (2,452) 2018-07-24 17:13
https://bts.frama-c.com/file_download.php?file_id=1276&type=bug
? wp.driver (6,392) 2018-07-24 17:13
https://bts.frama-c.com/file_download.php?file_id=1277&type=bug
Issue History
2018-07-17 16:41timourfNew Issue
2018-07-17 16:41timourfStatusnew => assigned
2018-07-17 16:41timourfAssigned To => correnson
2018-07-17 17:26yakobowskiNote Added: 0006594
2018-07-17 17:26yakobowskiTarget Version => Frama-C 17-Chlorine
2018-07-20 10:12timourfNote Added: 0006596
2018-07-20 10:12timourfFile Added: ErrorZ3.log
2018-07-24 17:03corrensonNote Added: 0006604
2018-07-24 17:13corrensonFile Added: coq.drv
2018-07-24 17:13corrensonFile Added: wp.driver
2018-07-24 17:13corrensonFile Deleted: ErrorZ3.log
2018-07-24 17:15corrensonNote Added: 0006605
2018-07-24 17:16corrensonNote Added: 0006606
2018-07-24 17:16corrensonStatusassigned => resolved
2018-07-24 17:16corrensonResolutionopen => fixed
2018-08-06 10:54timourfNote Added: 0006626
2018-08-06 10:54timourfStatusresolved => feedback
2018-08-06 10:54timourfResolutionfixed => reopened
2018-08-06 11:23corrensonNote Added: 0006627
2018-08-06 11:56timourfNote Added: 0006628
2018-08-06 11:56timourfStatusfeedback => assigned
2018-08-06 11:57timourfNote Edited: 0006628bug_revision_view_page.php?bugnote_id=6628#r356
2018-08-06 12:29timourfNote Added: 0006629
2018-08-09 16:16timourfNote Added: 0006633
2018-08-10 10:40timourfNote Added: 0006634
2018-08-17 10:45timourfNote Added: 0006635
2018-08-17 15:08timourfNote Edited: 0006635bug_revision_view_page.php?bugnote_id=6635#r358
2018-12-01 07:21visqNote Added: 0006685
2018-12-03 11:21corrensonNote Added: 0006686
2018-12-05 06:56visqNote Added: 0006689
2018-12-06 06:39visqNote Added: 0006691

Notes
(0006594)
yakobowski   
2018-07-17 17:26   
I have added Chlorine in the list of versions.
(0006596)
timourf   
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   
2018-07-24 17:03   
Thanks for the report.
There is actually an error in the generated drivers for why3:coq.
(0006605)
correnson   
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   
2018-07-24 17:16   
Fixed in Frama-C/Trunk ; fixed configuration files uploaded.
(0006626)
timourf   
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   
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   
2018-08-06 11:56   
(edited on: 2018-08-06 11:57)
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   
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   
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   
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   
2018-08-17 10:45   
(edited on: 2018-08-17 15:08)
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   
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   
2018-12-03 11:21   
You shall now upgrade to Frama-C 18.0 (Argon) which has been just released last week.
(0006689)
visq   
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   
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)