--- layout: fc_discuss_archives title: Message 57 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



Oups sorry, my mistake :)

I finally succeeded !! Youhou.

Thanks a lot for your help Claude and David.

Arnaud

On Jan 25, 2011, at 5:17 PM, Claude Marche wrote:

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