Function merge

src/list_sort.c:42–67

* Returns a list organized in an intermediate format suited * to chaining of merge() calls: null-terminated, no reserved or * sentinel head node, "prev" links not maintained. */ @ @ decreases 0; @*/

  @ decreases 0;
  @*/
static struct td_list_head *merge(
    int (*cmp)(const struct td_list_head *a, const struct td_list_head *b),
    struct td_list_head *a, struct td_list_head *b)
{
  struct td_list_head head, *tail = &head;

  /*@
    @ loop invariant \valid_function(cmp);
    @ loop invariant \valid(tail);
    @ loop invariant \valid(a);
    @ loop invariant \valid(b);
    @*/
  while (a && b) {
    /* if equal, take 'a' -- important for sort stability */
    if ((*cmp)(a, b) <= 0) {
      tail->next = a;
      a = a->next;
    } else {
      tail->next = b;
      b = b->next;
    }
    tail = tail->next;
  }
  tail->next = a?a:b;
  return head.next;
}

/*
 * Combine final list merge with restoration of standard doubly-linked