Defined in 1 files as a function:

Referenced in 1 files:

Smatch caller information:

arch/x86/kvm/mmu/mmu.c slot_rmap_walk_init() -> rmap_walk_init_level()

Type Parameter Key Value
PARAM_VALUE 0 iterator 3311955574709174272
PARAM_VALUE 0 iterator->slot 4096-ptr_max
PARAM_VALUE 1 level 1-3
DATA_SOURCE 0 iterator $0
DATA_SOURCE 1 level $2
NOSPEC 0 iterator->slot->base_gfn
NOSPEC 0 iterator->slot->id
NOSPEC 0 iterator->slot->npages
NOSPEC 0 iterator->start_gfn
PREEMPT_ADD
RX_PATH
TASK_NOT_RUNNING
NOCHECK_CALL
USER_DATA 0 iterator->end_gfn 0-4503599627894781,u64max[u]
USER_DATA 0 iterator->slot->base_gfn 0-524287[c]
USER_DATA 0 iterator->slot->flags 0-u32max
USER_DATA 0 iterator->slot->gmem.pgoff 0-524287[c]
USER_DATA 0 iterator->slot->id 0-32763[c]
USER_DATA 0 iterator->slot->npages 0-4503599627370495[c]
USER_DATA 0 iterator->start_gfn 0-s32max[c]
NO_OVERFLOW_SIMPLE 0 iterator->slot->npages
HALF_LOCKED2 &kvm->lock
HALF_LOCKED2 &kvm->mmu_lock
HALF_LOCKED2 &kvm->slots_lock

arch/x86/kvm/mmu/mmu.c slot_rmap_walk_next() -> rmap_walk_init_level()

Type Parameter Key Value
PARAM_VALUE 0 iterator 3311955574709174272
PARAM_VALUE 0 iterator->end_rmap 4096-ptr_max
PARAM_VALUE 0 iterator->level 2-3
PARAM_VALUE 0 iterator->rmap 4097-u64max
PARAM_VALUE 0 iterator->slot 4096-ptr_max
PARAM_VALUE 1 level 2-3
CAPPED_DATA 0 iterator->end_rmap 1
DATA_SOURCE 0 iterator $0
PARAM_COMPARE 0 iterator->end_level >= $0->level
PARAM_COMPARE 0 iterator->end_rmap < $0->rmap
PARAM_COMPARE 1 level <= $0->end_level
NOSPEC 0 iterator->start_gfn
RX_PATH
TASK_NOT_RUNNING
NOCHECK_CALL
USER_DATA 0 iterator->end_gfn 0-4503599627894781,u64max[u]
USER_DATA 0 iterator->gfn 0-9227875638629630013[c]
USER_DATA 0 iterator->start_gfn 0-s32max[c]
HALF_LOCKED2 &kvm->lock
HALF_LOCKED2 &kvm->mmu_lock
HALF_LOCKED2 &kvm->slots_lock