UNSAFE MODULE--------------------------------------------------------- thread stacks ---RTThread EXPORTSRTThread ; PROCEDURESP (<*UNUSED*> READONLY s: State): ADDRESS = BEGIN <* ASSERT(FALSE) *> END SP;
PROCEDURE-------------------------------------------------- modifying the models ---NewStack (<*UNUSED*> size: INTEGER; <*UNUSED*> VAR(*OUT*)s: Stack) = BEGIN <* ASSERT(FALSE) *> END NewStack; PROCEDUREDisposeStack (<*UNUSED*> VAR s: Stack) = BEGIN <* ASSERT(FALSE) *> END DisposeStack; PROCEDUREFlushStackCache () = (*VAR d: State;*) BEGIN (*Transfer (d, d);*) <* ASSERT(FALSE) *> END FlushStackCache;
PROCEDURE---------------------------------------------------------------------------UpdateStateForNewSP (<*UNUSED*> VAR s: State; <*UNUSED*> offset: INTEGER) = BEGIN <* ASSERT(FALSE) *> END UpdateStateForNewSP; PROCEDUREUpdateFrameForNewSP (<*UNUSED*> a: ADDRESS; <*UNUSED*> offset: INTEGER) = BEGIN <* ASSERT(FALSE) *> END UpdateFrameForNewSP;
BEGIN END RTThread.