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

  • Subject: [Frama-c-discuss] questions after attempting to use jessie on a matrix library
  • From: agoodloe at gmail.com (Alwyn Goodloe)
  • Date: Wed, 7 Jul 2010 11:17:48 -0400
  • In-reply-to: <1278509062.3060.77.camel@iti27>
  • References: <AANLkTinmh3pzyUOUK6SLwPfw27EHfoQ915TbNulf-VPF@mail.gmail.com> <1278509062.3060.77.camel@iti27>
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> 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.
>
>
>
> --
> Best regards,
> Boris Hollas
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>



-- 
Alwyn E. Goodloe, Ph.D.
agoodloe at gmail.com

Computer Scientist
National Institute of Aerospace
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100707/64b28692/attachment.htm>