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: Claude.Marche at inria.fr (Claude Marche)
- Date: Fri, 09 Jul 2010 11:02:12 +0200
- In-reply-to: <AANLkTiks0DlWKcNQZx8jW7Bqep5CEyLfxvHIllTn9jOH@mail.gmail.com>
- References: <AANLkTinmh3pzyUOUK6SLwPfw27EHfoQ915TbNulf-VPF@mail.gmail.com> <1278509062.3060.77.camel@iti27> <AANLkTiks0DlWKcNQZx8jW7Bqep5CEyLfxvHIllTn9jOH@mail.gmail.com>
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 |
- References:
- [Frama-c-discuss] questions after attempting to use jessie on a matrix library
- From: agoodloe at gmail.com (Alwyn Goodloe)
- [Frama-c-discuss] questions after attempting to use jessie on a matrix library
- From: hollas at informatik.htw-dresden.de (Boris Hollas)
- [Frama-c-discuss] questions after attempting to use jessie on a matrix library
- From: agoodloe at gmail.com (Alwyn Goodloe)
- [Frama-c-discuss] questions after attempting to use jessie on a matrix library
- Prev by Date: [Frama-c-discuss] Problem with loop invariant
- Next by Date: [Frama-c-discuss] *p and p[0]
- Previous by thread: [Frama-c-discuss] questions after attempting to use jessie on a matrix library
- Next by thread: [Frama-c-discuss] *p and p[0]
- Index(es):