diff --git a/core/system/src/pool_queue.c b/core/system/src/pool_queue.c index fad35b77..00228d0a 100644 --- a/core/system/src/pool_queue.c +++ b/core/system/src/pool_queue.c @@ -17,6 +17,7 @@ #include "api/inc/linker_exports.h" #include "api/inc/pool_queue_exports.h" #include "api/inc/uvisor_spinlock_exports.h" +#include #include int uvisor_pool_init(uvisor_pool_t * pool, void * array, size_t stride, size_t num) @@ -46,6 +47,10 @@ int uvisor_pool_init(uvisor_pool_t * pool, void * array, size_t stride, size_t n uvisor_spin_init(&pool->spinlock); + UVISOR_STATIC_ASSERT( + sizeof(uvisor_pool_t) == offsetof(uvisor_pool_t, management_array), + management_array_offset_must_be_aligned_to_pool_structure_size); + return 0; }