Function file_check_add_tail

src/filegen.c:161–187

@ @ requires \valid(file_check_new); @ requires \valid(pos); @ requires initialization: \initialized(&file_check_new->offset) && \initialized(&file_check_new->length); @ requires valid_file_check_node(file_check_new); @*/

  @ requires valid_file_check_node(file_check_new);
  @*/
static void file_check_add_tail(file_check_t *file_check_new, file_check_list_t *pos)
{
  unsigned int i;
  const unsigned int tmp=(file_check_new->length==0?0:((const unsigned char *)file_check_new->value)[0]);
  file_check_list_t *newe=(file_check_list_t *)MALLOC(sizeof(*newe));
  /*@ assert \valid(newe); */
  newe->offset=file_check_new->offset;
  /*@
    @ loop unroll 256;
    @ loop invariant 0 <= i <= 256;
    @ loop invariant \forall integer j; (0 <= j < i) ==> newe->file_checks[j].list.prev == &newe->file_checks[j].list;
    @ loop invariant \forall integer j; (0 <= j < i) ==> newe->file_checks[j].list.next == &newe->file_checks[j].list;
    @ loop assigns i, newe->file_checks[0 .. i-1].list.prev, newe->file_checks[0 .. i-1].list.next;
    @ loop variant 255-i;
    @*/
  for(i=0;i<256;i++)
  {
    TD_INIT_LIST_HEAD(&newe->file_checks[i].list);
    /*@ assert newe->file_checks[i].list.prev == &newe->file_checks[i].list; */
    /*@ assert newe->file_checks[i].list.next == &newe->file_checks[i].list; */
  }
  /*@ assert 0 <= tmp <= 255; */
  /*@ assert newe->file_checks[tmp].list.prev == &newe->file_checks[tmp].list; */
  /*@ assert newe->file_checks[tmp].list.next == &newe->file_checks[tmp].list; */
  td_list_add_tail(&file_check_new->list, &newe->file_checks[tmp].list);
  td_list_add_tail(&newe->list, &pos->list);
}

#ifndef DISABLED_FOR_FRAMAC
/*@