--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on November 2011 ---
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