Function data_check

src/fidentify.c:192–213

@ @ requires \valid(file_recovery); @ requires valid_file_recovery(file_recovery); @ requires \valid_function(file_recovery->data_check); @ requires 0 < blocksize <= READ_SIZE; @ requires READ_SIZE % blocksize == 0; @ requires \separated(file_recovery, &errno); @ ensures valid_file_recovery(file_recovery); @*/

  @ ensures  valid_file_recovery(file_recovery);
  @*/
static data_check_t data_check(file_recovery_t *file_recovery, const unsigned int blocksize)
{
  char *buffer_start;
  const unsigned int buffer_size=blocksize + READ_SIZE;
  data_check_t res;
  if( file_recovery->calculated_file_size >= PHOTOREC_MAX_FILE_SIZE )
  {
    /*@ assert valid_file_recovery(file_recovery); */
    return DC_STOP;
  }
  if(my_fseek(file_recovery->handle, 0, SEEK_SET) < 0)
  {
    /*@ assert valid_file_recovery(file_recovery); */
    return DC_STOP;
  }
  buffer_start=(char *)MALLOC(buffer_size);
  res=data_check_aux(file_recovery, blocksize, buffer_start);
  /*@ assert valid_file_recovery(file_recovery); */
  free(buffer_start);
  /*@ assert valid_file_recovery(file_recovery); */
  return res;
}

/*@
  @ requires valid_read_string(filename);