Function set_FAT_info

src/fat.c:135–181

@ @ requires \valid(disk_car); @ requires \valid_read(fat_header); @ requires \valid(partition); @ requires \separated(disk_car, fat_header, partition); @*/

  @ requires \separated(disk_car, fat_header, partition);
  @*/
static void set_FAT_info(disk_t *disk_car, const struct fat_boot_sector *fat_header, partition_t *partition)
{
  uint64_t start_fat1;
  uint64_t start_data;
  uint64_t part_size;
  unsigned long int no_of_cluster;
  unsigned long int fat_length;
  const char *buffer=(const char*)fat_header;
  partition->fsname[0]='\0';
  partition->blocksize=fat_sector_size(fat_header)* fat_header->sectors_per_cluster;
  fat_length=le16(fat_header->fat_length)>0?le16(fat_header->fat_length):le32(fat_header->fat32_length);
  part_size=(fat_sectors(fat_header)>0?fat_sectors(fat_header):le32(fat_header->total_sect));
  start_fat1=le16(fat_header->reserved);
  start_data=start_fat1+fat_header->fats*fat_length+(get_dir_entries(fat_header)*32+fat_sector_size(fat_header)-1)/fat_sector_size(fat_header);
  no_of_cluster=(part_size-start_data)/fat_header->sectors_per_cluster;
  if(no_of_cluster<4085)
  {
    partition->upart_type=UP_FAT12;
    snprintf(partition->info, sizeof(partition->info), "FAT12, blocksize=%u", partition->blocksize);
    if(buffer[38]==0x29)	/* BS_BootSig */
    {
      set_part_name_chomp(partition, buffer+FAT1X_PART_NAME, 11);
      if(check_VFAT_volume_name(partition->fsname, 11))
	partition->fsname[0]='\0';
    }
  }
  else if(no_of_cluster<65525)
  {
    partition->upart_type=UP_FAT16;
    snprintf(partition->info, sizeof(partition->info), "FAT16, blocksize=%u", partition->blocksize);
    if(buffer[38]==0x29)	/* BS_BootSig */
    {
      set_part_name_chomp(partition, buffer+FAT1X_PART_NAME, 11);
      if(check_VFAT_volume_name(partition->fsname, 11))
	partition->fsname[0]='\0';
    }
  }
  else
  {
    partition->upart_type=UP_FAT32;
    if(partition->sb_offset==0)
      snprintf(partition->info, sizeof(partition->info), "FAT32, blocksize=%u", partition->blocksize);
    else
      snprintf(partition->info, sizeof(partition->info), "FAT32 found using backup sector, blocksize=%u", partition->blocksize);
    fat32_set_part_name(disk_car,partition,fat_header);
  }
}

/*@
  @ requires \valid_read(fh1);