Frama-C Bug Tracking System - Frama-C
View Issue Details
0002155Frama-CPlug-in > wppublic2015-09-02 21:112016-06-21 14:08
kroeckx 
patrick 
normalminoralways
closedfixed 
Frama-C Sodium 
Frama-C Aluminium 
0002155: coq fails to compile Cint because Zbits is not found
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.
No tags attached.
patch wp.driver.patch (523) 2015-09-02 21:11
https://bts.frama-c.com/file_download.php?file_id=1059&type=bug
Issue History
2015-09-02 21:11kroeckxNew Issue
2015-09-02 21:11kroeckxStatusnew => assigned
2015-09-02 21:11kroeckxAssigned To => correnson
2015-09-02 21:11kroeckxFile Added: wp.driver.patch
2015-09-18 08:13patrickNote Added: 0006041
2015-10-08 14:53patrickNote Added: 0006060
2015-10-08 14:53patrickAssigned Tocorrenson => patrick
2015-10-08 14:53patrickStatusassigned => resolved
2015-10-08 14:53patrickResolutionopen => fixed
2016-06-21 14:08signolesFixed in Version => Frama-C Aluminium
2016-06-21 14:08signolesStatusresolved => closed

Notes
(0006041)
patrick   
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".
(0006060)
patrick   
2015-10-08 14:53   
Fix committed to master branch.