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] \at in ACSL assertions
- Subject: [Frama-c-discuss] \at in ACSL assertions
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- Date: Wed, 8 Dec 2010 21:21:16 +0100
- In-reply-to: <4CFFBC39.7080403@enseeiht.fr>
- References: <AANLkTimyk_961c8Xk6_U33TAxabBGSeoaRB+EtM-OiBR@mail.gmail.com> <4CFFBC39.7080403@enseeiht.fr>
Hello, On Wed, Dec 8, 2010 at 6:11 PM, Jorge Luis Honorat Poblette <jorge.honoratpoblette at enseeiht.fr> wrote: > Hello Pascal I am flattered but there are a lot of competent people other than me on this list, or for that matter, at IRIT. > im working with abstract interpretation and weakest > precondition analysis, I saw your email info on the mailing list of frama-c > and I would like to ask you if maybe you know if C constructs ?as loops and > "ifs" structures can be splited to generate this anlysis, I am sorry, I do not know how to say this, but I do not understand anything of your question. You are saying that you are working with abstract interpretation and weakest preconditions, which are two distinct techniques (inasmuch as any static analysis technique is not a particular instance of abstract interpretation). You do not say if you are using these techniques or trying to implement them. In the second case, I recommend you pick one: it should be enough to keep you busy for a couple of years if you try to do it right. I assume you are asking about splitting loops and ifs to generate this analysis (which one?), but I do not see what this can possibly mean. And this is somehow in the context of the discussion of the \at ACSL construct. Or perhaps not. Frankly, I can't tell. I you are asking about WP/AI in general, this is not a very good place, especially considering that you can find experts locally. In case you are asking about using Frama-C, then this is the appropriate place, but you really need to tell us what plug-in(s) you are using, and how, and what result you wish to obtain. Use an example and ask someone to proofread your message if you have to. Pascal
- References:
- [Frama-c-discuss] \at in ACSL assertions
- From: jorge.honoratpoblette at enseeiht.fr (Jorge Luis Honorat Poblette)
- [Frama-c-discuss] \at in ACSL assertions
- Prev by Date: [Frama-c-discuss] \at in ACSL assertions
- Next by Date: [Frama-c-discuss] Carbon release
- Previous by thread: [Frama-c-discuss] \at in ACSL assertions
- Next by thread: [Frama-c-discuss] Carbon release
- Index(es):