--- layout: fc_discuss_archives title: Message 87 from Frama-C-discuss on April 2010 ---
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