Numerous frama-c annotations

1 files changed, 9 insertions, 0 deletions

diff --git a/src/ntfs.c b/src/ntfs.c
index afc4c352..ec2c8f64 100644
--- a/src/ntfs.c
+++ b/src/ntfs.c
@@ -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)
   {