[splint.git] / imports / setjmp.lcl

/*
** 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; }
Commit	Line	Data
885824d3	1	/*
	2	** setjmp.h
	3	*/
	4
	5	constant int JB_ONSIGSTK;
	6	constant int JB_SIGMASK;
	7	constant int JB_PC;
	8	constant int JB_REGS;
	9	constant int JB_ZERO;
	10	constant int JB_MAGIC;
	11	constant int JB_AT;
	12	constant int JB_V0;
	13	constant int JB_V1 ;
	14	constant int JB_A0 ;
	15	constant int JB_A1 ;
	16	constant int JB_A2 ;
	17	constant int JB_A3 ;
	18	constant int JB_T0 ;
	19	constant int JB_T1 ;
	20	constant int JB_T2 ;
	21	constant int JB_T3 ;
	22	constant int JB_T4 ;
	23	constant int JB_T5 ;
	24	constant int JB_T6 ;
	25	constant int JB_T7 ;
	26	constant int JB_S0 ;
	27	constant int JB_S1 ;
	28	constant int JB_S2 ;
	29	constant int JB_S3 ;
	30	constant int JB_S4 ;
	31	constant int JB_S5 ;
	32	constant int JB_S6 ;
	33	constant int JB_S7 ;
	34	constant int JB_T8 ;
	35	constant int JB_T9 ;
	36	constant int JB_K0 ;
	37	constant int JB_K1 ;
	38	constant int JB_GP ;
	39	constant int JB_SP ;
	40	constant int JB_S8 ;
	41	constant int JB_RA ;
	42
	43	constant int JB_FREGS ;
	44	constant int JB_F0 ;
	45	constant int JB_F1 ;
	46	constant int JB_F2 ;
	47	constant int JB_F3 ;
	48	constant int JB_F4 ;
	49	constant int JB_F5 ;
	50	constant int JB_F6 ;
	51	constant int JB_F7 ;
	52	constant int JB_F8 ;
	53	constant int JB_F9 ;
	54	constant int JB_F10 ;
	55	constant int JB_F11 ;
	56	constant int JB_F12 ;
	57	constant int JB_F13 ;
	58	constant int JB_F14 ;
	59	constant int JB_F15 ;
	60	constant int JB_F16 ;
	61	constant int JB_F17 ;
	62	constant int JB_F18 ;
	63	constant int JB_F19 ;
	64	constant int JB_F20 ;
65	constant int JB_F21 ;
66	constant int JB_F22 ;
67	constant int JB_F23 ;
68	constant int JB_F24 ;
69	constant int JB_F25 ;
70	constant int JB_F26 ;
71	constant int JB_F27 ;
72	constant int JB_F28 ;
73	constant int JB_F29 ;
74	constant int JB_F30 ;
75	constant int JB_F31 ;
76	constant int JB_FPC_CSR ;
77
78	constant int SC_MDLO ;
79	constant int SC_MDHI ;
80
81	constant int JB_FLAGS ;
82	constant int JBMAGIC ;
83
84	constant int SIGCONTEXT_PAD;
85	constant int NJBREGS ;
86
87	typedef int jmp_buf[];
88	typedef int sigjmp_buf[];
89
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; }
94