Function file_nopwrite

src/hdaccess.c:1616–1623

@ @ requires \valid(disk_car); @ requires valid_disk(disk_car); @ requires disk_car->sector_size > 0; @ requires disk_car->offset < 0x2000000000000; @ requires 0 < count < 0x2000000000000; @ requires offset < 0x2000000000000; @ requires \valid_read((char *)buf + (0 .. count-1)); @*/

  @ requires \valid_read((char *)buf + (0 .. count-1));
  @*/
static int file_nopwrite(disk_t *disk_car, const void *buf, const unsigned int count, const uint64_t offset)
{
  struct info_file_struct *data=(struct info_file_struct *)disk_car->data;
  log_warning("file_nopwrite(%d,%u,buffer,%lu(%u/%u/%u)) write refused\n", data->handle,
      (unsigned)(count/disk_car->sector_size),(long unsigned)(offset/disk_car->sector_size),
      offset2cylinder(disk_car,offset),offset2head(disk_car,offset),offset2sector(disk_car,offset));
  return -1;
}

/*@
  @ requires \valid(disk_car);