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