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