# 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

*Subject*: [Frama-c-discuss] wp calculus*From*: Anne.Pacalet at sophia.inria.fr (Anne.Pacalet at sophia.inria.fr)*Date*: Mon, 22 Jun 2009 15:34:40 +0200 (CEST)*In-reply-to*: <4A3F6BDE.2000209@cea.fr>*References*: <2f03c2a30906201048q4451387auebb1aa9859a38b73@mail.gmail.com> <4A3F52A2.4080800@sophia.inria.fr> <2f03c2a30906220407n3f480efdx3cc62cfe04f0fc59@mail.gmail.com> <4A3F6BDE.2000209@cea.fr>

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

**Follow-Ups**:**[Frama-c-discuss] wp calculus***From:*mauro at bglug.it (Mauro Baluda)

**References**:**[Frama-c-discuss] wp calculus***From:*mauro at bglug.it (Mauro Baluda)

**[Frama-c-discuss] wp calculus***From:*anne.pacalet at sophia.inria.fr (Anne Pacalet)

**[Frama-c-discuss] wp calculus***From:*mbaluda at gmail.com (Mauro Baluda)

**[Frama-c-discuss] wp calculus***From:*benjamin.monate at cea.fr (Benjamin Monate)

- Prev by Date:
**[Frama-c-discuss] wp calculus** - Next by Date:
**[Frama-c-discuss] wp calculus** - Previous by thread:
**[Frama-c-discuss] wp calculus** - Next by thread:
**[Frama-c-discuss] wp calculus** - Index(es):