--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on July 2010 ---
[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                    |