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

Dear Claude,

thanks for your reply.
I tried the additional option and the discrepancies are gone now.

Jens

Am 08.12.2009 um 09:53 schrieb Claude Marche:

>
> I confirm I get the same behavior.
>
> After investigating, I found that this because in batch mode, the
> generation of goals for smt solvers (yices, z3, cvc3)
> is done with the why option "-exp goal" which ask to automatically
> expand definitions of predicates in the generated goals.
>
> 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...)
>
> Thanks for pointing the difference, we will try to fix that.
>
> - Claude
>



-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091208/023ceee9/attachment.htm