blob: e4569d63bb76836d9df7b58a876d771968cf90c1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
#include "kernel/prelude/kernel_prelude.hats"
#define ATS_DYNLOADFLAG 0
staload "./tss.sats"
staload UN = "prelude/SATS/unsafe.sats"
var tss : tss_t // Task State Segment
var stack1 : stack // Double fault stack
implement tss_init() : void = let
extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (tss_t@l)
prval (pf, fpf) = __assert (addr@(tss)) // takeout proof UNSAFE:
val sp1 = @{a = ptr_add<uint8>(addr@(stack1),STACK_SIZE)}
in
tss.ist.IS1 := sp1;
let prval () = fpf(pf) in end
end
|
