Cleanup of linkage issues for non-Linux hosts

[palacios.git] / palacios / include / palacios / vmx_lowlevel.h

diff --git a/palacios/include/palacios/vmx_lowlevel.h b/palacios/include/palacios/vmx_lowlevel.h
index ce6a440..713875f 100644 (file)
--- 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 uint64_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) {
@@ -205,22 +205,22 @@ static inline int vmx_off() {
 static inline int enable_vmx() {
 #ifdef __V3_64BIT__
     __asm__ __volatile__ (
-                         "movq %%cr4, %%rbx;"
-                         "orq  $0x00002000, %%rbx;"
-                         "movq %%rbx, %%cr4;"
+                         "movq %%cr4, %%rcx;"
+                         "orq  $0x00002000, %%rcx;"
+                         "movq %%rcx, %%cr4;"
                          : 
                          :
-                         : "%rbx"
+                         : "%rcx"
                          );
 
 
     __asm__ __volatile__ (
-                         "movq %%cr0, %%rbx; "
-                         "orq  $0x00000020,%%rbx; "
-                         "movq %%rbx, %%cr0;"
+                         "movq %%cr0, %%rcx; "
+                         "orq  $0x00000020,%%rcx; "
+                         "movq %%rcx, %%cr0;"
                          :
                          :
-                         : "%rbx"
+                         : "%rcx"
                          );
 #elif __V3_32BIT__
     __asm__ __volatile__ (