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

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                    |