Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002155Frama-CPlug-in > wppublic2015-09-02 21:112016-06-21 14:08
Assigned Topatrick 
PlatformOSOS Version
Product VersionFrama-C Sodium 
Target VersionFixed in VersionFrama-C Aluminium 
Summary0002155: coq fails to compile Cint because Zbits is not found
DescriptionAs described in, 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.
TagsNo tags attached.
Attached Filespatch file icon wp.driver.patch [^] (523 bytes) 2015-09-02 21:11 [Show Content]

- Relationships

-  Notes
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.

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

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker