Function init_file_stats

src/filegen.c:517–570

}

file_stat_t * init_file_stats(file_enable_t *files_enable)
{
  file_stat_t *file_stats;
  file_enable_t *file_enable;
  unsigned int enable_count=1;	/* Lists are terminated by NULL */
  unsigned int sign_nbr;
  unsigned int i;
  /*@
    @ loop invariant valid_file_enable_node(file_enable);
    @ loop assigns enable_count, file_enable;
    @*/
  for(file_enable=files_enable;file_enable->file_hint!=NULL;file_enable++)
  {
    if(file_enable->enable>0 && file_enable->file_hint->register_header_check!=NULL)
    {
      enable_count++;
    }
  }
  /*@ assert enable_count > 0; */
  file_stats=(file_stat_t *)MALLOC(enable_count * sizeof(file_stat_t));
  /*@ assert \valid(file_stats + (0 .. enable_count-1)); */
  i=0;
  /*@
    @ loop invariant \valid(file_stats + (0 .. enable_count-1));
    @ loop invariant valid_file_enable_node(file_enable);
    @ loop invariant 1 <= enable_count;
    @ loop invariant 0 <= i < enable_count;
    @ loop invariant \forall integer j; 0 <= j < i ==> valid_file_stat(&file_stats[j]);
    @*/
  for(file_enable=files_enable;file_enable->file_hint!=NULL;file_enable++)
  {
    /*@ assert i < enable_count; */
    /*@ assert \valid_read(file_enable); */
    /*@ assert \valid_read(file_enable->file_hint); */
    if(file_enable->enable>0 && file_enable->file_hint->register_header_check!=NULL)
    {
      file_stats[i].file_hint=file_enable->file_hint;
      file_stats[i].not_recovered=0;
      file_stats[i].recovered=0;
      /*@ assert \valid_function((file_enable->file_hint)->register_header_check); */
      file_enable->file_hint->register_header_check(&file_stats[i]);
      /*@ assert valid_file_stat(&file_stats[i]); */
      i++;
    }
  }
  sign_nbr=index_header_check();
  /*@ assert \valid(file_stats + (0 .. enable_count-1)); */
  /*@ assert 1 <= enable_count; */
  file_stats[enable_count-1].file_hint=NULL;
#ifndef DISABLED_FOR_FRAMAC
  log_info("%u first-level signatures enabled\n", sign_nbr);
#endif
  return file_stats;
}

/*@
  @ requires \valid(file_recovery);