Function __td_list_add

src/list.h:121–143

* Insert a new entry between two known consecutive entries. * * This is only for internal list manipulation where we know * the prev/next entries already! */ @ @ requires \valid(newe); @ requires \valid(prev); @ requires \valid(next); @ requires separation: \separated(newe, \union(prev,next)); @ requires prev == next || \separated(prev,next,newe); @ requires finite(prev); @ requi

  @ assigns next->prev,newe->next,newe->prev,prev->next;
  @*/
static inline void __td_list_add(struct td_list_head *newe,
			      struct td_list_head *prev,
			      struct td_list_head *next)
{
        /*@ assert finite(prev); */
        /*@ assert finite(next); */
        /*@ assert reachable_forward(prev->next,prev); */
        /*@ assert reachable_forward(next->next,next); */
        /*@ assert reachable_backward(prev->prev,prev); */
        /*@ assert reachable_backward(next->prev,next); */

        /*@ assert reachable_forward(next,prev); */
	newe->next = next;
	newe->prev = prev;
	prev->next = newe;
	next->prev = newe;
	/*@ assert next->prev == newe; */
	/*@ assert newe->next == next; */
	/*@ assert newe->prev == prev; */
	/*@ assert prev->next == newe; */
	/*@ assert reachable_forward(prev,newe); */
	/*@ assert reachable_backward(next,newe); */
}

/**
 * td_list_add - add a new entry