blob: 9a103f4cc51c2bf0b81ebe6cbafc3521716f113e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
#define ENTRY_COUNT 512
staload "./entry.sats"
staload "lib/SATS/valid.sats"
staload "lib/DATS/valid.dats"
typedef table_t = @[entry_t][ENTRY_COUNT]
vtypedef tablePtr1(c : int) = @{
ptr = [l : agz] (table_t@l , table_t@l -<lin,prf> void | ptr l),
level = (uint c | )
}
// Set all the entries in the table to unused (zero)
fn set_zero(&table_t): void
fun get_P4() : tablePtr1(0)
fun next_table{n : nat | n < 3}(tablePtr1(n), sizeLt(ENTRY_COUNT)) : Valid (tablePtr1(n+1))
|
