--- layout: fc_discuss_archives title: Message 70 from Frama-C-discuss on December 2009 ---
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 Jens Gerlach wrote: > Hello, > > we experience a discrepancy between the verification results in the Jessie-GUI versus those of the command line. > (I am talking about Beryllium-20090901 with why version 2.19 on Mac OS X.) > When verifying the following function. > > /*@ > requires \valid(p); > requires \valid(q); > > assigns *p; > assigns *q; > > ensures *p == \old(*q); > ensures *q == \old(*p); > */ > void swap(int* p, int* q) > { > int save = *p; > *p = *q; > *q = save; > } > > The results of the command line > > frama-c -jessie -jessie-no-regions -jessie-atp yices sw.c > > yields > ... > total : 6 > valid : 6 (100%) > ... > total wallclock time : 0.78 sec > > However, when calling the gui with > > frama-c -jessie -jessie-no-regions sw.c > > we obtain a timeout ("scissors") on the third precondition. > > I cannot understand why there is a timeout in the gui when the total wallclock time for yices is less than a second. > Can other people confirm this on their respective installations? > > Regards > > Jens Gerlach > > > > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |