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