diff --git a/xen/arch/arm/domain.c b/xen/arch/arm/domain.c
index 2f8eaab7b5..2cd481979c 100644
--- a/xen/arch/arm/domain.c
+++ b/xen/arch/arm/domain.c
@@ -63,7 +63,7 @@ static void do_idle(void)
     rcu_idle_exit(cpu);
 }
 
-void idle_loop(void)
+static void noreturn idle_loop(void)
 {
     unsigned int cpu = smp_processor_id();
 
@@ -331,6 +331,9 @@ static void schedule_tail(struct vcpu *prev)
     update_vcpu_system_time(current);
 }
 
+extern void noreturn return_to_new_vcpu32(void);
+extern void noreturn return_to_new_vcpu64(void);
+
 static void continue_new_vcpu(struct vcpu *prev)
 {
     current->arch.actlr = READ_SYSREG(ACTLR_EL1);
diff --git a/xen/arch/arm/include/asm/current.h b/xen/arch/arm/include/asm/current.h
index 73e81458e5..6973eeb1d1 100644
--- a/xen/arch/arm/include/asm/current.h
+++ b/xen/arch/arm/include/asm/current.h
@@ -45,7 +45,7 @@ static inline struct cpu_info *get_cpu_info(void)
 #define guest_cpu_user_regs() (&get_cpu_info()->guest_cpu_user_regs)
 
 #define switch_stack_and_jump(stack, fn) do {                           \
-    asm volatile ("mov sp,%0; b " STR(fn) : : "r" (stack) : "memory" ); \
+    asm volatile ("mov sp,%0; b " STR(fn) : : "r" (stack), "X" (fn) : "memory" ); \
     unreachable();                                                      \
 } while ( false )