diff options
Diffstat (limited to 'src/exfatp.c')
| -rw-r--r-- | src/exfatp.c | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/exfatp.c b/src/exfatp.c index 06c24ec2..edcb36a2 100644 --- a/src/exfatp.c +++ b/src/exfatp.c @@ -37,9 +37,14 @@ #include "log.h" #include "fat.h" +/*@ + @ requires \valid_read(buffer + ( 0 .. size-1)); + @ assigns \nothing; + @*/ static struct exfat_alloc_bitmap_entry *exfat_get_bitmap(unsigned char*buffer, const unsigned int size) { unsigned int i; + /*@ loop assigns i; */ for(i=0; i<size; i+=0x20) if(buffer[i]==0x81) return (struct exfat_alloc_bitmap_entry *)&buffer[i]; |