Defined in 1 files as a function:

Referenced in 2 files:

Smatch caller information:

arch/x86/kvm/vmx/nested.c vmx_complete_nested_posted_interrupt() -> kvm_vcpu_map_mark_dirty()

Type Parameter Key Value
PARAM_VALUE 0 vcpu 4096-ptr_max
PARAM_VALUE 0 vcpu->arch.apic 0,4096-ptr_max
PARAM_VALUE 0 vcpu->run->hypercall.ret 0-s32max,18446744071562067968-u64max
PARAM_VALUE 1 map 4096-ptr_max
DATA_SOURCE 0 vcpu $0
NOCHECK_CALL

arch/x86/kvm/vmx/nested.c vmx_complete_nested_posted_interrupt() -> kvm_vcpu_map_mark_dirty()

Type Parameter Key Value
PARAM_VALUE 0 vcpu 4096-ptr_max
PARAM_VALUE 0 vcpu->arch.apic 0,4096-ptr_max
PARAM_VALUE 0 vcpu->last_used_slot->base_gfn 0-18446744073709551614
PARAM_VALUE 0 vcpu->run->hypercall.ret 0-s32max,18446744071562067968-u64max
PARAM_VALUE 1 map 4096-ptr_max
DATA_SOURCE 0 vcpu $0
NOCHECK_CALL

arch/x86/kvm/vmx/vmx.c nested_vmx_mark_all_vmcs12_pages_dirty() -> kvm_vcpu_map_mark_dirty()

Type Parameter Key Value
PARAM_VALUE 0 vcpu 4096-ptr_max
PARAM_VALUE 0 vcpu->arch.nested_run_pending 0
PARAM_VALUE 0 vcpu->kvm 4096-ptr_max
PARAM_VALUE 1 map 4096-ptr_max
DATA_SOURCE 0 vcpu $0
NOCHECK_CALL

arch/x86/kvm/vmx/vmx.c nested_vmx_mark_all_vmcs12_pages_dirty() -> kvm_vcpu_map_mark_dirty()

Type Parameter Key Value
PARAM_VALUE 0 vcpu 4096-ptr_max
PARAM_VALUE 0 vcpu->arch.nested_run_pending 0
PARAM_VALUE 0 vcpu->kvm 4096-ptr_max
PARAM_VALUE 0 vcpu->last_used_slot->base_gfn 0-18446744073709551614
PARAM_VALUE 1 map 4096-ptr_max
CAPPED_DATA 0 vcpu->kvm 1
DATA_SOURCE 0 vcpu $0
NOCHECK_CALL

arch/x86/kvm/vmx/vmx.c nested_vmx_mark_all_vmcs12_pages_dirty() -> kvm_vcpu_map_mark_dirty()

Type Parameter Key Value
PARAM_VALUE 0 vcpu 4096-ptr_max
PARAM_VALUE 0 vcpu->arch.nested_run_pending 0
PARAM_VALUE 0 vcpu->kvm 4096-ptr_max
PARAM_VALUE 0 vcpu->last_used_slot->base_gfn 0-18446744073709551614
PARAM_VALUE 1 map 4096-ptr_max
CAPPED_DATA 0 vcpu->kvm 1
DATA_SOURCE 0 vcpu $0
NOCHECK_CALL