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

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                    |