Function fat32_set_part_name

src/fat.c:83–127

@ @ requires \valid(disk_car); @ requires valid_disk(disk_car); @ requires \valid(partition); @ requires valid_partition(partition); @ requires \valid_read(fat_header); @ requires \separated(disk_car, partition, fat_header); @ decreases 0; @*/

  @ decreases 0;
  @*/
static int fat32_set_part_name(disk_t *disk_car, partition_t *partition, const struct fat_boot_sector*fat_header)
{
  partition->fsname[0]='\0';
  if((fat_header->sectors_per_cluster>0)&&(fat_header->sectors_per_cluster<=128))
  {
    const unsigned int cluster_size=fat_header->sectors_per_cluster*disk_car->sector_size;
    unsigned char *buffer=(unsigned char*)MALLOC(cluster_size);
    if((unsigned)disk_car->pread(disk_car, buffer, cluster_size,
	  partition->part_offset + (le16(fat_header->reserved) + fat_header->fats * le32(fat_header->fat32_length) + (uint64_t)(le32(fat_header->root_cluster) - 2) * fat_header->sectors_per_cluster) * disk_car->sector_size) != cluster_size)
    {
#ifndef DISABLED_FOR_FRAMAC
      log_error("fat32_set_part_name() cannot read FAT32 root cluster.\n");
#endif
    }
    else
    {
      int i;
      int stop=0;
      for(i=0;(i<16*fat_header->sectors_per_cluster)&&(stop==0);i++)
      { /* Test attribut volume name and check if the volume name is erased or not */
        if(((buffer[i*0x20+0xB] & ATTR_EXT) !=ATTR_EXT) && ((buffer[i*0x20+0xB] & ATTR_VOLUME) !=0) && (buffer[i*0x20]!=0xE5))
        {
          set_part_name_chomp(partition, (const char *)&buffer[i*0x20],11);
          if(check_VFAT_volume_name(partition->fsname, 11))
            partition->fsname[0]='\0';
        }
        if(buffer[i*0x20]==0)
        {
          stop=1;
        }
      }
    }
    free(buffer);
  }
  if(partition->fsname[0]=='\0')
  {
#ifndef DISABLED_FOR_FRAMAC
    log_info("set_FAT_info: name from BS used\n");
#endif
    set_part_name_chomp(partition, (const char*)fat_header + FAT32_PART_NAME, 11);
    if(check_VFAT_volume_name(partition->fsname, 11))
      partition->fsname[0]='\0';
  }
  return 0;
}

/*@
  @ requires \valid(disk_car);