--- layout: fc_discuss_archives title: Message 88 from Frama-C-discuss on April 2010 ---
Hi, with //@ lemma help: \forall integer m,n; m>0 && n>0 ==> n <= m*n; it works for me. - Claude Fr?d?ric Gava wrote: > Dear Pascal and Frama-C users, >>> /*@ lemma is_peraps_needed : >>> @ \forall integer m, n; 0<m ==> 0<n ==> n<(m*n); >>> @*/ >>> >> >> Patrick Baudin pointed out to me at lunchbreak that this property is >> false for m=n=1. >> > Thanks Pascal ! (forget this easy case). But the program still > unprovable. Is it due to the use of two pointers on the same aera of > memory ? Note that when (m==1 or m==2 or n==1 or n==2) in the > "requieres", there is no pb. Is it due to a lack of axiom for the > "shift(ppd, 0)" genereted for the only lemma that still have no solution > for provers ? > > #include <limits.h> > > #define SZDBL (sizeof(double)) > > /*@ > requires m>0 && n>0 && m*n*SZDBL<LONG_MAX; > */ > double **matallocd(int m, int n){ > double *pd, **ppd; ppd= (double **)malloc(m*sizeof(double *)); > pd= (double *)malloc(m*n*SZDBL); > ppd[0]=pd; > /*@ assert \valid_range(ppd[0],0,n-1); */ > } > > FG > > > > > > > _______________________________________________ > 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 | http://maps.google.fr/maps?q=48.70963,2.17513+%28Claude+March%C3%A9%27s+Office%29