Function header_mpg_found

src/file_mpg.c:184–193

@ @ requires \valid(file_recovery_new); @ terminates \true; @ ensures valid_file_recovery(file_recovery_new); @ assigns *file_recovery_new; @*/

  @ assigns  *file_recovery_new;
  @*/
static int header_mpg_found(file_recovery_t *file_recovery_new)
{
  reset_file_recovery(file_recovery_new);
  file_recovery_new->extension=file_hint_mpg.extension;
  if(file_recovery_new->blocksize < 14)
    return 1;
  file_recovery_new->data_check=&data_check_mpg;
  file_recovery_new->file_check=&file_check_size;
  return 1;
}

/*@
  @ requires buffer_size >= 13;