From e02a7e790650b31b713dde5c39ad6172c048f571 Mon Sep 17 00:00:00 2001 From: Xander Date: Thu, 13 Jul 2023 00:26:49 +0200 Subject: int to string conversion implementation --- kernel/interrupts/idt.dats | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/interrupts/idt.dats') 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); -- cgit v1.2.3