--- layout: fc_discuss_archives title: Message 70 from Frama-C-discuss on December 2009 ---
[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



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                    |