--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on January 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Frama-C 0000362]: wrong proof obligation generated ...



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                    |