From 260d6f0e0625a32d8a2d790d7ffc9bc4f78f5ef5 Mon Sep 17 00:00:00 2001 From: julia Date: Wed, 12 Feb 2025 17:17:38 +1100 Subject: [PATCH] vspace004: allocate a cap for the final pool This *coincidentally* fails with ret == seL4_RevokeFirst(9) if the number of pools to allocate before failing is less than the actual amount, because we don't allocate a capability for the last pool. In essence, that could be happening even if we had the correct number of pools, but doesn't because of how the kernel (presumably) checks that the cap is free after checking the ASID pools are free. Signed-off-by: julia --- apps/sel4test-tests/src/tests/vspace.c | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/apps/sel4test-tests/src/tests/vspace.c b/apps/sel4test-tests/src/tests/vspace.c index 86b710a8..83d0da8f 100644 --- a/apps/sel4test-tests/src/tests/vspace.c +++ b/apps/sel4test-tests/src/tests/vspace.c @@ -183,9 +183,15 @@ test_run_out_asid_pools(env_t env) pool = vka_alloc_untyped_leaky(vka, seL4_PageBits); test_assert(pool); ret = vka_cspace_alloc_path(vka, &path); + test_eq(ret, seL4_NoError); ret = seL4_ARCH_ASIDControl_MakePool(env->asid_ctrl, pool, env->cspace_root, path.capPtr, path.capDepth); test_eq(ret, seL4_NoError); } + + pool = vka_alloc_untyped_leaky(vka, seL4_PageBits); + test_assert(pool); + ret = vka_cspace_alloc_path(vka, &path); + test_eq(ret, seL4_NoError); /* We do one more pool allocation that is supposed to fail (at this point there shouldn't be any more available) */ ret = seL4_ARCH_ASIDControl_MakePool(env->asid_ctrl, pool, env->cspace_root, path.capPtr, path.capDepth); test_eq(ret, seL4_DeleteFirst);