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] Discrepancy between Jessie gui and command line when using yices

Hello,

Claude Marche a ?crit :
> Thus to obtain the same behavior in the gui, you need to do
> 
> frama-c -jessie  -jessie-why-opt " -exp goal" sw.c
> 
> (Do not forget the space before the -exp, because of the frama-c model 
> for options parsing...)

Yes, that works. Indeed quoting the Frama-C User Manual, Section 3.3 
"Frama-C Command Line and General Options", page 17:

==========
If the option's argument is a string (that is, neither an integer nor a 
float, etc), the following format is also possible:

	-option_name=value.

This last format must be used when value starts with a minus sign.
==========

Thus another less-hackish solution is:

	frama-c -jessie -jessie-why-opt="-exp goal" sw.c

(no additional space before -exp expected).

--
Julien