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

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



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                    |