--- layout: fc_discuss_archives title: Message 66 from Frama-C-discuss on June 2009 ---
[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