Function data_check_aux

src/fidentify.c:106–181

@ @ 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 \valid(buffer_start + (0 .. blocksize + READ_SIZE -1)); @ requires \separated(file_recovery, &errno, buffer_start + (..)); @ decreases 0; @ ensures valid_

  @ assigns file_recovery->data_check, file_recovery->file_check, file_recovery->offset_error, file_recovery->offset_ok, file_recovery->time, file_recovery->data_check_tmp;
  @*/
static data_check_t data_check_aux(file_recovery_t *file_recovery, const unsigned int blocksize, char *buffer_start)
{
  /*@ ghost const unsigned int buffer_size=blocksize + READ_SIZE; */
  /*@
    @ loop invariant valid_file_recovery(file_recovery);
    @ loop invariant file_recovery == \at(file_recovery, Pre);
    @ loop invariant \valid_read(buffer_start + (0 .. blocksize + READ_SIZE - 1));
    @ loop invariant file_recovery->calculated_file_size < PHOTOREC_MAX_FILE_SIZE;
    @ loop invariant file_recovery->file_size < PHOTOREC_MAX_FILE_SIZE;
    @ loop invariant \valid_function(file_recovery->data_check);
    @ loop invariant \separated(file_recovery, &errno, buffer_start + (..));
    @ loop assigns *file_recovery->handle, errno;
    @ loop assigns buffer_start[0 .. blocksize + READ_SIZE -1];
    @ loop assigns file_recovery->file_size;
    @ loop assigns file_recovery->calculated_file_size, file_recovery->data_check_tmp;
    @ loop assigns file_recovery->data_check, file_recovery->file_check, file_recovery->offset_error, file_recovery->offset_ok, file_recovery->time, file_recovery->data_check_tmp;
    @*/
  while(1)
  {
    char *buffer=buffer_start+blocksize;
    unsigned int i;
    size_t lu=0;
    /*@ assert valid_file_recovery(file_recovery); */
    memset(buffer, 0, READ_SIZE);
    lu=fread(buffer, 1, READ_SIZE, file_recovery->handle);
    if(lu <= 0)
    {
      /*@ assert valid_file_recovery(file_recovery); */
      return DC_STOP;
    }
    /*@ assert 0 < lu <= READ_SIZE; */
    /*@
      @ loop invariant valid_file_recovery(file_recovery);
      @ loop invariant file_recovery == \at(file_recovery, Pre);
      @ loop invariant \valid_read(buffer_start + (0 .. blocksize + READ_SIZE - 1));
      @ loop invariant file_recovery->calculated_file_size < PHOTOREC_MAX_FILE_SIZE;
      @ loop invariant file_recovery->file_size < PHOTOREC_MAX_FILE_SIZE;
      @ loop invariant \valid_function(file_recovery->data_check);
      @ loop invariant \separated(file_recovery, &errno, buffer_start + (..));
      @ loop assigns i, file_recovery->file_size;
      @ loop assigns file_recovery->calculated_file_size, file_recovery->data_check_tmp;
      @ loop assigns file_recovery->data_check, file_recovery->file_check, file_recovery->offset_error, file_recovery->offset_ok, file_recovery->time, file_recovery->data_check_tmp;
      @ loop variant lu - i;
      @*/
    for(i=0; i<lu; i+=blocksize)
    {
      /*@ assert i + 2*blocksize <= buffer_size; */
      /*@ assert \valid_read(&buffer_start[i] + (0 .. 2*blocksize-1)); */
      const data_check_t res=data_check_wrapper((const unsigned char *) &buffer_start[i], 2*blocksize, file_recovery);
      /*@ assert valid_data_check_result(res, file_recovery); */
      /*@ assert \valid_read(&buffer_start[i] + (0 .. 2*blocksize-1)); */
      file_recovery->file_size+=blocksize;
      if(res != DC_CONTINUE || file_recovery->data_check==NULL)
      {
	/*@ assert valid_file_recovery(file_recovery); */
	return res;
      }
      if( file_recovery->calculated_file_size >= PHOTOREC_MAX_FILE_SIZE ||