# 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 01:00:05 -0400

In my first trials with frama-c's jessie plugin, I'm trying to use Frama-C/Jessie to verify a simple library of matrix operations, but I have a few questions. We will consider two of the simplest functions. The first simply allocates space for a m x n matrix. It seems that the spec should be /*@ @ requires m > 0 && n >0 ; @ assigns \result; @ ensures \valid(\result) && (\forall int i; @ 0<= i < m ==> \valid(\result+i*n + (0..n-1))); */ I've annotated the program as follows: double** allocM (int m,int n) { int i = 0; double** p; p= malloc(m *sizeof(double *)); /*@ assert \valid(p+ (0..m-1)); */ if (p == NULL) { printf("out of memory\n"); return NULL; } /*@ loop invariant \forall int k; @ 0 <= k < i <=m ==> \valid(p+k*n+ (0..n-1)); @ loop variant m-i; @ */ for (i = 0; i<m;i++) { if (i < 0) break; /*@ assert 0 <= i <= m; */ (p)[i] = malloc(n * sizeof(double *)); /*@ assert \valid(p+i*n+(0..n-1)); */ if((p)[i] == NULL) { return NULL; } } return p; } ================================== The first question I have is this the right way to use \valid in this context. ============================= The second example is equally simple it simply creates nxm matrix of ones. Initially, my first thought was that it should be annotated something like : /*@ requires m > 0 && n > 0; @ assigns \result; @ ensures \valid(\result); @ ensures \forall int i; \forall int j; @ 0 <= i < m && 0 <= j <n ==> \result[i][j] == 1; @*/ double** ones(int m,int n) { /*@ assert m > 0 && n > 0; */ double **c = allocM(m,n); /*@ assert \valid(c); */ int i,j; /*@ loop assigns c[0..m-1][0..n-1]; @ loop invariant \forall int k; \forall int l; @ (0<= i <=m && 0 <= j <= n) && ( 0 <= k < i && 0 <= l < j ==> c[k][l] == 1); @*/ for (i = 0; i<m; i++){ for (j = 0; j<n;j++){ c[i][j] = 1; /*@ assert c[i][j] == 1; */ } } return c; } ====================== I didn't see any nested loop examples or multidimensional array examples so I'm doing things a bit by trial and error. From my first trials it seems like you have to annotate each of the nested loops separately?? I'm wondering if even simple nested loops is too much for the automated provers because even after playing with the invariant locations, the automated provers couldn't discharge even the simple loop invariant. I don't mind going to interactive proof, but just wanted any feedback I could get. Based on a dereferencing obligation is seems I need to show \valid c[i][j] or actually something like \valid(c +i*m+j) before the c[i][j] dereference??? I'm sure these questions are a bit silly but this really my first real try with this tool. ================== Any help is appreciated. -- 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/ece4224e/attachment.htm>

**Follow-Ups**:**[Frama-c-discuss] questions after attempting to use jessie on a matrix library***From:*hollas at informatik.htw-dresden.de (Boris Hollas)

- Prev by Date:
**[Frama-c-discuss] newbie Jessie config question** - Next by Date:
**[Frama-c-discuss] questions after attempting to use jessie on a matrix library** - Previous by thread:
**[Frama-c-discuss] newbie Jessie config question** - Next by thread:
**[Frama-c-discuss] questions after attempting to use jessie on a matrix library** - Index(es):