--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on March 2011 ---
Hello, I am trying to annotate 2 functions (code is included at the end of the message) with very similar structure: or_scalar computes, given a rowB by colB float matrix b and a float a, a new matrix c where c[i][j] == (a!=0 || b[i][j]!=0) equal_scalar computes, given the same parameters, a matrix c where c[i][j]= (a == b[i][j]) The annotations are also very similar, however for some reason alt-ergo proves every obligation on or_scalar, but doesn't even seem to try to prove the outer loop invariant on equal_scalar... Thank you for your help, Romain Jobredeaux /*@ requires rowB > 0 && colB > 0 ; @ requires (\valid(b+ (0..rowB-1)) && (\forall integer k; 0 <= k < rowB ==> \valid(b[k] +(0..colB-1) ) )); @ requires (\valid(c+ (0..rowB-1)) && (\forall integer k; 0 <= k < rowB ==> \valid(c[k] +(0..colB-1) ) )); @ ensures \forall integer i; \forall integer j; (0 <= i < rowB && 0 <=j < colB) ==> (c[i][j] == (a!=0 || b[i][j]!=0)); @*/ int** or_scalar(float a,float** b,int rowB,int colB,int **c) { int i=0,j=0; /*@ loop invariant (0 <= i <= rowB) && (\forall integer l; \forall integer k; (0<=l<colB && 0 <= k <i) ==> @ c[k][l] == (a!=0 || b[k][l]!=0)) ; @ loop variant rowB-i; @*/ while ( i < rowB ) { j=0; /*@ loop invariant (0 <= j <= colB) && (\forall integer k; (0<=k<j) ==> @ c[i][k] == (a!=0 || b[i][k]!=0)) ; @ loop variant colB-j; @*/ while ( j<colB) { c[i][j]= (a!=0) || (b[i][j]!=0); j++; } /*@ assert \forall integer k; 0<=k<colB ==> (c[i][k] == (a!=0 || b[i][k]!=0)) ; */ i++; } return c; } /*@ requires rowB > 0 && colB > 0 ; @ requires (\valid(b+ (0..rowB-1)) && (\forall integer k; 0 <= k < rowB ==> \valid(b[k] +(0..colB-1) ) )); @ requires (\valid(c+ (0..rowB-1)) && (\forall integer k; 0 <= k < rowB ==> \valid(c[k] +(0..colB-1) ) )); @ ensures \forall integer i; \forall integer j; (0 <= i < rowB && 0 <=j < colB) ==> (c[i][j] == (b[i][j]==a)); @*/ int** equal_scalar(float a,float** b,int rowB,int colB,int **c) { int i=0,j=0; /*@ loop invariant (0 <= i <= rowB) && (\forall integer l; \forall integer k; (0<=l<colB && 0 <= k <i) ==> @ c[k][l] == (b[k][l]==a)) ; @ loop variant rowB-i; @*/ while ( i < rowB ) { j=0; /*@ loop invariant (0 <= j <= colB) && (\forall integer k; (0<=k<j) ==> @ c[i][k] == (b[i][k]==a)) ; @ loop variant colB-j; @*/ while ( j<colB) { c[i][j]= (b[i][j] == a); j++; } /*@ assert \forall integer k; 0<=k<colB ==> (c[i][k] == (b[i][k]==a)) ; */ i++; } return c; }