--- layout: fc_discuss_archives title: Message 83 from Frama-C-discuss on April 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



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