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