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