Defined in 1 files as a function:

Referenced in 1 files:

Smatch caller information:

drivers/net/usb/cdc_ncm.c cdc_ncm_bind_common() -> cdc_ncm_free()

Type Parameter Key Value
PARAM_VALUE 0 ctx 4096-ptr_max
RX_PATH
TASK_NOT_RUNNING
NOCHECK_CALL

drivers/net/usb/cdc_ncm.c cdc_ncm_unbind() -> cdc_ncm_free()

Type Parameter Key Value
PARAM_VALUE 0 ctx 4096-ptr_max
PARAM_VALUE 0 ctx->control->dev.kobj.parent->sd->attr.open->nr_mmapped 0-4294967295
PARAM_VALUE 0 ctx->control->dev.kobj.sd->attr.open->nr_mmapped 0-4294967295
PARAM_VALUE 0 ctx->control->dev.power.wakeirq->status 0-4294967295
PARAM_VALUE 0 ctx->data->dev.kobj.parent->sd->attr.open->nr_mmapped 0-4294967295
PARAM_VALUE 0 ctx->data->dev.kobj.sd->attr.open->nr_mmapped 0-4294967295
PARAM_VALUE 0 ctx->data->dev.power.wakeirq->status 0-4294967295
PARAM_VALUE 0 ctx->stop.counter 1
CAPPED_DATA 0 ctx->tx_timer.base 1
CAPPED_DATA 0 &ctx->tx_timer 1
PARAM_COMPARE 0 &ctx->tx_timer != $0->tx_timer.base->running
RX_PATH
TASK_NOT_RUNNING
NOCHECK_CALL