--- layout: fc_discuss_archives title: Message 59 from Frama-C-discuss on November 2008 ---
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); @*/ }