--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on January 2010 ---
Dear Jochen, I took a little time to look at your code. Indeed your analysis is good, the problem is that the lemma "cnt(b,n,x) depends only on the elements b[0..n)", even obvious for you, is not for the provers. Even worse, since, as you say, you need induction on n to prove it, they can't prove it because none of them perform induction. Such a lemma is related to the analysis of memory separation, and computation of the so-called "footprint" of a formula. this kind of problem is dealt elegantly by separation logic, but such a logic is not available in Frama-C/Jessie. Fortunately there are a few work-around. In your case, you can specify the footprint of cnt by using the "reads" clause: /*@ axiomatic cnt_axioms { logic integer cnt{L}(int* a, integer n, int val) reads a[0..n-1] ; .... */ Then, after adding "requires n>=0", because otherwise your loop invariant i <= n is wrong, I managed to prove everything by Simplify. (other provers, although more modern, seem less powerful...) The effect of the reads clause is more or less to automatically generate the needed lemma - Claude Jochen Burghardt wrote: > Claude Marche wrote: >> Jochen Burghardt wrote: >>> >>> Dear Claude Marche, >>> >>> yesterday, I replied to a mail from the bug-tracking system, >>> adressing my mail to benjamin.monate at cea.fr who was referred to in >>> the mail header. Today, I recognized on the bug-tracker www-page >>> that you are referred to as the author of that mail I replied to. >>> >>> So I forward my yesterday reply to you. Please apologize the >>> inconvenience. >>> >>> Best regards >>> Jochen Burghardt >>> >> You're right, I misunderstood the problem at first. I thought you had >> a VC that was proved whereas is was not supposed to hold, but it was >> not a soundness problem. >> >> The phenomenon you have is a consequence of the region analysis that >> is performed during the process of VC generation. In the >> assertion >> >> //@ assert \forall int *c; s{Here}(c,8) == s{M}(c,8); >> >> the pointer c is not related to anything in the program. As a >> consequence it is considered to lie in a memory region that is >> disjoint from anything else. And consequently, the equality is >> translated as the trivial s(c,8,result) == s(c,8,result); because the >> program does not modify >> the memory region in question. >> >> Those issues are discussed in Y. Moy Phd thesis >> http://www.lri.fr/~marche/moy09phd.pdf >> >> A solution might be the deactivated the region analysis, but I'm not >> sure it is the right way. The main problem to me is that assertion is >> a non-sense: you quantify over *any* pointer, which does not make >> sense to me. >> >> My guess is that you did not specify your problem the right way: >> Could you explain what you wanted to do originally ? >> >> - Claude > (Answer see attached file; its line numbers, starting from 1, are used > as file-internal references, be careful not to insert or delete lines) > > -- 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 |