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

[Claude Marche]

Hi,

with

//@ lemma help: \forall integer m,n; m>0 && n>0 ==> n <= m*n;

it works for me.

- Claude

Frédéric Gava wrote:
> 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
> 
> 
> 
> 
> 
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-- 
Claude Marché                          | tel: +33 1 72 92 59 69
INRIA Saclay - Île-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Université                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - Bâtiment N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |
http://maps.google.fr/maps?q=48.70963,2.17513+%28Claude+March%C3%A9%27s+Office%29