--- layout: fc_discuss_archives title: Message 34 from Frama-C-discuss on February 2010 ---
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") 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. 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 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! 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. Best regards, B?rbara Vieira