Documented in 1 files:

Defined in 1 files as a function:

Referenced in 1 files:

Smatch caller information:

drivers/md/dm-vdo/block-map.c vdo_traverse_forest() -> compute_boundary()

Type Parameter Key Value
PARAM_VALUE 0 map 4096-ptr_max
PARAM_VALUE 0 map->root_count 1-u64max
CAPPED_DATA 1 root_index 1
DATA_SOURCE 0 map $0
PARAM_COMPARE 0 map->root_count > $1
PARAM_COMPARE 1 root_index < $0->root_count
RX_PATH
TASK_NOT_RUNNING
NO_OVERFLOW_SIMPLE 0 map->root_count
NO_OVERFLOW_SIMPLE 1 root_index