diff options
Diffstat (limited to 'src/ntfs.c')
| -rw-r--r-- | src/ntfs.c | 9 |
1 files changed, 9 insertions, 0 deletions
@@ -184,6 +184,10 @@ int test_NTFS(const disk_t *disk_car, const struct ntfs_boot_sector*ntfs_header, return 0; } +/*@ + @ requires \valid_read(record); + @ assigns \nothing; + @*/ static const ntfs_attribheader *ntfs_getattributeheaders(const ntfs_recordheader* record) { const char* location = (const char*)record; @@ -195,11 +199,16 @@ static const ntfs_attribheader *ntfs_getattributeheaders(const ntfs_recordheader return (const ntfs_attribheader *)location; } +/*@ + @ requires \valid_read(attrib); + @ assigns \nothing; + @*/ static const ntfs_attribheader* ntfs_searchattribute(const ntfs_attribheader* attrib, uint32_t attrType, const char* end, int skip) { if(attrib==NULL) return NULL; /* Now we should be at attributes */ + /*@ loop assigns attrib; */ while((const char *)attrib + sizeof(ntfs_attribheader) < end && le32(attrib->type)!= 0xffffffff) { |