Function __td_list_del

src/list.h:220–226

* Delete a list entry by making the prev/next entries * point to each other. * * This is only for internal list manipulation where we know * the prev/next entries already! */ @ @ requires \valid(prev); @ requires \valid(next); @ requires prev == next || \separated(prev,next); @ terminates \true; @ ensures next->prev == prev; @ ensures prev->next == next; @ assigns next->prev,pre

  @ assigns next->prev,prev->next;
  @*/
static inline void __td_list_del(struct td_list_head * prev, struct td_list_head * next)
{
	next->prev = prev;
	prev->next = next;
	/*@ assert next->prev == prev; */
	/*@ assert prev->next == next; */
}

/**
 * td_list_del - deletes entry from list.