--- layout: fc_discuss_archives title: Message 34 from Frama-C-discuss on February 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Generate Coq file using Frama-c / Why



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