Defined in 1 files as a function:

Referenced in 1 files:

Smatch caller information:

arch/x86/kvm/vmx/nested.c copy_shadow_to_vmcs12() -> vmcs12_write_any()

Type Parameter Key Value
DATA_SOURCE 0 vmcs12 r get_vmcs12
DATA_SOURCE 3 field_value r __vmcs_readl
PREEMPT_ADD <- disables preempt
NOCHECK_CALL

arch/x86/kvm/vmx/nested.c handle_vmwrite() -> vmcs12_write_any()

Type Parameter Key Value
PARAM_VALUE 2 offset 1-s16max
CAPPED_DATA 1 field 1
CAPPED_DATA 1 field 1
DATA_SOURCE 1 field r kvm_register_read
DATA_SOURCE 2 offset r get_vmcs12_field_offset
NOSPEC 1 field
NOCHECK_CALL
USER_DATA 1 field 0-u64max[c]
USER_DATA 3 field_value 0-u64max