Defined in 1 files as a function:

Referenced in 1 files:

Smatch caller information:

arch/x86/kvm/vmx/vmx.c atomic_switch_perf_msrs() -> add_atomic_switch_msr()

Type Parameter Key Value
PARAM_VALUE 0 vmx 4096-ptr_max
PARAM_VALUE 0 vmx->loaded_vmcs 4096-ptr_max
PARAM_VALUE 0 vmx->loaded_vmcs->soft_vnmi_blocked 0-1
PARAM_VALUE 0 vmx->ple_window_dirty 0
PARAM_VALUE 0 vmx->vt.emulation_required 0
CAPPED_DATA 0 vmx->loaded_vmcs->host_state.cr3 1
DATA_SOURCE 0 vmx $0
NOCHECK_CALL

arch/x86/kvm/vmx/vmx.c update_transition_efer() -> add_atomic_switch_msr()

Type Parameter Key Value
PARAM_VALUE 0 vmx 4096-ptr_max
PARAM_VALUE 0 vmx->ve_info 18379471554275704832,18446612682070032384
PARAM_VALUE 0 vmx->vmcs01.msr_bitmap 0,18379471554275704832,18446612682070032384
PARAM_VALUE 0 vmx->vpid 0-64
PARAM_VALUE 1 msr 3221225600
PARAM_VALUE 2 guest_val 1-u64max
DATA_SOURCE 0 vmx $0
PARAM_COMPARE 2 guest_val > $3
PARAM_COMPARE 2 guest_val > $3
PARAM_COMPARE 3 host_val < $2
NOCHECK_CALL