Linux Driver Verification » Linux Kernel Safety RuleDB

Here one can see a list of defines represented different attributes to become some kind of annotations. For instance, see the example below (complete example is here):

static void ehci_urb_done(struct oxu_hcd *oxu, struct urb *urb)
__releases(oxu->lock)
__acquires(oxu->lock)
{
        ...
        spin_unlock(&oxu->lock);
        usb_hcd_giveback_urb(oxu_to_hcd(oxu), urb, urb->status);
        spin_lock(&oxu->lock);
}

We can check whether a function really releases oxu->lock and then acquires oxu->lock or not.