Function header_check_dad

src/file_dad.c:98–122

@ @ requires buffer_size >= 10; @ requires separation: \separated(&file_hint_dad, buffer+(..), file_recovery, file_recovery_new); @ requires valid_header_check_param(buffer, buffer_size, safe_header_only, file_recovery, file_recovery_new); @ terminates \true; @ ensures valid_header_check_result(\result, file_recovery_new); @*/

  @ ensures  valid_header_check_result(\result, file_recovery_new);
  @*/
static int header_check_dad(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 dad_header *dad=(const struct dad_header *)buffer;
  const unsigned int size=le32(dad->size);
  if(size<16)
    return 0;
  if(file_recovery->file_stat!=NULL &&
      file_recovery->file_check!=NULL &&
      file_recovery->file_stat->file_hint==&file_hint_dad &&
      file_recovery->calculated_file_size==file_recovery->file_size)
  {
    /*@ assert \valid_function(file_recovery->file_check); */
    header_ignored(file_recovery_new);
    return 0;
  }
  reset_file_recovery(file_recovery_new);
  file_recovery_new->extension=file_hint_dad.extension;
  file_recovery_new->min_filesize=size;
  if(file_recovery_new->blocksize >= 16)
  {
    file_recovery_new->data_check=&data_check_dad;
    file_recovery_new->file_check=&file_check_size_max;
  }
  return 1;
}

static void register_header_check_dad(file_stat_t *file_stat)
{