Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Generate Coq file using Frama-c / Why
  • From: barbaraisabelvieira at gmail.com (Barbara Vieira)
  • Date: Thu, 18 Feb 2010 16:01:55 +0000
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