Function file_check_doc

src/file_doc.c:421–424

@ @ requires file_recovery->file_check == &file_check_doc; @ requires valid_file_check_param(file_recovery); @ ensures valid_file_check_result(file_recovery); @*/

  @ ensures  valid_file_check_result(file_recovery);
  @*/
static void file_check_doc(file_recovery_t *file_recovery)
{
  file_check_doc_aux(file_recovery, 0);
}

/*@
  @ requires \valid_read(dir_entry);