--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on July 2010 ---
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. -- Best regards, Boris Hollas