--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on August 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] why-2.34 compile problem



On Thu, Aug 14, 2014 at 1:19 PM, Christoph Thielecke <u28616 at hs-harz.de>
wrote:

> Another problem:
> WHYLIB=lib bin/why.opt --no-pervasives -tc lib/why/prelude.why
> for f in lib/why/bool.why lib/why/integer.why lib/why/divisions.why
> lib/why/real.why lib/why/arrays.why lib/why/jessie.why
> lib/why/jessie_bitvectors.why lib/why/mybag.why lib/why/mix.why
> lib/why/floats_common.why lib/why/floats_strict.why lib/why/floats_full.why
> lib/why/floats_multi_rounding.why  ; do \
>                 WHYLIB=lib bin/why.opt -tc $f; \
>         done
> coqc  -R lib/coq Why lib/coq/WhyFloats.v
> File "/home/crissi/frama-c/why-2.34/lib/coq/WhyFloats.v", line 111,
> characters 7-37:
> Error: The reference Fcalc_digits.Zpower_gt_Zdigits was not found
> in the current environment.
> make: *** [lib/coq/WhyFloats.vo] Error 1
>
>
> Any ideas?
>

You must have flocq 2.3.0.  You'll need this patch:

--- lib/coq/WhyFloats.v.orig 2014-03-17 16:01:46.000000000 -0600
+++ lib/coq/WhyFloats.v 2014-04-21 15:39:55.680771647 -0600
@@ -108,7 +108,7 @@
 generalize (Zeq_bool_eq _ _ H1). clear.
 rewrite Fcalc_digits.Z_of_nat_S_digits2_Pnat.
 intros H.
-apply (Fcalc_digits.Zpower_gt_Zdigits Fcalc_digits.radix2 (Zpos prec)
(Zpos m)).
+apply (Fcore_digits.Zpower_gt_Zdigits Fcalc_digits.radix2 (Zpos prec)
(Zpos m)).
 revert H.
 unfold FLT_exp.
 generalize (Fcore_digits.Zdigits radix2 (Zpos m)).

Regards,
-- 
Jerry James
http://www.jamezone.org/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140814/b6e281bc/attachment.html>