diff --git a/libsel4/arch_include/arm/sel4/arch/syscalls.h b/libsel4/arch_include/arm/sel4/arch/syscalls.h
index 5fba479558169496bbdafa07886f9be00536429f..e073d802363b563c090a3584a6b9a9de18a267a3 100644
--- a/libsel4/arch_include/arm/sel4/arch/syscalls.h
+++ b/libsel4/arch_include/arm/sel4/arch/syscalls.h
@@ -237,7 +237,7 @@ seL4_Wait(seL4_CPtr src, seL4_Word* sender)
     if (sender) {
         *sender = src_and_badge;
     }
-    return info;
+    return (seL4_MessageInfo_t){.words = {info.words[0]}};
 }
 
 static inline seL4_MessageInfo_t
@@ -279,7 +279,7 @@ seL4_WaitWithMRs(seL4_CPtr src, seL4_Word* sender,
     if (sender) {
         *sender = src_and_badge;
     }
-    return info;
+    return (seL4_MessageInfo_t){.words = {info.words[0]}};
 }
 
 static inline seL4_MessageInfo_t
@@ -308,7 +308,7 @@ seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
     seL4_SetMR(2, msg2);
     seL4_SetMR(3, msg3);
 
-    return info;
+    return (seL4_MessageInfo_t){.words = {info.words[0]}};
 }
 
 static inline seL4_MessageInfo_t
@@ -359,7 +359,7 @@ seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
         *mr3 = msg3;
     }
 
-    return info;
+    return (seL4_MessageInfo_t){.words = {info.words[0]}};
 }
 
 static inline seL4_MessageInfo_t
@@ -392,7 +392,7 @@ seL4_ReplyWait(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender)
     if (sender) {
         *sender = src_and_badge;
     }
-    return info;
+    return (seL4_MessageInfo_t){.words = {info.words[0]}};
 }
 
 static inline seL4_MessageInfo_t
@@ -447,7 +447,7 @@ seL4_ReplyWaitWithMRs(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *send
     if (sender) {
         *sender = src_and_badge;
     }
-    return info;
+    return (seL4_MessageInfo_t){.words = {info.words[0]}};
 }
 
 static inline void