Linux Driver Verification

Model 131_1a: Driver tries to stop an hrtimer which was never started (http://forge.ispras.ru/issues/3283) was tested on kernel linux-2.6.36.1.
There is only 1 driver, which uses the functions being checking this model (drivers/input/joystick/walkera0701.ko). But LDV-tools can't check it correctly because this driver has the next structure:

static void walkera0701_irq_handler(void *handler_data)
{ ...}

static int walkera0701_connect(struct walkera_dev *w, int parport)
{
  ...
   w->pardevice = parport_register_device(w->parport, "walkera0701",
                    NULL, NULL, walkera0701_irq_handler,
                    PARPORT_DEV_EXCL, w);
   ...
}