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