Function header_check_dir

src/file_dir.c:101–114

@ @ requires buffer_size >= sizeof(struct msdos_dir_entry); @ requires separation: \separated(&file_hint_dir, 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_dir(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)
{
  const struct msdos_dir_entry *de=(const struct msdos_dir_entry*)buffer;
  if(!is_fat_directory(buffer))
    return 0;
  reset_file_recovery(file_recovery_new);
  file_recovery_new->extension=file_hint_dir.extension;
  file_recovery_new->data_check=&data_check_fatdir;
  file_recovery_new->file_check=&file_check_size;
  file_recovery_new->file_rename=&file_rename_fatdir;
  file_recovery_new->time=date_dos2unix(le16(de->time),le16(de->date));
  /*@ assert valid_file_recovery(file_recovery_new); */
  return 1;
}

static void register_header_check_dir(file_stat_t *file_stat)
{