--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on February 2010 ---
Barbara Vieira wrote: > Hi everyone, > > I'm trying to generate the Coq file for a C annotated file, but I don't know what is going on, because I always get the same error. > > I'm using Why 2.23 and I installed the last Frama-C version for Mac OS Snow Leopard (the compiled sources). > > When I run the command: > > $ frama-c -jessie -jessie-atp coq file.c > > I got the same error every time: > > ... > > Generating Why function func > [jessie] Calling VCs generator. > why -coq [...] why/framac-example.why > Fatal error: exception Failure("real constants not supported with Coq V7") > This means that Why has been compiled for the support of the old Coq version 7, instead of the current version 8.x. This is a mistake that I I'm not sure can be fixed since you installed a binary package. But let's try: > make: *** [coq/framac-example_why.v] Error 2 > [jessie] user error: Jessie subprocess failed: make -f framac-example.makefile coq > > > What I did first, was to try to generate the Coq file using the sample.makefile that is inside the folder sample.jessie. Of course I got the same error. Of course... > Anyway, I decided to generate the Coq file using Why, so I typed: > > (I'm inside sample.jessie folder) > $ cd why > $ why --lib-file jessie.why --coq sample.why > > You should enforce the coq version by using why --coq-v8 ... But I can't test if it really works... > The file sample.v is generated, but... the command: > > $coqc framac_example.v > > gives the following errror: > > File "./framac_example.v", line 23, characters 67-76: > Error: The reference bitvector was not found in the current environment. > > Well, it seems that the lib jessie_why.v is not being loaded. Well, I generated the jessie_why.vo ( I took it from why lib) and I added it to the same folder of sample.v. And then I typed, > > $ coqc -require jessie_why framac_example.v > File "./framac_example.v", line 30, characters 4-5: > Error: The reference x was not found in the current environment. > > So, I decided to use the CoqIDE: > > $ coqide -require jessie_why framac_example.v > > But it seems that some of the lemmas are not correctly generated. For example: > > > (*Why axiom*) Lemma bitvector_of_char_P_of_char_P_of_bitvector : > ((x:bitvector) (bitvector_of_char_P (char_P_of_bitvector x)) = x). > Admitted. > > > I think that some foralls were missed! > No, this is the old coq v7 syntax for forall. Please try again with why --coq-v8 > Well, I really don't know what to do! My problem is to generated the Coq file using the Jessie-plugin. As far as I understood, the problem is in Why and not in Frama-C, but I don't know how to solve it. > > It's a combination of problems: - Frama-C binary package should have been compiled with coq V8 support - Why should redetect properly the coq version after installation Hope this helps, - Claude -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |