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

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                    |