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
- Subject: [Frama-c-discuss] Supported features, Global invariants, and POs
- From: Claude.Marche at inria.fr (Claude Marché)
- Date: Mon, 18 May 2009 13:46:06 +0200
- In-reply-to: <4A0D94E6.9080208@fr.thalesgroup.com>
- References: <1241624519.21376.229.camel@supelec> <5EFD4D7AC6265F4D9D3A849CEA9219191AB19E@LAXA.intra.cea.fr><F1229212CB084F4CBEA197909C8699F1021BDA24@TLSMAIL1.tls.fr.astrium.corp> <4A02BAAB.5010809@inria.fr> <F1229212CB084F4CBEA197909C8699F1021BDA26@TLSMAIL1.tls.fr.astrium.corp> <4A0D94E6.9080208@fr.thalesgroup.com>
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 |
- References:
- [Frama-c-discuss] A variation domain failed to be computed
- From: jcdemay at rennes.supelec.fr (Jonathan-Christofer Demay)
- [Frama-c-discuss] A variation domain failed to be computed
- From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
- [Frama-c-discuss] Logical annotations
- From: Thomas.PAREAUD at astrium.eads.net (PAREAUD, Thomas)
- [Frama-c-discuss] Logical annotations
- From: Claude.Marche at inria.fr (Claude Marché)
- [Frama-c-discuss] Logical annotations
- From: Thomas.PAREAUD at astrium.eads.net (PAREAUD, Thomas)
- [Frama-c-discuss] Supported features, Global invariants, and POs
- From: eric.jenn at fr.thalesgroup.com (JENN Eric)
- [Frama-c-discuss] A variation domain failed to be computed
- Prev by Date: [Frama-c-discuss] Supported features, Global invariants, and POs
- Next by Date: [Frama-c-discuss] Jessie-Plugin inconsistence between batch- and GUI-mode
- Previous by thread: [Frama-c-discuss] Supported features, Global invariants, and POs
- Next by thread: [Frama-c-discuss] A variation domain failed to be computed
- Index(es):