--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on April 2011 ---
Hi all, Working on the function given at the end of this e-mail, I can't seem to manage to prove one of the VCs regarding the inner loop with the jessie plugin... I'm wondering if there is an aliasing issue here (i.e. a problem would rise if p[i] and p[j] point to the same location with i!=j). Thank you for your help, Romain J. /*@ requires rowA > 0 && colA > 0 ; @ requires (\valid(a+ (0..rowA-1)) && (\forall integer k; 0 <= k < rowA ==> \valid(a[k] +(0..colA-1) ) )) ; @ requires (\valid(p+ (0..colA-1)) && (\forall integer k; 0 <= k < colA ==> \valid(p[k] +(0..rowA-1) ))) ; @ ensures (\forall integer i; \forall integer j; (0 <= i < rowA && 0 <=j < colA) ==> (p[j][i] == a[i][j])); @*/ float** transpose(float** a,int rowA,int colA, float **p) { int i=0,j=0; /*@ loop invariant (0<=j<=colA) && (\forall integer k;\forall integer l;((0 <= l < rowA)&&(0<=k< j))==>(p[k][l]==a[l][k])); @ loop variant colA-j; */ while (j<colA) { i=0; /*@ loop invariant (0<=i<=rowA) && (\forall integer k;(0<=k<i) ==> (p[j][k]==a[k][j])) @ && (\forall integer k;\forall integer l;((0<=l<rowA) && (0<=k<j)) ==> (p[k][l]==a[l][k])); @ loop variant rowA-i; */ while (i<rowA) { p[j][i] = a[i][j]; i++; } j++; } return p; }