diff options
| author | Xander <xander@biltopia.org> | 2023-08-20 22:57:07 +0200 |
|---|---|---|
| committer | Xander <xander@biltopia.org> | 2023-08-20 23:03:17 +0200 |
| commit | 70cca66089896730797a71ba545c7f4e87b12975 (patch) | |
| tree | 167a22d505b32bf80bd8b432833e12a74a98941b /kernel/memory/paging/table.sats | |
| parent | 7fce269442cb37810a14d088ea4a61d040ec3066 (diff) | |
| download | ats-os-70cca66089896730797a71ba545c7f4e87b12975.tar.xz ats-os-70cca66089896730797a71ba545c7f4e87b12975.zip | |
Diffstat (limited to 'kernel/memory/paging/table.sats')
| -rw-r--r-- | kernel/memory/paging/table.sats | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/kernel/memory/paging/table.sats b/kernel/memory/paging/table.sats index 491b77e..6b8e188 100644 --- a/kernel/memory/paging/table.sats +++ b/kernel/memory/paging/table.sats @@ -17,11 +17,10 @@ fun table_set_at{n:int}(table: !table_t(n), i: sizeLt(ENTRY_COUNT), x: entry_t): overload [] with table_get_at overload [] with table_set_at -// Set all the entries in the table to unused (zero) -fn set_zero(&Table_t):<!wrt> void - castfn consume(Table_t): void -fun get_P4() : table_t 0 +fn get_P4() : table_t 0 + +fn next_table{n : nat | n < 3}(table_t n, index : sizeLt(ENTRY_COUNT)) : Valid (table_t (n+1)) -fun next_table{n : nat | n < 3}(table_t n, sizeLt(ENTRY_COUNT)) : Valid (table_t (n+1)) +fn next_table_create{n : nat | n < 3}(table_t n, index : sizeLt(ENTRY_COUNT)) : Valid (table_t (n+1)) |