Defined in 1 files as a function:

No references found in the database

Smatch caller information:

arch/x86/kvm/vmx/tdx.c td_state_non_arch_read64() -> tdvps_state_non_arch_check()

Type Parameter Key Value
PARAM_VALUE 0 field 256
PARAM_VALUE 1 bits 64
DATA_SOURCE 0 field $1
NOCHECK_CALL