Function header_check_ext2_sb

src/file_ext.c:88–101

@ @ requires buffer_size >= sizeof(struct ext2_super_block); @ requires separation: \separated(&file_hint_ext2_sb, 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_ext2_sb(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 ext2_super_block *sb=(const struct ext2_super_block *)buffer;
  if(test_EXT2(sb, NULL)!=0)
    return 0;
  /*@ assert le32(sb->s_log_block_size) <= 6; */
  reset_file_recovery(file_recovery_new);
  file_recovery_new->extension=file_hint_ext2_sb.extension;
  file_recovery_new->file_size=(uint64_t)EXT2_MIN_BLOCK_SIZE<<le32(sb->s_log_block_size);
  file_recovery_new->data_check=&data_check_size;
  file_recovery_new->file_check=&file_check_size;
  file_recovery_new->file_rename=&file_rename_ext;
  return 1;
}

/*@
  @ requires file_recovery->data_check==&data_check_extdir;