--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on April 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] potential aliasing problem



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;
}