+#ifdef CONFIG_VIRT_TIMER
+
+extern void vtime_start_cpu_timer(void);
+extern void vtime_stop_cpu_timer(void);
+
+#else
+
+static inline void vtime_start_cpu_timer(void) { }
+static inline void vtime_stop_cpu_timer(void) { }
+
+#endif /* CONFIG_VIRT_TIMER */
+