View Issue Details [ Jump to Notes ] | [ 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 | ||||||
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 |
|
![]() |
|
patrick (developer) 2015-09-18 08:13 |
In fact "Cint.v" is reusing some trivial lemmaes wich are into "Bits.v". But I don't see why "Zbit.v" have to be moved from "cbits" library to "cint" library. The patch fixes the problem. The good way to correct that is to rewrite the trivial two lemmaes about two_power_nat into "Cint.v" since there no good reason that "cint" library requires "Bit.v". |
patrick (developer) 2015-10-08 14:53 |
Fix committed to master branch. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2015-09-02 21:11 | kroeckx | New Issue | |
2015-09-02 21:11 | kroeckx | Status | new => assigned |
2015-09-02 21:11 | kroeckx | Assigned To | => correnson |
2015-09-02 21:11 | kroeckx | File Added: wp.driver.patch | |
2015-09-18 08:13 | patrick | Note Added: 0006041 | |
2015-10-08 14:53 | patrick | Source_changeset_attached | => framac master 21d379bf |
2015-10-08 14:53 | patrick | Note Added: 0006060 | |
2015-10-08 14:53 | patrick | Assigned To | correnson => patrick |
2015-10-08 14:53 | patrick | Status | assigned => resolved |
2015-10-08 14:53 | patrick | Resolution | open => fixed |
2016-06-21 14:08 | signoles | Fixed in Version | => Frama-C Aluminium |
2016-06-21 14:08 | signoles | Status | resolved => closed |