# 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] Verifications of calls to unannotated functions

*Subject*: [Frama-c-discuss] Verifications of calls to unannotated functions*From*: Claude.Marche at inria.fr (Claude Marche)*Date*: Mon, 01 Feb 2010 17:10:45 +0100*In-reply-to*: <FC0686BB6178BC43B9DC035287A11A720DEDF3E52B@SI-MBX12.de.bosch.com>*References*: <FC0686BB6178BC43B9DC035287A11A720DEDF3E36A@SI-MBX12.de.bosch.com> <4B66E2B0.6010302@cea.fr> <20100201155523.703e6289@is010235> <FC0686BB6178BC43B9DC035287A11A720DEDF3E52B@SI-MBX12.de.bosch.com>

Hollas Boris (CR/AEY1) wrote: > > However, I see a problem with a postcondition \true: Assume you have statements S; T in the code where S is a call of an unannotated function and T is some statement. Further, assume the verifier has shown {P} T {Q}, where P = wp(T,Q) is the weakest precondition of T wrt Q. Then, the verifier has to show that true -> P is valid, which means it has to show that P is valid. The problem I see is that the verifier will fail here. > > Maybe the verifier works differently? > Your remark would be true if the default assigns was "everything", but as said in previous mails it is not the case. If f() assigns \nothing, then you just need to prove P before the call to f(). Generally speaking, to prove that an assertion P is true after a method call f(...), what you need to prove is as follows. let me write S |= p to mean "program p runs correctly in memory state S". Thus to prove S |= f(...) {P}, you need to prove 1) S |= Pre(f) 2) for any memory state S' such that assigns(S,S',Locs(f)) and S' |= Post(f), S' |= P. here Locs(f) denotes the assigns clause for f, and assigns(S,S',Locs(f)) means "any memory location not in Locs(f) are the same in S and S'" Turning this into a rule for WP calculus needs to make precise the memory model. But if we assume a simple memory model represented by a variable Heap (thus *p is select(Heap,p), *p = v is Heap := store(Heap,p,v)) then you can say WP(f(),P)(H) = Pre(f) /\ forall H', (assigns(H,H',Locs(f)) && Post(f)(H')) ==> P(H') If Locs(f) is the empty set ("assigns \nothing"), then assigns(H,H',Locs(f)) reduces to H=H', and the whole reduces to WP(f(),P)(H) = Pre(f) /\ (Post(f)(H) ==> P(H)) If Post(f) is true, it reduces to WP(f(),P)(H) = Pre(f) /\ P(H) hence you have to prove both Pre(f) and P in the pre-state. Does it helps ? I'm not sure it was your question... - Claude -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |

**References**:**[Frama-c-discuss] Verifications of calls to unannotated functions***From:*Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))

**[Frama-c-discuss] Verifications of calls to unannotated functions***From:*Patrick.Baudin at cea.fr (BAUDIN Patrick)

**[Frama-c-discuss] Verifications of calls to unannotated functions***From:*virgile.prevosto at cea.fr (Virgile Prevosto)

**[Frama-c-discuss] Verifications of calls to unannotated functions***From:*Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))

- Prev by Date:
**[Frama-c-discuss] Verifications of calls to unannotated functions** - Next by Date:
**[Frama-c-discuss] Verifications of calls to unannotated functions** - Previous by thread:
**[Frama-c-discuss] Verifications of calls to unannotated functions** - Next by thread:
**[Frama-c-discuss] Verifications of calls to unannotated functions** - Index(es):