added 32 bit operand support

[palacios.git] / palacios / include / geekos / vmcs.h

diff --git a/palacios/include/geekos/vmcs.h b/palacios/include/geekos/vmcs.h
index 30af389..f73ec3d 100644 (file)
--- a/palacios/include/geekos/vmcs.h
+++ b/palacios/include/geekos/vmcs.h
@@ -350,10 +350,9 @@ union SegAccess {
 
 struct VMCSSegment {
   ushort_t selector   ; 
-  uint_t baseAddr     ; // should be 64 bits?
+  union SegAccess access;
   uint_t limit        ; 
-  union SegAccess access       ;
-
+  uint_t baseAddr     ; // should be 64 bits?
 };
 
 
@@ -560,15 +559,15 @@ struct VMXRegs {
   uint_t eax;
 };
   
-void SerialPrint_VMX_Regs(struct VMXRegs *regs);
-void SerialPrint_VMCSData(struct VMCSData * vmcs);
-void SerialPrint_VMCSGuestStateArea(struct VMCSGuestStateArea * guestState);
-void SerialPrint_VMCSHostStateArea(struct VMCSHostStateArea * hostState);
-void SerialPrint_VMCSExecCtrlFields(struct VMCSExecCtrlFields * execCtrls);
-void SerialPrint_VMCSExitCtrlFields(struct VMCSExitCtrlFields * exitCtrls);
-void SerialPrint_VMCSEntryCtrlFields(struct VMCSEntryCtrlFields * entryCtrls);
-void SerialPrint_VMCSExitInfoFields(struct VMCSExitInfoFields * exitInfo);
-void SerialPrint_VMCSSegment(char * segname, struct VMCSSegment * seg, int abbr);
+void PrintTrace_VMX_Regs(struct VMXRegs *regs);
+void PrintTrace_VMCSData(struct VMCSData * vmcs);
+void PrintTrace_VMCSGuestStateArea(struct VMCSGuestStateArea * guestState);
+void PrintTrace_VMCSHostStateArea(struct VMCSHostStateArea * hostState);
+void PrintTrace_VMCSExecCtrlFields(struct VMCSExecCtrlFields * execCtrls);
+void PrintTrace_VMCSExitCtrlFields(struct VMCSExitCtrlFields * exitCtrls);
+void PrintTrace_VMCSEntryCtrlFields(struct VMCSEntryCtrlFields * entryCtrls);
+void PrintTrace_VMCSExitInfoFields(struct VMCSExitInfoFields * exitInfo);
+void PrintTrace_VMCSSegment(char * segname, struct VMCSSegment * seg, int abbr);
 
 VMCS * CreateVMCS();
 extern uint_t VMCS_WRITE();
@@ -577,10 +576,6 @@ extern uint_t VMCS_READ();
 //uint_t VMCSRead(uint_t tag, void * val);
 
 
-
-
-
-#include <geekos/serial.h>
 #include <geekos/vmcs_gen.h>
 
 #endif