Function fat16_remove_used_space

src/fatp.c:107–149

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

  @ decreases 0;
  @*/
static void fat16_remove_used_space(disk_t *disk_car,const partition_t *partition, alloc_data_t *list_search_space, const unsigned int fat_offset, const unsigned int no_of_cluster, const unsigned int start_data, const unsigned int cluster_size, const unsigned int sector_size)
{
  unsigned char *buffer;
  const uint16_t *p16;
  unsigned int prev_cluster;
  uint64_t hd_offset=partition->part_offset+(uint64_t)fat_offset*sector_size;
  uint64_t start_free=0;
  uint64_t end_free=0;
  log_trace("fat16_remove_used_space\n");
  buffer=(unsigned char *)MALLOC(sector_size);
  p16=(const uint16_t*)buffer;
  del_search_space(list_search_space, partition->part_offset,
      partition->part_offset + (uint64_t)start_data * sector_size - 1);
  for(prev_cluster=2;prev_cluster<=no_of_cluster+1;prev_cluster++)
  {
    unsigned int offset_o;
    offset_o=prev_cluster%(sector_size/2);
    if((offset_o==0)||(prev_cluster==2))
    {
      if((unsigned)disk_car->pread(disk_car, buffer, sector_size, hd_offset) != sector_size)
      {
	/* Consider these FAT sectors points to free clusters */
      }
      hd_offset+=sector_size;
    }
    if(le16(p16[offset_o])!=0)
    {
      /* Not free */
      if(end_free+1==partition->part_offset+(start_data+(uint64_t)(prev_cluster-2)*cluster_size)*sector_size)
	end_free+=cluster_size*sector_size;
      else
      {
	if(start_free != end_free)
	  del_search_space(list_search_space, start_free, end_free);
	start_free=partition->part_offset+(start_data+(uint64_t)(prev_cluster-2)*cluster_size)*sector_size;
	end_free=start_free+(uint64_t)cluster_size*sector_size-1;
      }
    }
  }
  free(buffer);
  if(start_free != end_free)
    del_search_space(list_search_space, start_free, end_free);
}

/*@
  @ requires \valid(disk_car);