Function data_check_wrapper

src/fidentify.c:77–88

@ @ requires \valid_function(file_recovery->data_check); @ requires valid_data_check_param(buffer, buffer_size, file_recovery); @ ensures valid_file_recovery(file_recovery); @ ensures valid_data_check_result(\result, file_recovery); @ assigns file_recovery->calculated_file_size, file_recovery->data_check_tmp; @ assigns file_recovery->data_check, file_recovery->file_check, file_recove

  @ 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_wrapper(const unsigned char *buffer, const unsigned int buffer_size, file_recovery_t *file_recovery)
{
  data_check_t tmp;
  /*@ assert \valid(file_recovery); */
  /*@ assert valid_file_recovery(file_recovery); */
  /*@ split file_recovery->data_check; */
  /*@ assert \valid_function(file_recovery->data_check); */
  tmp=file_recovery->data_check(buffer, buffer_size, file_recovery);
  /*@ assert valid_file_recovery(file_recovery); */
  /*@ assert valid_data_check_result(tmp, file_recovery); */
  return tmp;
}

/*@
  @ requires \valid(file_recovery);