/usr/share/splint/imports/setjmp.lcl is in splint-data 3.1.2.dfsg1-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 | /*
** 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; }
|