Defined in 1 files as a function:

Referenced in 1 files:

Smatch caller information:

arch/x86/kvm/vmx/vmx.c vmx_vcpu_create() -> vmx_destroy_pml_buffer()

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->controls_shadow.exec 0
PARAM_VALUE 0 vmx->loaded_vmcs->controls_shadow.pin 0
PARAM_VALUE 0 vmx->loaded_vmcs->cpu (-1)
PARAM_VALUE 0 vmx->loaded_vmcs->host_state.cr3 0
PARAM_VALUE 0 vmx->loaded_vmcs->host_state.cr4 0
PARAM_VALUE 0 vmx->loaded_vmcs->host_state.ds_sel 0
PARAM_VALUE 0 vmx->loaded_vmcs->host_state.es_sel 0
PARAM_VALUE 0 vmx->loaded_vmcs->host_state.fs_base 0
PARAM_VALUE 0 vmx->loaded_vmcs->host_state.fs_sel 0
PARAM_VALUE 0 vmx->loaded_vmcs->host_state.gs_base 0
PARAM_VALUE 0 vmx->loaded_vmcs->host_state.gs_sel 0
PARAM_VALUE 0 vmx->loaded_vmcs->host_state.ldt_sel 0
PARAM_VALUE 0 vmx->loaded_vmcs->host_state.rsp 0
PARAM_VALUE 0 vmx->loaded_vmcs->launched 0
PARAM_VALUE 0 vmx->loaded_vmcs->msr_bitmap 0,18379471554275704832,18446612682070032384
PARAM_VALUE 0 vmx->loaded_vmcs->shadow_vmcs 0
PARAM_VALUE 0 vmx->loaded_vmcs->vmcs 18379471554275704832,18446612682070032384
PARAM_VALUE 0 vmx->vmcs01.msr_bitmap 0,18379471554275704832,18446612682070032384
PARAM_VALUE 0 vmx->vmcs01.shadow_vmcs 0,18379471554275704832,18446612682070032384
PARAM_VALUE 0 vmx->vmcs01.vmcs 0,18379471554275704832,18446612682070032384
PARAM_VALUE 0 vmx->vpid 0-64
PARAM_VALUE 0 vmx->vt.pi_wakeup_list.next 4096-ptr_max
PARAM_VALUE 0 vmx->vt.pi_wakeup_list.next->next 4096-ptr_max
PARAM_VALUE 0 vmx->vt.pi_wakeup_list.prev 4096-ptr_max
PARAM_VALUE 0 vmx->vt.pi_wakeup_list.prev->next 4096-ptr_max
PARAM_VALUE 0 vmx->vt.pi_wakeup_list.prev->prev 4096-ptr_max
BUF_SIZE 0 vmx->loaded_vmcs (-1),160
CAPPED_DATA 0 vmx->vpid 1
DATA_SOURCE 0 vmx r to_vmx
NOCHECK_CALL

arch/x86/kvm/vmx/vmx.c vmx_vcpu_free() -> vmx_destroy_pml_buffer()

Type Parameter Key Value
PARAM_VALUE 0 vmx 4096-ptr_max
DATA_SOURCE 0 vmx r to_vmx
NOCHECK_CALL