imports/setjmp.lcl

   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