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