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] [Frama-C 0000362]: wrong proof obligation generated ...

  • Subject: [Frama-c-discuss] [Frama-C 0000362]: wrong proof obligation generated ...
  • From: Claude.Marche at inria.fr (Claude Marche)
  • Date: Tue, 05 Jan 2010 13:25:12 +0100
  • In-reply-to: <4B2BBA74.1010508@first.fraunhofer.de>
  • References: <4B2A68AD.3070207@first.fraunhofer.de> <4B2B4952.4020701@inria.fr> <4B2BBA74.1010508@first.fraunhofer.de>
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                    |