--- layout: fc_discuss_archives title: Message 65 from Frama-C-discuss on June 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] wp calculus



> 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)

This simple computation is ok as long as you don't have any pointer
neither in the predicate, nor on the instructions that you consider...
which might happen, but is quite rare in C programs...
In fact, even in that case, you'll more probably get :
WP(x = x+1, x < 1) = (x+1 < 1)
or
= let x = x+1 in x<0
because WP makes a kind of "stupid" substitution in the predicate.

>> the algorithms works on single paths so there is no need to calculate
wp for loops...

This is great, because it make things a lot simpler.
But you still have function calls I guess, haven't you ?

Benjamin Monate replied :
> Anne may show some possible outputs on your very example with different
memory models.

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,
the WP can for instance consider 'x' as loading the value stored at x
address (&x) in a memory m state ie. x <--> load (m, &x). And the WP then
computes a new memory state m' which in your case is : store(m, &x, load
(m, &x) + 1).
So you get something like:
WP = load (store(m, &x, load (m, &x) + 1), &x) < 1

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.

At the moment, I am trying to work a different memory models for the new
wp plugin. So, I might be able to provide something that can be useful for
you
if you explain a bit more what your needs are in terms of the kind of
programs you want to deal with.

Best regards,
-- 
Anne.