--- layout: fc_discuss_archives title: Message 87 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 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