Check if the block looks like an indirect/double-indirect block */ @ @ requires blocksize >= 8; @ requires \valid_read(buffer + (0 .. blocksize-1)); @ assigns \result; @*/
| 71 | @ assigns \result; |
| 72 | @*/ |
| 73 | static inline int ind_block(const unsigned char *buffer, const unsigned int blocksize) |
| 74 | { |
| 75 | const uint32_t *p32=(const uint32_t *)buffer; |
| 76 | unsigned int i; |
| 77 | unsigned int diff=1; /* IND: Indirect block */ |
| 78 | if(le32(p32[0])==0) |
| 79 | return 0; |
| 80 | if(le32(p32[1])==le32(p32[0])+blocksize/4+1) |
| 81 | diff=blocksize/4+1; /* DIND: Double Indirect block */ |
| 82 | /*@ |
| 83 | @ loop assigns i; |
| 84 | @*/ |
| 85 | for(i=0;i<blocksize/4-1 && le32(p32[i+1])!=0;i++) |
| 86 | { |
| 87 | if(le32(p32[i+1])!=le32(p32[i])+diff) |
| 88 | { |
| 89 | return 0; |
| 90 | } |
| 91 | } |
| 92 | i++; |
| 93 | /*@ |
| 94 | @ loop assigns i; |
| 95 | @*/ |
| 96 | for(;i<blocksize/4 && le32(p32[i])==0;i++); |
| 97 | if(i<blocksize/4) |
| 98 | { |
| 99 | return 0; |
| 100 | } |
| 101 | return 1; /* Ok: ind_block points to non-fragmented block */ |
| 102 | } |
| 103 | |
| 104 | #endif |
no outgoing calls
no test coverage detected