On Fri, Feb 09, 2024 at 12:51:41PM +0100, Jan Beulich wrote:
> On 09.02.2024 11:45, Roger Pau Monné wrote:
> > On Thu, Feb 08, 2024 at 02:40:53PM +0100, Jan Beulich wrote:
> >> On 06.02.2024 15:25, Roger Pau Monne wrote:
> >>> @@ -2086,6 +2091,9 @@ void vmcs_dump_vcpu(struct vcpu *v)
> >>> if ( v->arch.hvm.vmx.secondary_exec_control &
> >>> SECONDARY_EXEC_VIRTUAL_INTR_DELIVERY )
> >>> printk("InterruptStatus = %04x\n", vmr16(GUEST_INTR_STATUS));
> >>> + if ( cpu_has_vmx_virt_spec_ctrl )
> >>> + printk("SPEC_CTRL mask = %#016lx shadow = %#016lx\n",
> >>> + vmr(SPEC_CTRL_MASK), vmr(SPEC_CTRL_SHADOW));
> >>
> >> #0... doesn't make a lot of sense; only e.g. %#lx does. Seeing context
> >> there's no 0x prefix there anyway. Having looked at the function the
> >> other day, I know though that there's a fair mix of 0x-prefixed and
> >> unprefixed hex numbers that are output.
> >
> > For consistency with how other MSRs are printed I should use the '0x'
> > prefix.
>
> MSRs? It's VMCS fields which are printed here.
Well, yes, but it represents a MSR value.
Thanks, Roger.
