/*
** setjmp.h
*/

constant int JB_ONSIGSTK;
constant int JB_SIGMASK;
constant int JB_PC;
constant int JB_REGS;
constant int JB_ZERO;
constant int JB_MAGIC;
constant int JB_AT;
constant int JB_V0;
constant int JB_V1	;
constant int JB_A0	;
constant int JB_A1	;
constant int JB_A2	;
constant int JB_A3	;
constant int JB_T0		;
constant int JB_T1	;
constant int JB_T2	;
constant int JB_T3	;
constant int JB_T4	;
constant int JB_T5	;
constant int JB_T6	;
constant int JB_T7	;
constant int JB_S0		;
constant int JB_S1	;
constant int JB_S2	;
constant int JB_S3	;
constant int JB_S4	;
constant int JB_S5	;
constant int JB_S6	;
constant int JB_S7	;
constant int JB_T8	;
constant int JB_T9	;
constant int JB_K0	;
constant int JB_K1	;
constant int JB_GP	;
constant int JB_SP	;
constant int JB_S8	;
constant int JB_RA	;

constant int JB_FREGS   ;
constant int JB_F0	;
constant int JB_F1	;
constant int JB_F2	;
constant int JB_F3	;
constant int JB_F4	;
constant int JB_F5	;
constant int JB_F6	;
constant int JB_F7	;
constant int JB_F8	;
constant int JB_F9	;
constant int JB_F10	;
constant int JB_F11	;
constant int JB_F12	;
constant int JB_F13	;
constant int JB_F14	;
constant int JB_F15	;
constant int JB_F16	;
constant int JB_F17	;
constant int JB_F18	;
constant int JB_F19	;
constant int JB_F20	;
constant int JB_F21	;
constant int JB_F22	;
constant int JB_F23	;
constant int JB_F24	;
constant int JB_F25	;
constant int JB_F26	;
constant int JB_F27	;
constant int JB_F28	;
constant int JB_F29	;
constant int JB_F30	;
constant int JB_F31	;
constant int JB_FPC_CSR ;

constant int SC_MDLO	;
constant int SC_MDHI	;

constant int JB_FLAGS   ;
constant int JBMAGIC	;

constant int SIGCONTEXT_PAD;
constant int NJBREGS	;
 
typedef int jmp_buf[];
typedef int sigjmp_buf[];

void  longjmp( jmp_buf __env, int __val ) { ensures true; }
int   setjmp( jmp_buf __env ) { ensures true; }
int   sigsetjmp(sigjmp_buf __env, int __savemask) { ensures true; }
void  siglongjmp( sigjmp_buf __env, int __val) { ensures true; }