Function td_list_del

src/list.h:245–254

* td_list_del - deletes entry from list. * @entry: the element to delete from the list. * Note: td_list_empty on entry does not return true after this, the entry is * in an undefined state. */ @ @ requires \valid(entry); @ requires \valid(entry->prev); @ requires \valid(entry->next); @ requires \separated(entry, \union(entry->prev,entry->next)); @ requires entry->prev == entry->next

  @ assigns \old(entry->prev)->next, \old(entry->next)->prev, entry->next, entry->prev;
  @*/
static inline void td_list_del(struct td_list_head *entry)
{
	__td_list_del(entry->prev, entry->next);
	/*@ assert entry->prev->next == entry->next; */
	/*@ assert entry->next->prev == entry->prev; */
	entry->next = (struct td_list_head*)LIST_POISON1;
	entry->prev = (struct td_list_head*)LIST_POISON2;
	/*@ assert \at(entry->prev,Pre)->next == \at(entry->next,Pre); */
	/*@ assert \at(entry->next,Pre)->prev == \at(entry->prev,Pre); */
}

#if 0
/**