void kfree(void *p) {
    free(p);
}

struct spin_lock {
    int a;
};

#define ldv_assert(b) if(!(b)) __VERIFIER_error()

static int spin_lock = 1;

void ldv_spin_lock(struct spin_lock *lock)
{
    ldv_assert(spin_lock == 1);
    spin_lock = 2;
}

void spin_unlock(struct spin_lock *lock) {
    ldv_assert(spin_lock == 2);
    spin_lock = 1;
}

struct lirq {
    int index;
    unsigned int irq;
};

#define MAX 32

struct priv {
    struct spin_lock lock;
    int ngpio;
    unsigned long imask;
    struct lirq lirqs[MAX];
};

unsigned long get_mask(struct priv *priv, unsigned int offset);

static void grgpio_set_imask(struct priv *priv, unsigned int offset,
                 int val)
{
    unsigned long mask = get_mask(priv, offset);

    //security: double lock occurs on all paths
        ldv_spin_lock(&priv->lock);

    if (val)
        priv->imask |= mask;
    else
        priv->imask &= ~mask;

    spin_unlock(&priv->lock);
}

static void irq_unmap(struct priv *priv, unsigned int irq)
{
    int index;
    int i;
    struct lirq *lirq;
    int ngpio = priv->ngpio;
    int k = 2;

    ldv_spin_lock(&priv->lock);
    /* Free underlying irq if last user unmapped */
    index = -1;
    for (i = 0; k < ngpio; i++) {
        lirq = &priv->lirqs[i];
        if (lirq->irq == irq) {
            grgpio_set_imask(priv, i, 0);
            index = lirq->index;
            break;
        }
    }
    spin_unlock(&priv->lock);
}

struct priv *get_priv(void);
unsigned int get_irq(void);

void main(void) {
    struct priv *priv = get_priv();
    unsigned int irq = get_irq();
    irq_unmap(priv, irq);
}