--- layout: fc_discuss_archives title: Message 59 from Frama-C-discuss on November 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C labels/States



Skipped content of type multipart/alternative-------------- next part --------------

/*@ axiomatic InterInv1 {
  @ predicate interInv{L1,L2}
  @               (int i, unsigned char *indata_i, unsigned char *outdata_i,unsigned char x_i, 
  @               unsigned char y_i, unsigned char *d_i, unsigned char tx_i, unsigned char ty_i,
  @               unsigned char *dkey_i,
  @               unsigned char *indata_f, unsigned char *outdata_f,unsigned char x_f, 
  @               unsigned char y_f, unsigned char *d_f, unsigned char tx_f, unsigned char ty_f,
  @               unsigned char *dkey_f,int j, unsigned long len); }
  @ axiomatic InterInv2 {
  @ axiom interInv_ind{L1,L2}:
  @         \forall int i, unsigned char *indata_i, unsigned char *outdata_i, unsigned char x_i,
  @                     unsigned char y_i, unsigned char *d_i,unsigned char tx_i, unsigned char ty_i,unsigned char *dkey_i,
  @                 unsigned char *indata_f, unsigned char *outdata_f, 
  @                     unsigned char x_f, unsigned char y_f, unsigned char *d_f,
  @                     unsigned char tx_f, unsigned char ty_f,unsigned char *dkey_f,
  @                     int j, unsigned long len;
  @     (\at(x_f,L2) == ((\at(x_i,L1)+1)&0xff) &&
  @         \at(tx_f,L2)== \at(d_i[x_f],L1) && 
  @         \at(y_f,L2) == ((\at(tx_f,L2)+ \at(y_i,L1))&0xff) &&
  @         \at(ty_f,L2)== \at(d_i[y_f],L1) &&
  @         \at(d_f[x_f],L2)== \at(ty_f,L2) &&
  @         \at(d_f[y_f],L2) == \at(tx_f,L2) && 
  @         \at(dkey_f[((len>>3L)-j)*i],L2) == \at(d_f[(tx_f+ty_f)&0xff],L2) &&
  @         \at(outdata_f[i],L2) == (\at(d_f[(tx_f+ty_f)&0xff],L2) ^ \at(indata_f[i],L2)) &&
  @         \at(indata_f[i],L2) == \at(indata_i[i],L2)) ==>
  @         interInv{L1,L2}(i,indata_i,outdata_i,x_i,y_i,d_i,tx_i,ty_i,dkey_i,
  @                     indata_f,outdata_f,x_f,y_f,d_f,tx_f,ty_f,dkey_f,j,len);
  @ }
  @*/
   
 /*@ requires \valid_range(indata,0,len) &&
   @          \valid_range(outdata,0,len) &&
   @        0<=i<=len &&
   @          \valid_range(d,0,255) &&
   @          \valid_range(dkey,0,len);
   @ ensures
   @      interInv{Old,Here}(i,indata,outdata,x,y,d,tx,ty,dkey,indata,outdata,x,y,d,tx,ty,dkey,j,len);
   @*/
 void LOOP(int i, unsigned char x, unsigned char y,unsigned char tx, unsigned char ty,
               unsigned char *d, unsigned char *outdata, unsigned char *indata, unsigned char *dkey,
               int j, const unsigned long len)
 {
  
      x=((x+1)&0xff); 
      tx=d[x]; 
      y=((tx+y)&0xff); 
      ty=d[y]; 
      d[x]= ty;
      d[y]=tx; 
      dkey[((len>>3L)-j)*i] = d[(tx+ty)&0xff];
      (outdata[i]) = (d[(tx+ty)&0xff] ^ (indata[i]));
      
   /*@ ghost goto L; */
   /*@ ghost L:*/ 
   
      /*@ assert
        @         interInv{Pre,L}(i,indata,outdata,x,y,d,tx,ty,dkey,indata,outdata,x,y,d,tx,ty,dkey,j,len);
        @*/
 }