Skip to content

Commit 260d6f0

Browse files
committed
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 <git.ts@trainwit.ch>
1 parent 3583555 commit 260d6f0

File tree

1 file changed

+6
-0
lines changed

1 file changed

+6
-0
lines changed

apps/sel4test-tests/src/tests/vspace.c

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -183,9 +183,15 @@ test_run_out_asid_pools(env_t env)
183183
pool = vka_alloc_untyped_leaky(vka, seL4_PageBits);
184184
test_assert(pool);
185185
ret = vka_cspace_alloc_path(vka, &path);
186+
test_eq(ret, seL4_NoError);
186187
ret = seL4_ARCH_ASIDControl_MakePool(env->asid_ctrl, pool, env->cspace_root, path.capPtr, path.capDepth);
187188
test_eq(ret, seL4_NoError);
188189
}
190+
191+
pool = vka_alloc_untyped_leaky(vka, seL4_PageBits);
192+
test_assert(pool);
193+
ret = vka_cspace_alloc_path(vka, &path);
194+
test_eq(ret, seL4_NoError);
189195
/* We do one more pool allocation that is supposed to fail (at this point there shouldn't be any more available) */
190196
ret = seL4_ARCH_ASIDControl_MakePool(env->asid_ctrl, pool, env->cspace_root, path.capPtr, path.capDepth);
191197
test_eq(ret, seL4_DeleteFirst);

0 commit comments

Comments
 (0)