Defined in 1 files as a function:

Referenced in 1 files:

Smatch caller information:

drivers/xen/evtchn.c evtchn_read() -> evtchn_ring_offset()

Type Parameter Key Value
PARAM_VALUE 0 u 4096-ptr_max
BUF_SIZE 0 u s32min-(-2),1-s32max
BUF_SIZE 0 u s32min-(-2),1-s32max
CAPPED_DATA 0 &u->ring_cons_mutex 1
LOCK2 0 &u->ring_cons_mutex
TYPE_LOCK (struct per_user_data)->ring_cons_mutex

drivers/xen/evtchn.c evtchn_read() -> evtchn_ring_offset()

Type Parameter Key Value
PARAM_VALUE 0 u 4096-ptr_max
BUF_SIZE 0 u s32min-(-2),1-s32max
BUF_SIZE 0 u s32min-(-2),1-s32max
CAPPED_DATA 0 &u->ring_cons_mutex 1
LOCK2 0 &u->ring_cons_mutex
TYPE_LOCK (struct per_user_data)->ring_cons_mutex

drivers/xen/evtchn.c evtchn_ring_entry() -> evtchn_ring_offset()

Type Parameter Key Value
PARAM_VALUE 0 u 4096-ptr_max
BUF_SIZE 0 u s32min-(-1),1-s32max
BUF_SIZE 0 u s32min-(-1),1-s32max
DATA_SOURCE 0 u $0
DATA_SOURCE 1 idx $1
PREEMPT_ADD
RX_PATH
TASK_NOT_RUNNING
HALF_LOCKED2 0 &u->ring_cons_mutex
HALF_LOCKED2 0 &u->ring_prod_lock