| View Issue Details [ Jump to Notes ] [ Related Changesets ] | [ Issue History ] [ Print ] |
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0002155 | Frama-C | Plug-in > wp | public | 2015-09-02 21:11 | 2016-06-21 14:08 |
|
| Reporter | kroeckx | |
| Assigned To | patrick | |
| Priority | normal | Severity | minor | Reproducibility | always |
| Status | closed | Resolution | fixed | |
| Platform | | OS | | OS Version | |
| Product Version | Frama-C Sodium | |
| Target Version | | Fixed in Version | Frama-C Aluminium | |
|
| Summary | 0002155: coq fails to compile Cint because Zbits is not found |
| Description | As described in https://lists.gforge.inria.fr/pipermail/frama-c-discuss/2014-March/004380.html, [^] I get the same error message that Cint can't be compiled because Zbits isn't compiled yet.
I'm getting this on a Debian system.
I attached a patch based on the mail that seems to fix the issue for me.
|
| Tags | No tags attached. |
|
| Attached Files |  wp.driver.patch [^] (523 bytes) 2015-09-02 21:11 [Show Content] [Hide Content]--- wp.driver 2015-09-02 21:05:01.931775827 +0200
+++ wp.driver 2015-09-02 21:04:57.495868573 +0200
@@ -65,13 +65,13 @@
{coq="Rmin";altergo="min_real";why3="Rg.min"};
library cint:
+coq.file += "coqwp/Bits.v";
+coq.file += "coqwp/Zbits.v";
coq.file += "coqwp/Cint.v";
why3.file += "why3/Cint.why";
altergo.file += "ergo/Cint.mlw";
library cbits: cint
-coq.file += "coqwp/Bits.v";
-coq.file += "coqwp/Zbits.v";
coq.file += "coqwp/Cbits.v";
altergo.file += "ergo/Cbits.mlw";
why3.file += "why3/Cbits.why";
|
|
Relationships 
Relationships