X-Git-Url: http://v3vee.org/palacios/gitweb/gitweb.cgi?a=blobdiff_plain;f=palacios%2Fsrc%2Fpalacios%2Fvmx.c;h=f71df0a7bc23b3a7c2435f559d55525e5ffd9e48;hb=22c7f98617f63f097b08e8159383c23aa6d9ad33;hp=6d50ff3ad4721dd72e00a68d6c9bb01401b5e122;hpb=29b7ff8811c82ab543f5c969e44ff217637a09c7;p=palacios.git

diff --git a/palacios/src/palacios/vmx.c b/palacios/src/palacios/vmx.c
index 6d50ff3..f71df0a 100644
--- a/palacios/src/palacios/vmx.c
+++ b/palacios/src/palacios/vmx.c
@@ -857,7 +857,8 @@ void v3_init_vmx_cpu(int cpu_id) {
     struct v3_msr tmp_msr;
     uint64_t ret = 0;
 
-    v3_get_msr(VMX_CR4_FIXED0_MSR,&(tmp_msr.hi),&(tmp_msr.lo));
+    v3_get_msr(VMX_CR4_FIXED0_MSR, &(tmp_msr.hi), &(tmp_msr.lo));
+
 #ifdef __V3_64BIT__
     __asm__ __volatile__ (
 			  "movq %%cr4, %%rbx;"
@@ -944,3 +945,9 @@ void v3_init_vmx_cpu(int cpu_id) {
 
 }
 
+
+void v3_deinit_vmx_cpu(int cpu_id) {
+    extern v3_cpu_arch_t v3_cpu_types[];
+    v3_cpu_types[cpu_id] = V3_INVALID_CPU;
+    V3_FreePages((void *)host_vmcs_ptrs[cpu_id], 1);
+}