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] Supported features, Global invariants, and POs


JENN Eric wrote:
> Dear Colleagues,
> 
> (Again (sorry about that...) some probably dumb questions for which I 
> haven't found any clear answer in the archive / documentation...)
> 
> *Q1*: *Is there any way to know what subset/features of ACSL is 
> supported by Jessie ? *
> As far as I understand, all but red parts in the ACSL document are 
> "supported by Frama-C", but what about *Jessie*?
> (Even though it sounds like a FAQ... I have checked Frama-C's source 
> distribution for any appropriate "pdf" file, without any success. I 
> think that this information would be extremely useful...)

This information is is the manual of the jessie plugin( 
http://frama-c.cea.fr/jessie.html), in section
7.2  Unsupported features

which is at the end of the doc.

It is certainly incomplete, and please do not hesitate to report to us 
the missing information, it will benefit to every user.

> *Q2:  I woud like to use an inductive predicate ("is_reacheable", which 
> is identical to the one in page 2.24 of the ACSL documentation), but I 
> would like to used it to define a /global invariant/.*  

> 
> Whenever I run Jessie (e.g., "frama-c -jessie-analysis -jessie-gen-goals 
> list.c"), I get the following error message:
> "File "list.jc", line 390, characters 47-79 : typing error : a memory 
> state is needed (\at missing?)."

Please look carefully at the example: there is one label to that 
predicate, which indicates that it depends on one memory state.

> I guess that this comes from the fact that invariants are (by default) 
> *weak* and so the tool needs to know the context in which the property 
> shall hold... Unfortunately, I am actually interested by a *strong * 
> invariant, and I don't know how to express that.
> 
> Any idea?

No it is not related to strong or weak invariant, it simply needs a 
label in the definition.

Now, about weak or strong invariant: I'm pretty sure your invariant 
cannot be strong: this is a property that must be maintained by 
functions which build lists, and they might violated that invariant 
temporarily. Anyway, making that invariant strong will probably not help 
jessie, jessie prefers weak invariants.

> *Q3:*  When a PO can't be discharged, I guess that having a look to the 
> PO structure in gWhy might help.
> However, if most of the POs can be understood fairly easily, some 
> explanations (or pointers to documents) would be helpful concerning the 
> following elements:
> + store
> + shift
> + select
> More generally, do you have any hints on how one shall proceed when a PO 
> can't be discharged automatically?
> This is certainly a stupid question, but I guess that there might be 
> some "procedure" or "approach" or whatever to address the problem.
> I'm dreading getting the following answer: "you have to be an expert..." 
> ;-)

My opinion is that proving annotations is as least as much difficult as 
programming. Programming is something that you have to learn, and 
improving your programming skill is the same as improving your expertise...

Now, to answer the precise question: when something is not proved 
although you think it is true, I suggest first to insert assertions in 
the code, to state intermediate properties you think are needed to 
obtain a proof. Seeing whether the assertion is proved or not, and 
seeing whether the post-condition is proven when given the assertion, 
will help you to understand.


- Claude

> Thanks for your help / advices.
> 
> Have a nice week-end.
> 
> Regards,
> e.
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> 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                    |