Project

General

Profile

Download (1.07 KB)

Bug #10026 ยป hlist_add_head.c

Denis Efremov, 01/09/2020 09:10 PM

 
struct hlist_node {
struct hlist_node *next, **pprev;
};

struct hlist_head {
struct hlist_node *first;
};

/**
* hash_add - add an object to a hashtable
* @hashtable: hashtable to add to
* @node: the &struct hlist_node of the object to be added
* @key: the key of the object to be added
*/
#define hash_add(hashtable, node, key) \
hlist_add_head(node, &hashtable[hash_min(key, HASH_BITS(hashtable))])


/*@ requires \valid(n);
requires \valid(h);
requires h->first == \null || \valid(h->first);
requires h->first != n;
requires h->first != n->next;
requires h->first->pprev != &n;

assigns n->next, n->pprev, h->first->pprev, h->first;

ensures h->first == n;

ensures n->next == \old(h->first);
ensures n->pprev == &h->first;

behavior NOT_EMPTY_BUCKET:
assumes \valid(h->first);
ensures \old(h->first->pprev) == &n->next;
*/
static inline void hlist_add_head(struct hlist_node *n, struct hlist_head *h)
{
struct hlist_node *first = h->first;
n->next = first;
if (first)
first->pprev = &n->next;
h->first = n;
n->pprev = &h->first;
}
    (1-1/1)