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 see another situation where the --exp goal option is (would be) helpful.

Consider the goal to prove is P(a) where P is a user-defined predicate of the following shape:

Logic P(x) = e1 /\ e2

If provers are unable to prove P(a) and you don't understand why, it can be interesting to know which of e1 or e2 (or both) are actually not proved.

In the case of a goal directly written as e1 /\ e2, the --split-user-conj option can be used to split the goal in two "subgoals" e1 and e2.

Unfortunately, for the moment using options --exp goal and --split-user-conj together does not have the expected effect (the split is maybe done before the exp goal?).

Notice that in the Why Eclipse plugin (http://www.lri.fr/~oudot/), it is possible to split goals separately directly in the GUI, so that we can use it in conjunction with the --exp goal option. My experience on verifying Java programs with invariants involving several conjunctions of formulas, proved that feature very helpful.
But maybe for small C programs it is not as vital as that.

- Nicolas

-----Original Message-----
From: frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Claude Marche
Sent: jeudi 10 d?cembre 2009 09:17
To: Frama-C public discussion
Subject: Re: [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                    |




 



_______________________________________________
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