diff options
Diffstat (limited to 'kernel/interrupts/idt.dats')
| -rw-r--r-- | kernel/interrupts/idt.dats | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/interrupts/idt.dats b/kernel/interrupts/idt.dats index ba6bb20..851a2b0 100644 --- a/kernel/interrupts/idt.dats +++ b/kernel/interrupts/idt.dats @@ -64,7 +64,7 @@ var idt : @[idt_entry_t][IDT_MAX_DESCRIPTORS] // The table var idtr : idtr_t // interrupt descriptor table register instance fun idt_set_descriptor {n : nat | n < IDT_MAX_DESCRIPTORS} (vector: int n, isr: uint64, flags: uint8) : void = let - extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (@[idt_entry_t][IDT_MAX_DESCRIPTORS]@l) + extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (@[idt_entry_t][IDT_MAX_DESCRIPTORS]@l) // takeout proof UNSAFE: prval (pf, fpf) = __assert (addr@(idt)) val x = $UN.cast{uint64}(0xFFFF) val y = $UN.cast{uint64}(0xFFFFFFF) @@ -118,7 +118,7 @@ end implement idt_init() : void = let extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (idtr_t@l) - prval (pf, fpf) = __assert (addr@(idtr)) + prval (pf, fpf) = __assert (addr@(idtr)) // takeout proof UNSAFE: in idtr.base := addr@(idt); idtr.limit := $UN.cast(8 * IDT_MAX_DESCRIPTORS); |