Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] questions after attempting to use jessie on a matrix library

Alwyn Goodloe wrote:
> Boris,
>
>   THANKS for the help. How silly of me to screw up the postcondition!!!!
>   
>    After consulting the wiki it seems that  the way around the problem
> of lack of support for multidimensional arrays is to do everything 
> with pointer arithmetic at least that's what I inferred.   This may 
> make it not the right tool
> for verifying that little library,  but I have a couple of other 
> applications for frama-C/Jessie in mind.
>
>    I sometimes use splint so good suggestion.
>  
> Alwyn
>
>  
> On Wed, Jul 7, 2010 at 9:24 AM, Boris Hollas 
> <hollas at informatik.htw-dresden.de 
> <mailto:hollas at informatik.htw-dresden.de>> wrote: 
>
>     On Wed, 2010-07-07 at 01:00 -0400, Alwyn Goodloe wrote:
>
>     > /*@
>     >   @ requires m > 0 && n >0 ;
>     >   @ assigns \result;
>     >   @ ensures \valid(\result) && (\forall int i;
>     >   @   0<= i < m  ==>  \valid(\result+i*n + (0..n-1)));
>     >  */
>
>     >               return NULL;
>     > ==================================
>     > The first question I have is this the right way to use
>     > \valid in this context.
>     > =============================
>
>     Since your function may return a NULL pointer, the postcondition
>     doesn't
>     hold.
>
>     Also, there's a potential risk of dangling pointers in your
>     program. As
>     far as I know, the absence of dangling pointers cannot be verified
>     with
>     Jessie. You may consider the tool splint for that purpose.
>
>     >  I didn't see any nested loop examples or multidimensional array
>     > examples
>
>     They are not yet supported. See the wiki on how to circumvent the
>     problem.
>

As far as I understand, your example does not involve any 
multi-dimensional arrays
like

int t[100][10];

but a 1-dimensional array whose cells are pointers to other 
1-dimensional arrays. The latter
is supported by Jessie.

What is missing in your example is probably a proper loop invariant on 
the internal loop.

- Claude

-- 
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                    |