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

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