--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on February 2010 ---
Hi Claude, >> 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 ... Yes, it works. I just to have to type $ why --lib-file jessie.why --coq-v8 sample.why and after that $ coqide -requires jessie_why sample.v Anyway, I will try to follow the instructions from Pascal. Thank you. Best regards, B?rbara A 2010/02/19, ?s 09:29, Claude Marche escreveu: > 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 | > > > > > > > > > _______________________________________________ > Why-discuss mailing list > Why-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why-discuss