--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on August 2014 ---
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>