--- layout: fc_discuss_archives title: Message 36 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



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