X-Git-Url: http://v3vee.org/palacios/gitweb/gitweb.cgi?a=blobdiff_plain;f=palacios%2Fsrc%2Fpalacios%2Fsvm_wbinvd.c;h=9d96f31bdde21e6923bd3b898e3343c7ea433557;hb=28cd2d6deca639fe40256c4d3f2c8f9491ec777a;hp=9fe3dc314f05ad1b4fb847774d472c5e8a20a54d;hpb=8a9058301d5a8dc0509aea2c52fed7cd93b7c38d;p=palacios.git

diff --git a/palacios/src/palacios/svm_wbinvd.c b/palacios/src/palacios/svm_wbinvd.c
index 9fe3dc3..9d96f31 100644
--- a/palacios/src/palacios/svm_wbinvd.c
+++ b/palacios/src/palacios/svm_wbinvd.c
@@ -30,13 +30,13 @@
 
 int v3_handle_svm_wbinvd(struct guest_info * info) {
 
-  if (info->cpl != 0) { 
-    PrintDebug("WBINVD: cpl != 0, injecting GPF\n");
-    v3_raise_exception(info, GPF_EXCEPTION);
-  } else {
-    info->rip += 2;
-    asm("wbinvd");
-  }
-
-  return 0;
+    if (info->cpl != 0) { 
+	PrintDebug(info->vm_info, info, "WBINVD: cpl != 0, injecting GPF\n");
+	v3_raise_exception(info, GPF_EXCEPTION);
+    } else {
+	info->rip += 2;
+	asm volatile ("wbinvd" ::: "memory");
+    }
+
+    return 0;
 }