diff --git a/src/fat_common.c b/src/fat_common.c
index 25460267..cb4e6c28 100644
--- a/src/fat_common.c
+++ b/src/fat_common.c
@@ -31,13 +31,25 @@
 #include "fat_common.h"
 
 unsigned int fat_sector_size(const struct fat_boot_sector *fat_header)
-{ return (fat_header->sector_size[1]<<8)+fat_header->sector_size[0]; }
+{
+  const unsigned int res=(fat_header->sector_size[1]<<8)+fat_header->sector_size[0];
+  /*@ assert res <= 65535; */
+  return res;
+}
 
 unsigned int get_dir_entries(const struct fat_boot_sector *fat_header)
-{ return (fat_header->dir_entries[1]<<8)+fat_header->dir_entries[0]; }
+{
+  const unsigned int res=(fat_header->dir_entries[1]<<8)+fat_header->dir_entries[0];
+  /*@ assert res <= 65535; */
+  return res;
+}
 
 unsigned int fat_sectors(const struct fat_boot_sector *fat_header)
-{ return (fat_header->sectors[1]<<8)+fat_header->sectors[0]; }
+{
+  const unsigned int res=(fat_header->sectors[1]<<8)+fat_header->sectors[0];
+  /*@ assert res <= 65535; */
+  return res;
+}
 
 unsigned int fat_get_cluster_from_entry(const struct msdos_dir_entry *entry)
 {
diff --git a/src/fat_common.h b/src/fat_common.h
index 1a07f76c..2b43e79f 100644
--- a/src/fat_common.h
+++ b/src/fat_common.h
@@ -136,6 +136,7 @@ struct msdos_dir_slot {
 
 /*@
   @ requires \valid_read(entry);
+  @ requires \initialized(entry);
   @ assigns \nothing;
   @ */
 unsigned int fat_get_cluster_from_entry(const struct msdos_dir_entry *entry);
@@ -148,18 +149,24 @@ int is_fat_directory(const unsigned char *buffer);
 
 /*@
   @ requires \valid_read(fat_header);
+  @ requires \initialized(fat_header);
+  @ ensures \result <= 65535;
   @ assigns \nothing;
   @ */
 unsigned int get_dir_entries(const struct fat_boot_sector *fat_header);
 
 /*@
   @ requires \valid_read(fat_header);
+  @ requires \initialized(fat_header);
+  @ ensures \result <= 65535;
   @ assigns \nothing;
   @ */
 unsigned int fat_sector_size(const struct fat_boot_sector *fat_header);
 
 /*@
   @ requires \valid_read(fat_header);
+  @ requires \initialized(fat_header);
+  @ ensures \result <= 65535;
   @ assigns \nothing;
   @ */
 unsigned int fat_sectors(const struct fat_boot_sector *fat_header);