Function td_list_add

src/list.h:168–171

* td_list_add - add a new entry * @newe: new entry to be added * @head: list head to add it after * * Insert a new entry after the specified head. * This is good for implementing stacks. */ @ @ requires \valid(newe); @ requires \valid(head); @ requires \valid(head->next); @ requires separation: \separated(newe, \union(head,head->next)); @ requires finite(head); @ requires finite(

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

/**
 * td_list_add_tail - add a new entry