Function header_check_bvr

src/file_bvr.c:82–97

@ @ requires separation: \separated(&file_hint_bvr, 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_bvr(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)
{
  if(file_recovery->file_stat!=NULL &&
    file_recovery->file_check!=NULL &&
    file_recovery->file_stat->file_hint==&file_hint_bvr)
  {
    /*@ 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_bvr.extension;
  file_recovery_new->data_check=&data_check_bvr;
  file_recovery_new->file_check=&file_check_size;
  return 1;
}

static void register_header_check_bvr(file_stat_t *file_stat)
{