Type Definition setjmp::jmp_buf

type jmp_buf = [__jmp_buf_tag; 1];