--- layout: fc_discuss_archives title: Message 57 from Frama-C-discuss on January 2011 ---
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