Function index_header_check

src/filegen.c:266–288

}

static unsigned int index_header_check(void)
{
  struct td_list_head *tmp;
  struct td_list_head *next;
  unsigned int nbr=0;
  /* Initialize file_check_list from file_check_plist */
  /*@
    @ loop invariant \valid_read(tmp);
    @ loop invariant \valid_read(next);
    @*/
  td_list_for_each_prev_safe(tmp, next, &file_check_plist.list)
  {
    file_check_t *current_check;
    current_check=td_list_entry(tmp, file_check_t, list);
    /*@ assert valid_file_check_node(current_check); */
    /* dettach current_check from file_check_plist */
    td_list_del(tmp);
    /*@ assert \initialized(&current_check->offset) && \initialized(&current_check->length); */
    index_header_check_aux(current_check);
    nbr++;
  }
  return nbr;
}

void free_header_check(void)
{