diff --git a/drivers/rpmsg/rpmsg_port_spi.c b/drivers/rpmsg/rpmsg_port_spi.c
index 8514a9ea6e..64b26cdaba 100644
--- a/drivers/rpmsg/rpmsg_port_spi.c
+++ b/drivers/rpmsg/rpmsg_port_spi.c
@@ -26,6 +26,7 @@
 #include <errno.h>
 #include <stdio.h>
 
+#include <nuttx/nuttx.h>
 #include <nuttx/crc16.h>
 #include <nuttx/kmalloc.h>
 #include <nuttx/kthread.h>
diff --git a/drivers/rptun/rptun_ivshmem.c b/drivers/rptun/rptun_ivshmem.c
index 34ad6030b1..0e970e573c 100644
--- a/drivers/rptun/rptun_ivshmem.c
+++ b/drivers/rptun/rptun_ivshmem.c
@@ -28,6 +28,7 @@
 #include <errno.h>
 #include <stdio.h>
 
+#include <nuttx/nuttx.h>
 #include <nuttx/board.h>
 #include <nuttx/drivers/addrenv.h>
 #include <nuttx/pci/pci_ivshmem.h>
diff --git a/fs/v9fs/virtio_9p.c b/fs/v9fs/virtio_9p.c
index 652361add5..67e470d2cd 100644
--- a/fs/v9fs/virtio_9p.c
+++ b/fs/v9fs/virtio_9p.c
@@ -25,6 +25,7 @@
 #include <debug.h>
 #include <errno.h>
 
+#include <nuttx/nuttx.h>
 #include <nuttx/spinlock.h>
 #include <nuttx/virtio/virtio.h>