diff --git a/include/arch/arm/arch/fastpath/fastpath.h b/include/arch/arm/arch/fastpath/fastpath.h
index 00b2e0491..d66bdb19a 100644
--- a/include/arch/arm/arch/fastpath/fastpath.h
+++ b/include/arch/arm/arch/fastpath/fastpath.h
@@ -17,6 +17,7 @@
 void slowpath(syscall_t syscall)
 VISIBLE NORETURN;
 
+/** DONT_TRANSLATE */
 static inline void NORETURN fastpath_restore(word_t badge, word_t msgInfo, tcb_t *cur_thread)
 {
     register word_t badge_reg asm("r0") = badge;
diff --git a/src/arch/arm/32/c_traps.c b/src/arch/arm/32/c_traps.c
index 8e07ad2a3..06bb40aa7 100644
--- a/src/arch/arm/32/c_traps.c
+++ b/src/arch/arm/32/c_traps.c
@@ -15,6 +15,7 @@
 
 #include <api/syscall.h>
 
+/** DONT_TRANSLATE */
 void VISIBLE c_handle_syscall(word_t cptr, word_t msgInfo, syscall_t syscall)
 {
 #ifdef CONFIG_FASTPATH