--- layout: fc_discuss_archives title: Message 83 from Frama-C-discuss on April 2010 ---
Dear Frama-C users, Here a simple program that could not be proved by Alt-Ergo and Z3: #include <limits.h> #define SZDBL (sizeof(double)) /*@ lemma is_peraps_needed : @ \forall integer m, n; 0<m ==> 0<n ==> n<(m*n); @*/ /*@ requires m>0 && n>0 && m*n<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); */ } If someone have a solution... Note that in my true program, I used "ppd[i]= ppd[i-1]+n" forall 1<=i<m Thanks, FG