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,

I somehow do not understand what this option is exactly doing.
I tried to find more information in the manual, but unfortunately I
couldn't.
In the help-page I found even more VC transformation options like --exp all
or eval-goals...
I am wondering now, if it is sufficient if a VC can be proved with the
option -exp goal, but not without (timeout).
Especially as it seems to be a default option in batch mode.
To answer this I'd like to understand better what is meant by "expand
definitions of predicates in the generated goals".
Maybe someone can help with this.

Thank you in advance,
Kerstin



>> 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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/ms-tnef
Size: 3375 bytes
Desc: not available
Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091209/6c0566bd/attachment.bin