--- layout: fc_discuss_archives title: Message 100 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



Kerstin Hartig wrote:
> 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.
>
>   

If the goal contains f(a), and f is a predicate or function defined by

logic P(x) = e

then replace f(a) in the goal by e where occurrence of x are replaced by a.

It can be expected that automatic provers could do that themselves, but 
unfortunately provers are sometimes so as smart as expected...

- Claude


> 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
>>>       
>>> ------------------------------------------------------------------------
>>>
>>> _______________________________________________
>>> 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                    |