--- layout: fc_discuss_archives title: Message 4 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



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