5 constant int JB_ONSIGSTK;
6 constant int JB_SIGMASK;
10 constant int JB_MAGIC;
43 constant int JB_FREGS ;
76 constant int JB_FPC_CSR ;
78 constant int SC_MDLO ;
79 constant int SC_MDHI ;
81 constant int JB_FLAGS ;
82 constant int JBMAGIC ;
84 constant int SIGCONTEXT_PAD;
85 constant int NJBREGS ;
87 typedef int jmp_buf[];
88 typedef int sigjmp_buf[];
90 void longjmp( jmp_buf __env, int __val ) { ensures true; }
91 int setjmp( jmp_buf __env ) { ensures true; }
92 int sigsetjmp(sigjmp_buf __env, int __savemask) { ensures true; }
93 void siglongjmp( sigjmp_buf __env, int __val) { ensures true; }