2021-03-02 01:42 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002155Frama-CPlug-in > wppublic2015-09-02 21:112016-06-21 14:08
Reporterkroeckx 
Assigned Topatrick 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Sodium 
Target VersionFixed in VersionFrama-C Aluminium 
Summary0002155: coq fails to compile Cint because Zbits is not found
DescriptionAs 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.
TagsNo tags attached.
Attached Files
  • patch file icon wp.driver.patch (523 bytes) 2015-09-02 21:11 - 
    --- 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";
    patch file icon wp.driver.patch (523 bytes) 2015-09-02 21:11 +

-Relationships
+Relationships

-Notes

~0006041

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

~0006060

patrick (developer)

2015-10-08 14:53

 Fix committed to master branch.
+Notes

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