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] how jessie and why platform work to generate a .v output?

Hi,

Le 02/11/2013 05:45, Xiao-lei Cui a ?crit :
> Hi all,
>     I am trying to figure out the workflow from C source(plus
> embeddedACSL spec) to the .v file passed to proof assistant.
>     I am using why2. Is the following workflow correct?
>     C/ACSL -> (frama-c/jessie)
>                       -->filename.jc ->(jessie/why)
>                                                   -->filename.why->(why)

more or less

> from
>>  frama-c -jessie -pp-annot max.c
> I got max.why, which is over 300lines of code.
> I then use why command to generate .v output for coq:
>>  why --coq max.why
> File "max.why", line 17, characters 29-35:
> Unbound type 'tag_id'
> 
>    Did I miss something or some step?
>    Thanks in advance.

the "why" command should be giving an additional prelude file as input.
Indeed you should not call why directly but use

make -f max.makefile coq

Anyway, the support of Coq in Why2 is known to be painful for the user.
Using Coq to discharge VCs using Why3 is much much easier to do, so I
strongly recommend to use Why3 instead.

- Claude





-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           |
Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |