X-Git-Url: http://v3vee.org/palacios/gitweb/gitweb.cgi?a=blobdiff_plain;f=palacios%2Finclude%2Fgeekos%2Fvmcs.h;h=f73ec3d9e024a0a6dad677982c8de5883d1d6483;hb=a31286a91d6a84a60b34ee088517ee5d0d2176b0;hp=30af389405649d79b124fb34e8c8934ee773174b;hpb=626595465a2c6987606a6bc697df65130ad8c2d3;p=palacios.git

diff --git a/palacios/include/geekos/vmcs.h b/palacios/include/geekos/vmcs.h
index 30af389..f73ec3d 100644
--- 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