update

[l4.git] / l4 / pkg / libvcpu / lib / src / vcpu.cc

diff --git a/l4/pkg/libvcpu/lib/src/vcpu.cc b/l4/pkg/libvcpu/lib/src/vcpu.cc
index 51bbe1be167a6e597162588deb9e11a1838f0524..abe6b44c8878282c49bfea13030fcf964a89f628 100644 (file)
--- a/l4/pkg/libvcpu/lib/src/vcpu.cc
+++ b/l4/pkg/libvcpu/lib/src/vcpu.cc
@@ -27,8 +27,9 @@ l4vcpu_print_state(l4_vcpu_state_t *vcpu,
 {
   printf("%svcpu=%p state=%x savedstate=%x label=%lx\n",
          prefix, vcpu, vcpu->state, vcpu->saved_state, vcpu->i.label);
-  printf("%ssticky=%x user_task=%lx\n",
-         prefix, vcpu->sticky_flags, vcpu->user_task << L4_CAP_SHIFT);
+  printf("%ssticky=%x user_task=%lx  pfa=%lx\n",
+         prefix, vcpu->sticky_flags, vcpu->user_task << L4_CAP_SHIFT,
+         vcpu->r.pfa);
   printf("%sentry_sp=%lx entry_ip=%lx\n",
          prefix, vcpu->entry_sp, vcpu->entry_ip);
   l4vcpu_print_state_arch(vcpu, prefix);