Function td_list_add_tail

src/list.h:199–202

* td_list_add_tail - add a new entry * @newe: new entry to be added * @head: list head to add it before * * Insert a new entry before the specified head. * This is useful for implementing queues. */ @ @ requires \valid(newe); @ requires \valid(head); @ requires \valid(head->prev); @ requires separation: \separated(newe, head); @ requires \separated(newe, \union(head->prev, head));

  @ assigns head->prev,newe->next,newe->prev,\old(head->prev)->next;
  @*/
static inline void td_list_add_tail(struct td_list_head *newe, struct td_list_head *head)
{
	__td_list_add(newe, head->prev, head);
}

/*
 * Delete a list entry by making the prev/next entries