Function header_check_tar

src/file_tar.c:117–134

@ @ requires buffer_size >= sizeof(struct tar_posix_header); @ requires separation: \separated(&file_hint_tar, buffer+(..), file_recovery, file_recovery_new); @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new); @ ensures valid_header_check_result(\result, file_recovery_new); @ assigns *file_recovery_new; @*/

  @ assigns  *file_recovery_new;
  @*/
static int header_check_tar(const unsigned char *buffer, const unsigned int buffer_size, const unsigned int safe_header_only, const file_recovery_t *file_recovery, file_recovery_t *file_recovery_new)
{
  /*@ assert valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new); */
  const struct tar_posix_header *h = (const struct tar_posix_header *)buffer;
  if(is_valid_tar_header(h) == 0)
    return 0;
  /*@ assert \valid_read(file_recovery); */
  if(file_recovery->file_stat != NULL && file_recovery->file_stat->file_hint == &file_hint_tar)
  {
    /* header_ignored(file_recovery_new); is useless as there is no file check */
    return 0;
  }
  reset_file_recovery(file_recovery_new);
  file_recovery_new->extension = file_hint_tar.extension;
  file_recovery_new->min_filesize = 512;
  /*@ assert valid_file_recovery(file_recovery_new); */
  return 1;
}

/*@
  @ requires valid_register_header_check(file_stat);