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

[Frama-c-discuss] Frama-c-discuss Digest, Vol 32, Issue 12



On 01/25/2011 02:02 PM, Arnaud Dieumegard wrote:
> This helps !
>
> I manage to create some lemmas that allows me to prove the program:
>
> //@	lemma diff_point_prop: *(vect.a) != *(vect.Sum)&&  *(vect.b) != *(vect.Sum);
>
> or
>
> //@	lemma diff_prop: \forall UINT8 m, UINT8 n; 0<= m<  3&&  0<= n<  3 ==>  vect.a[m] != vect.Sum[n]&&  vect.b[m] != vect.Sum[n];
>
>    

Ouch! You confuse t[i] and t+i, this is certainly a mistake

Anyway, you should not introduce lemmas but a predicate, e.g

/*@ predicate valid_struct_S(struct S *s) =
          \valid_range(s->a,0,2) && \valid_range(s->b,0,2) &&
          \forall integer i,j; 0 <= i < 3 && 0 <= j < 3 ==> s->a+i != 
s->b+j ;
*/

and then use

/*@ requires valid_struct(&vect)
        ....

- Claude


> I only need one of them to prove the program.
> But a problem still exists:
> I cannot prove the lemmas ! (But it's normal).
>
> Maybe it will be better to assume this in the function contract.
>
> Arnaud
>
> On Jan 25, 2011, at 11:19 AM, Claude Marche wrote:
>
>    
>> Hi all,
>>
>> Sorry but I have currently very little time to answer on such a question on a specific program
>>
>> Quick guess: Jessie poorly supports arrays embedded in structs and behaves like it was
>> a pointer to another array, e.g.
>>
>> struct S {
>>   int a[3]
>> }
>>
>> handle as it was
>>
>> struct S {
>>   int *a;
>> }
>>
>>
>> this explains why you need to specify \valid_range(a,0,2) even if it is obvious.
>>
>> Similarly, for two array fields a and b you should say something like
>>
>>
>> forall i ,j  0<= i<= 3&&  0<= j<= 3 ==>   a+i != b+j
>>
>> to tell that a and b do not point to the same array
>>
>> Hope this helps,
>>
>> - Claude
>>
>>
>> On 01/25/2011 09:20 AM, Arnaud Dieumegard wrote:
>>      
>>> Hi all,
>>>
>>> I tried to prove my program without the struct and it succeeded !!!
>>>
>>> Maybe I have to create some logic specification for the struct ?
>>> Or something to help the solver to understand what is on the structure.
>>>
>>> You could find enclosed the new c-code.
>>>
>>> I will now try to add some "structure specification".
>>>
>>>
>>>
>>>
>>>
>>> Arnaud
>>>
>>> On Jan 24, 2011, at 9:05 PM, David MENTRE wrote:
>>>
>>>
>>>        
>>>> Hello,
>>>>
>>>> 2011/1/24 David MENTRE<dmentre at linux-france.org>:
>>>>
>>>>          
>>>>> Yes. Please find attached a variation of Arnaud's program that
>>>>> compiles and runs under Jessie.
>>>>>
>>>>> I really don't understand why the assert in the for() loop of function
>>>>> f() (VC 6.) is not proved.
>>>>>
>>>>> I'm using Frama-C Boron with Alt-Ergo 0.91.
>>>>>
>>>>>            
>>>> I still cannot prove the assertion with Frama-C Carbon beta 2, Why
>>>> 2.28 and Alt-ergo 0.91[1]. The problem is probably in the assertion
>>>> itself, but I don't see where.
>>>>
>>>> Regards,
>>>> d.
>>>>
>>>> [1] And a slight modification on annotations, see attached C file.
>>>> <dieumegard-case2.c>_______________________________________________
>>>> Frama-c-discuss mailing list
>>>> Frama-c-discuss at lists.gforge.inria.fr
>>>> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>>>>
>>>>          
>>>
>>> Cordialement,
>>>
>>> Arnaud Dieumegard
>>> Research engineer
>>> IRIT / ACADIE
>>> arnaud.dieumegard at enseeiht.fr
>>>
>>>
>>>
>>>
>>>
>>> _______________________________________________
>>> Frama-c-discuss mailing list
>>> Frama-c-discuss at lists.gforge.inria.fr
>>> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>>>        
>>
>> -- 
>> 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                    |
>>
>>
>>
>>
>>
>>
>>
>>
>> _______________________________________________
>> Frama-c-discuss mailing list
>> Frama-c-discuss at lists.gforge.inria.fr
>> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>>      
> Cordialement,
>
> Arnaud Dieumegard
> Research engineer
> IRIT / ACADIE
> arnaud.dieumegard at enseeiht.fr
>
>
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>    


-- 
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                    |