2 files changed, 8 insertions, 2 deletions
diff --git a/src/cpu/intel/common/common.h b/src/cpu/intel/common/common.h
index 909f75ac40..ef0a5d9044 100644
--- a/src/cpu/intel/common/common.h
+++ b/src/cpu/intel/common/common.h
@@ -8,6 +8,7 @@
 
 void set_vmx_and_lock(void);
 void set_feature_ctrl_vmx(void);
+void set_feature_ctrl_vmx_arg(bool enable);
 void set_feature_ctrl_lock(void);
 
 /*
diff --git a/src/cpu/intel/common/common_init.c b/src/cpu/intel/common/common_init.c
index 765a174dd1..0f40e4b1dd 100644
--- a/src/cpu/intel/common/common_init.c
+++ b/src/cpu/intel/common/common_init.c
@@ -16,11 +16,10 @@ void set_vmx_and_lock(void)
 	set_feature_ctrl_lock();
 }
 
-void set_feature_ctrl_vmx(void)
+void set_feature_ctrl_vmx_arg(bool enable)
 {
 	msr_t msr;
 	uint32_t feature_flag;
-	int enable = CONFIG(ENABLE_VMX);
 
 	feature_flag = cpu_get_feature_flags_ecx();
 	/* Check that the VMX is supported before reading or writing the MSR. */
@@ -62,6 +61,12 @@ void set_feature_ctrl_vmx(void)
 	printk(BIOS_DEBUG, "VMX status: %s\n",
 		enable ? "enabled" : "disabled");
 }
+
+void set_feature_ctrl_vmx(void)
+{
+	set_feature_ctrl_vmx_arg(CONFIG(ENABLE_VMX));
+}
+
 void set_feature_ctrl_lock(void)
 {
 	msr_t msr;