ID0002389: **This issue was created automatically from Mantis Issue 2389. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002389 | Frama-C | Plug-in > wp | public | 2018-07-17 | 2020-02-17 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | timourf | **Assigned To** | correnson | **Resolution** | fixed | | **Priority** | normal | **Severity** | crash | **Reproducibility** | always | | **Platform** | x86_64 | **OS** | Linux | **OS Version** | - | | **Product Version** | - | **Target Version** | Frama-C 17-Chlorine | **Fixed in Version** | Frama-C 20-Calcium | ### 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 ### 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 ### 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 ## Attachments - [coq.drv](/uploads/7d46c6d1e6ee9a9a0ee6e60e0dbb72f7/coq.drv) - [wp.driver](/uploads/9801629381f7c222b5f698622a1d6551/wp.driver)