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