Function autoset_geometry

src/hdaccess.c:1656–1702

@ @ requires \valid(disk); @ requires valid_disk(disk); @ requires 0 < disk->geom.heads_per_cylinder <= 255; @ requires 0 < disk->geom.sectors_per_head <= 63; @ requires \valid_read(buffer + (0 .. DEFAULT_SECTOR_SIZE-1)); @ requires separation: \separated(disk, buffer + (0 .. DEFAULT_SECTOR_SIZE-1)); @ decreases 0; @ ensures valid_disk(disk); @*/ assigns disk->geom.cylinders; ass

// ensures 0 < disk->geom.heads_per_cylinder <= 255;
// ensures 0 < disk->geom.sectors_per_head <= 63;
static void autoset_geometry(disk_t *disk, const unsigned char *buffer, const int verbose)
{
  /*@ assert 0 < disk->sector_size; */
  if((disk->arch)->get_geometry_from_mbr!=NULL)
  {
    /*@ assert \valid_function(disk->arch->get_geometry_from_mbr); */
    CHSgeometry_t geometry;
    geometry.cylinders=0;
    geometry.heads_per_cylinder=0;
    geometry.sectors_per_head=0;
    geometry.bytes_per_sector=0;
    disk->arch->get_geometry_from_mbr(buffer, verbose, &geometry);
    disk->autodetect=1;
    if( geometry.heads_per_cylinder > 0 &&
	geometry.heads_per_cylinder <= 255 &&
	geometry.sectors_per_head > 0 &&
	geometry.sectors_per_head <= 63
      )
    {
      /*@ assert 0 < geometry.heads_per_cylinder <= 255; */
      /*@ assert 0 < geometry.sectors_per_head <= 63; */
      disk->geom.heads_per_cylinder=geometry.heads_per_cylinder;
      disk->geom.sectors_per_head=geometry.sectors_per_head;
      /*@ assert 0 < disk->geom.heads_per_cylinder <= 255; */
      /*@ assert 0 < disk->geom.sectors_per_head <= 63; */
      if(geometry.bytes_per_sector!=0)
      {
	disk->geom.bytes_per_sector=geometry.bytes_per_sector;
	disk->sector_size=geometry.bytes_per_sector;
	/*@ assert 0 < disk->sector_size; */
      }
      /*@ assert 0 < disk->sector_size; */
    }
    else
    {
      disk->geom.heads_per_cylinder=255;
      disk->geom.sectors_per_head=63;
    }
  }
  /*@ assert 0 < disk->sector_size; */
  /*@ assert 0 < disk->geom.heads_per_cylinder <= 255; */
  /*@ assert 0 < disk->geom.sectors_per_head <= 63; */
  /* Round up because file is often truncated. */
  disk->geom.cylinders=(disk->disk_size / disk->sector_size +
      (uint64_t)disk->geom.sectors_per_head * disk->geom.heads_per_cylinder - 1) /
    disk->geom.sectors_per_head / disk->geom.heads_per_cylinder;
}

/*@
  @ requires \valid_read(hdr);