--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on October 2010 ---
Hi, Sorry I didn't realize this list was english-only. Thank you for the quick reply. I followed your advice, I 'lightened' the annotations a bit, everything goes through except for 2 proofs that are directly related with the 'assigns' clauses in the function 'ones'. I'm attaching the other function this time (allocM function included): /*@ @ requires m > 0 && n >0 ; @ assigns \nothing; @ ensures (\valid(\result + (0..m-1)) && (\forall integer k; 0 <= k < m ==> \valid(\result[k] +(0..n-1) ) ) ); */ float** allocM (int m,int n) { int i = 0; float** p; p= malloc(m *sizeof(float *)); /*@ assert \valid_range(p,0,m-1); */ /*@ assert p != \null; */ /*@ loop assigns p[0..m-1]; @ loop invariant (0 <= i <= m) && (\forall integer k; (0 <= k < i ) ==> \valid(p[k] + (0..n-1)) ); @ loop variant m-i; @ */ for (i = 0; i<m;i++) { /*@ assert 0 <= i < m; */ (p)[i] = malloc(n * sizeof(float)); /*@ assert \valid(p[i] +(0..n-1)); */ } return p; } /*@ requires m > 0 && n > 0; @ @ assigns \nothing; @ ensures \result == \null || (\forall integer i; \forall integer j; @ 0 <= i < m && 0 <= j <n ==> *(\result[i]+j) == 1.0); */ float** ones(int m,int n) { /*@ assert m > 0 && n > 0; */ float **c = allocM(m,n); /*@ assert (\valid(c+ (0..m-1)) && (\forall integer k; 0 <= k < m ==> \valid(c[k] +(0..n-1) ) )) ; */ int i = 0; int j = 0; /*@ loop assigns *(c[0..m-1] + (0..n-1)); @ loop invariant (0 <= i <=m) && (\forall integer k; \forall integer q; (0<= k < i && 0 <= q < n) ==> (*(c[k]+q) == 1.0)) ; @ loop variant m-i ; */ for (i = 0; i<m; i++){ /*@ assert 0<= i < m; */ /*@ assert \valid(c[i]+(0..n-1)); */ /*@ loop assigns *(c[i] +(0..n-1)); @ loop invariant (0 <= j <= n) && (\forall integer l; 0 <= l < j ==> ( *(c[i] + l) == 1.0) ); @ loop variant n-j ; */ for (j = 0; j<n;j++){ /*@ assert 0<=j < n ; */ /*@ assert \valid(c[i]+j); */ *(c[i] + j) = (float) 1.0; } } return c; } the outer loop 'assigns' clause and the one for the function as a whole generate proof obligations that are not handled by any of the provers. The clause in the inner loop is handled. I don't understand why. Thanks in advance, Romain. Quoting Claude Marche <Claude.Marche at inria.fr>: > Hi, > > First of all, please note that it is an english speaking list, do > not send messages in french please. > > A few remarks first: > > * replace each "\forall int" by "\forall integer" and remove each > cast "(float)" in specifications, it will avoid > unnecessary extras casts hence might make prover's life easier > > * your file is not self-contained: NULL undefined, allocM > undeclared. replacing NULL by \null helps. > > * the spec of allocM is crucial for your problems with assigns > clauses since if you expect it to allocate a new block, > you have to specify that. > > * for me, using provers Alt-Ergo, Simplify, Z3 and CVC3, everything > is proved except the VC corresponding > to your main "assigns \nothing" clause. Which is not correct if > allocM is not specified correctly. > > Try to install more provers if needed: see > http://why.lri.fr/provers.en.html > > In particular the preservation of your loop invariants seems to be OK > > Hope this helps, > > - Claude > > On 09/24/2010 06:04 PM, Romain Jobredeaux wrote: >> Bonjour, >> >> Ce message fait suites aux questions d'Alwyn Goodloe de d?but >> juillet sur les boucles imbriqu?es et les tableaux ? dimensions >> multiples (qui comme on l'a fait remarquer pr?c?demment n'en sont >> pas vraiment, puisqu'il s'agit en fait de pointeurs doubles >> pointant sur un tableau de pointeurs). La fonction d'allocation >> passe maintenant toutes les obligations de preuves, mais nous >> rencontrons encore des difficult?s avec la fonction suivante, qui >> alloue une "matrice" de taille m,n et la remplit de 1 : >> >> /*@ requires m > 0 && n > 0; >> @ assigns \nothing; >> @ >> @ ensures \result == NULL || (\forall int i; \forall int j; >> @ 0 <= i < m && 0 <= j <n ==> *(\result[i]+j) == (float) 1.0); >> @*/ >> >> float** ones(int m,int n) >> { >> /*@ assert m > 0 && n > 0; */ >> >> float **c = allocM(m,n); >> >> /*@ assert (\valid(c+ (0..m-1)) && (\forall int k; 0 <= k < m >> ==> \valid(c[k] +(0..n-1) ) )) ; */ >> >> int i = 0; >> int j = 0; >> >> >> /*@ loop assigns *(c[0..m-1]+(0..n-1)); >> @ loop invariant (0 <= i <=m) && (\forall int k; \forall int >> q; (0<= k < i && 0 <= q < n) ==> (*(c[k]+q) == (float) 1.0)) ; >> @ loop variant m-i ; >> */ >> for (i = 0; i<m; i++){ >> /*@ assert 0<= i < m; */ >> /*@ assert \valid(c[i]+(0..n-1)); */ >> >> /*@ loop assigns *(c[i] +(0..n-1)); >> @ loop invariant (0 <= j <= n) && (\forall int l; 0 <= l < j >> ==> ( *(c[i] + l) == (float)1.0) ); >> @ loop invariant \forall int p; \forall int q; (0 <= p <i && >> 0 <= q < n) ==> *(c[p]+q) == \at(*(c[p]+q),Here) ; >> @ loop invariant \forall int p; \forall int q; (i < p <n && 0 >> <= q < n) ==> *(c[p]+q) == \at(*(c[p]+q),Here) ; >> @ loop variant n-j ; >> */ >> for (j = 0; j<n;j++){ >> >> /*@ assert 0<=j < n ; */ >> /*@ assert \valid(c[i]+j); */ >> *(c[i] + j) = (float) 1.0; >> /*@ assert *(c[i] + j) == (float) 1.0; */ >> } >> /*@ assert \forall int l; 0 <= l < n ==> ( *(c[i] + l) == >> (float)1.0) ; */ >> >> >> } >> return c; >> } >> Seules 3 obligations de preuves ne sont pas prouvees >> automatiquement (parmi les 38 de default behavior), et notamment >> l'invariant de boucle exterieure (qui est en fait le plus important >> pour nous) : >> /*@ loop invariant (0 <= i <=m) && (\forall int k; \forall int q; >> (0<= k < i && 0 <= q < n) ==> (*(c[k]+q) == (float) 1.0)) >> >> Les deux autre invariants non prouv?s concernent des conditions de >> type "not_assigns" sur la boucle int?rieure, et apres avoir >> recherch? sur google et dans les manuels des diff?rents outils je >> n'ai trouv? nulle part une description exacte de ce que ces >> conditions signifient... Pouvez-vous m'aider l? aussi ? >> >> Je suis relativement nouveau dans le domaine des methodes >> formelles, et dans l'usage de l'outil, je ne sais donc pas bien >> s'il manque simplement une anotation quelquepart, ou s'il faut >> faire la preuve interactivement.... >> >> Merci de votre aide, >> >> Romain Jobredeaux >> >> >> _______________________________________________ >> 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 > > > -- > 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 | > > > > > > > > > _______________________________________________ > 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 >