--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on November 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Partial verification



On 07/11/2011 12:27, n.rousset at laposte.net wrote:
>
> Beware, -jessie-help is not a frama-c option (as far as I know).
> In my previous message, I typed:
> jessie -help
> for the -help option of the jessie command line...
> Anyway, it gives you all the options.
>

I guess some clarifications wouldn't hurt: there are two Jessies out there:
- A Frama-C plugin, that enables the -jessie-help option of Frama-C. Its 
role is to take a C program and generate a program suitable for ...
- ...An independent application that in turn can generate Why and Why3 
programs. Like all well-behaved apps, it has a -help option.

http://krakatoa.lri.fr/ has a nice diagram that explains the whole 
process from C/ACSL code to provers using Jessie.

-- 
E tutto per oggi, a la prossima volta
Virgile