Merge branch 'devel' of palacios@newskysaw.cs.northwestern.edu:/home/palacios/palacio...

[palacios-OLD.git] / palacios / include / palacios / vmm_time.h

diff --git a/palacios/include/palacios/vmm_time.h b/palacios/include/palacios/vmm_time.h
index 3255aca..c9248b8 100644 (file)
--- a/palacios/include/palacios/vmm_time.h
+++ b/palacios/include/palacios/vmm_time.h
@@ -93,11 +93,8 @@ static inline uint64_t v3_get_host_time(struct vm_time *t) {
 // Returns *monotonic* guest time.
 static inline uint64_t v3_get_guest_time(struct vm_time *t) {
 #ifdef CONFIG_TIME_HIDE_VM_COST
-    if (t->exit_time) {
-        return t->exit_time + t->guest_host_offset;
-    } else {
-        return v3_get_host_time(t) + t->guest_host_offset;
-    }
+    V3_ASSERT(t->exit_time);
+    return t->exit_time + t->guest_host_offset;
 #else
     return v3_get_host_time(t) + t->guest_host_offset;
 #endif