[Frama-c-discuss] Pb with a simple pointer allocation

Frédéric Gava gava at univ-paris12.fr
Thu Apr 29 00:53:30 CEST 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






More information about the Frama-c-discuss mailing list