Imagelibrary/seL4
1
0
Fork 1
mirror of https://github.com/seL4/seL4.git synced 2026-04-04 22:39:54 +00:00
Code Issues Packages Projects Releases Wiki Activity

aarch64/vspace: add performASIDControl annotations

Browse Source 
Type and ghost state annotations for verification.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein
2024-01-10 10:04:39 +11:00
parent 5d1f3bc3ce
commit 2b29446484
1 changed files with 3 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
src/arch/arm/64/kernel/vspace.c
View File

@@ -1244,10 +1244,13 @@ static exception_t performPageGetAddress(pptr_t base_ptr, bool_t call)
static exception_t performASIDControlInvocation(void *frame, cte_t *slot,
cte_t *parent, asid_t asid_base)
{
/** AUXUPD: "(True, typ_region_bytes (ptr_val \<acute>frame) 12)" */
/** GHOSTUPD: "(True, gs_clear_region (ptr_val \<acute>frame) 12)" */
cap_untyped_cap_ptr_set_capFreeIndex(&(parent->cap),
MAX_FREE_INDEX(cap_untyped_cap_get_capBlockSize(parent->cap)));
memzero(frame, BIT(seL4_ASIDPoolBits));
/** AUXUPD: "(True, ptr_retyps 1 (Ptr (ptr_val \<acute>frame) :: asid_pool_C ptr))" */
cteInsert(
cap_asid_pool_cap_new(