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] [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                    |