--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on July 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Plateform Why3 0.72



On 07/20/2012 10:20 AM, DAHAN Mickael wrote:
>
> Hello.
>
> I would like to know how can I do to launch the plateform Why3 0.72 on 
> frama-c Nitrogen.
>
>

The formulation of your question is somewhat strange... Please see 
http://krakatoa.lri.fr for explanations on the relations between 
Frama-C, Why3, and the Jessie plugin. In short:

* compile and install Frama-C Nitrogen and Why3 in any order (the newer 
Why3 0.73 if possible ;-)
* compile and install Why 2.31 which contains the Jessie plugin
* detect provers: why3config --detect

then:

frama-c -jessie file.c

will start compute VCs for your C code and start the why3 GUI on them

- Claude
-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? nettoy?e...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120720/75c6addc/attachment.html>