View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | 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 | OS | 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 |
![]() |
|
yakobowski (manager) 2018-07-17 17:26 |
I have added Chlorine in the list of versions. |
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). |
correnson (manager) 2018-07-24 17:03 |
Thanks for the report. There is actually an error in the generated drivers for why3:coq. |
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. |
correnson (manager) 2018-07-24 17:16 |
Fixed in Frama-C/Trunk ; fixed configuration files uploaded. |
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 |
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 ? |
timourf (reporter) 2018-08-06 11:56 Last edited: 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. |
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 |
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 |
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. |
timourf (reporter) 2018-08-17 10:45 Last edited: 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. |
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) |
correnson (manager) 2018-12-03 11:21 |
You shall now upgrade to Frama-C 18.0 (Argon) which has been just released last week. |
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. |
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) |
correnson (manager) 2019-10-17 16:30 |
Fixed in upcomping Calcium version |
signoles (manager) 2020-02-17 18:08 |
Fixed in Frama-C 20.0 (Calcium). |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
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 |