X-Git-Url: http://v3vee.org/palacios/gitweb/gitweb.cgi?a=blobdiff_plain;f=palacios%2Finclude%2Fpalacios%2Fvmx_lowlevel.h;h=c169139b34f6dc96f570ca5d21c45d72b551023f;hb=9b82fd29e9dc2b85339938098f77d8cf3487b099;hp=ce6a440f1ed08dc0a40fd1b48cb6800babd96dd7;hpb=24e7a3946e4d5c09377321e1f06479be9db8481f;p=palacios.git

diff --git a/palacios/include/palacios/vmx_lowlevel.h b/palacios/include/palacios/vmx_lowlevel.h
index ce6a440..c169139 100644
--- a/palacios/include/palacios/vmx_lowlevel.h
+++ b/palacios/include/palacios/vmx_lowlevel.h
@@ -97,17 +97,17 @@ static inline int vmcs_load(addr_t vmcs_ptr) {
     return VMX_SUCCESS;
 }
 
-static inline int vmcs_store(addr_t vmcs_ptr) {
-    uint64_t vmcs_ptr_64 = (uint64_t)vmcs_ptr;
+static inline addr_t vmcs_store() {
+    uint64_t vmcs_ptr = 0;
 
     __asm__ __volatile__ (
                VMPTRST_OPCODE
                EAX_07_MODRM
                :
-               : "a"(&vmcs_ptr_64)
+               : "a"(&vmcs_ptr)
                : "memory");
 
-    return VMX_SUCCESS;
+    return vmcs_ptr;
 }
 
 static inline int vmcs_read(vmcs_field_t vmcs_field, void * dst) {