<<>> <> <> <> <<>> ProcessStackCheck: CEDAR DEFINITIONS = BEGIN StackPushTest: PROC [bytes: INT ¬ 16*1024] RETURNS [BOOL]; <> END.