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] wp calculus

On Mon, Jun 22, 2009 at 3:34 PM, <Anne.Pacalet at sophia.inria.fr> wrote:
>> Mauro Baluda wrote :
>>> what I need is to obtain the precondition that guarantees that the
> execution of a given C statement brings the program in a state
>>> fullfilling a given C (if possible) predicate... ex:
>>> WP(x = x+1, x < 1) =(x<0)

we take care of aliasing dynamically... because we are executing tests
we know what pointers are pointing to during the analysis
this is described in the paper but I assure you I don't need the WP to
take care of pointers directly

> In fact, even in that case, you'll more probably get :
> WP(x = x+1, x < 1) = (x+1 < 1)

this is perfectly fine

> or
> = let x = x+1 in x<0
> because WP makes a kind of "stupid" substitution in the predicate.

I just need the stupid substitution!

> But you still have function calls I guess, haven't you ?
I'll consider function calls in the future but this shouldn't impact on WP

> As Benjamin said, you can use different memory models according to the
> kind of computation you are dealing with. In a general case with pointers
...
> Of course, in your simple example, it still leads to something equivalent
> to (x<0), but this is to show that the computations are not always so
> trivial.

I'll think about that but as I told you I don't think this will be
critical in my case

Mauro
-- 
Computer science is no more about computers than astronomy is about telescopes
    - Edsger W. Dijkstra