CONFIG_VTX checked within CONFIG_ARCH_ARM block?

[axel-h]

I'm a but confused about what commit e08dbb4 added. Looking at

capdl/capdl-loader-app/include/capdl.h

Lines 169 to 185 in e082ee7

	#if defined(CONFIG_ARCH_ARM)
	CDL_PT = seL4_ARM_PageTableObject,
	CDL_PD = seL4_ARM_PageDirectoryObject,
	CDL_Frame = seL4_ARM_SmallPageObject,
	#ifdef CONFIG_ARCH_AARCH64
	CDL_PUD = seL4_ARM_PageUpperDirectoryObject,
	#if !(defined(CONFIG_ARM_HYPERVISOR_SUPPORT) && defined (CONFIG_ARM_PA_SIZE_BITS_40))
	CDL_PGD = seL4_ARM_PageGlobalDirectoryObject,
	#endif
	#endif
	#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
	CDL_VCPU = seL4_ARM_VCPUObject,
	#endif
	#ifdef CONFIG_VTX
	CDL_VCPU = seL4_X86_VCPUObject,
	#endif
	#elif defined(CONFIG_ARCH_X86)

, there is a block for CONFIG_VTX within a CONFIG_ARCH_ARM block. Looks to me as if CDL_VCPU is never declared on CONFIG_ARCH_X86 at all then?

[corlewis]

I have to admit that I don't remember the details for this anymore or what the use case for it was, but it does look like you're right and that that commit is not correct. Looking purely at the code in that file, I would think that the CONFIG_VTX block should be moved to line 193, after the CONFIG_ARCH_X86_64 block and within the CONFIG_ARCH_X86 block.