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
0002389Frama-CPlug-in > wppublic2018-07-17 16:412018-12-06 06:39
Reportertimourf 
Assigned Tocorrenson 
PrioritynormalSeveritycrashReproducibilityalways
StatusassignedResolutionreopened 
Platformx86_64OSLinuxOS Version
Product Version 
Target VersionFrama-C 17-ChlorineFixed in Version 
Summary0002389: Failure to detect qed libraries when running wp
DescriptionThis 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 ReproduceInstalled 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 InformationProduct 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 [^]
TagsNo tags attached.
Attached Files? file icon coq.drv [^] (2,452 bytes) 2018-07-24 17:13
? file icon wp.driver [^] (6,392 bytes) 2018-07-24 17:13

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

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

Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker