/* Generated by CIL v. 1.3.7 */
/* print_CIL_Input is true */

#line 44 "../dma_example.h"
struct _control_block {
   unsigned long long in_addr ;
   unsigned long long out_addr ;
   unsigned int num_elements_per_spe ;
   unsigned int id ;
   unsigned int pad[2] ;
};
#line 44 "../dma_example.h"
typedef struct _control_block control_block_t;
#line 339 "/usr/include/stdio.h"
extern int printf(char const   * __restrict  __format  , ...) ;
#line 203 "../spu_mfcio.h"
extern void mfc_put(void volatile   *ls , unsigned int ea , unsigned int size , unsigned int tag ,
                    unsigned int tid , unsigned int rid ) ;
#line 211
extern void mfc_get(void volatile   *ls , unsigned int ea , unsigned int size , unsigned int tag ,
                    unsigned int tid , unsigned int rid ) ;
#line 252
extern void mfc_write_tag_mask(unsigned int mask ) ;
#line 270
extern void mfc_read_tag_status_all() ;
#line 27 "dma_example_spu.c"
float local_buffer_in[4096]  __attribute__((__aligned__(128)))  ;
#line 35 "dma_example_spu.c"
float local_buffer_out[4096]  __attribute__((__aligned__(128)))  ;
#line 42 "dma_example_spu.c"
control_block_t control_block  __attribute__((__aligned__(128)))  ;
#line 103
extern int __VERIFIER_nondet_int() ;
#line 121
extern int ( /* missing proto */  assert)() ;
#line 76 "dma_example_spu.c"
int spu_main(unsigned long long speid  __attribute__((__unused__)) , unsigned long long argp ,
             unsigned long long envp  __attribute__((__unused__)) ) 
{ unsigned int tag ;
  unsigned long long in_addr ;
  unsigned long long out_addr ;
  int i ;
  int num_chunks ;
  int tmp ;
  int tmp___0 ;
  int tmp___1 ;
  int tmp___2 ;
  int tmp___3 ;
  int tmp___4 ;
  char const   * __restrict  __cil_tmp15 ;
  void volatile   *__cil_tmp16 ;
  unsigned int __cil_tmp17 ;
  unsigned int __cil_tmp18 ;
  control_block_t *__cil_tmp19 ;
  unsigned long __cil_tmp20 ;
  unsigned long __cil_tmp21 ;
  unsigned long __cil_tmp22 ;
  unsigned long __cil_tmp23 ;
  unsigned long __cil_tmp24 ;
  unsigned long __cil_tmp25 ;
  unsigned long __cil_tmp26 ;
  unsigned long __cil_tmp27 ;
  unsigned long __cil_tmp28 ;
  int __cil_tmp29 ;
  unsigned int __cil_tmp30 ;
  unsigned long __cil_tmp31 ;
  unsigned int __cil_tmp32 ;
  unsigned int __cil_tmp33 ;
  int __cil_tmp34 ;
  int __cil_tmp35 ;
  unsigned long __cil_tmp36 ;
  unsigned long __cil_tmp37 ;
  unsigned long long __cil_tmp38 ;
  control_block_t *__cil_tmp39 ;
  unsigned long long __cil_tmp40 ;
  int __cil_tmp41 ;
  unsigned long __cil_tmp42 ;
  unsigned long __cil_tmp43 ;
  unsigned long long __cil_tmp44 ;
  unsigned long __cil_tmp45 ;
  unsigned long long __cil_tmp46 ;
  unsigned long __cil_tmp47 ;
  unsigned long __cil_tmp48 ;
  float *__cil_tmp49 ;
  void volatile   *__cil_tmp50 ;
  unsigned int __cil_tmp51 ;
  unsigned long __cil_tmp52 ;
  unsigned int __cil_tmp53 ;
  int __cil_tmp54 ;
  unsigned int __cil_tmp55 ;
  unsigned long __cil_tmp56 ;
  unsigned long __cil_tmp57 ;
  float *__cil_tmp58 ;
  void volatile   *__cil_tmp59 ;
  unsigned int __cil_tmp60 ;
  unsigned long __cil_tmp61 ;
  unsigned int __cil_tmp62 ;
  int __cil_tmp63 ;
  unsigned int __cil_tmp64 ;

  {
#line 92
  tag = 0U;
#line 94
  if (tag == 4294967295U) {
    {
#line 96
    __cil_tmp15 = (char const   * __restrict  )"SPU ERROR, unable to reserve tag\n";
#line 96
    printf(__cil_tmp15);
    }
#line 97
    return (1);
  } else {

  }
  {
#line 102
  __cil_tmp16 = (void volatile   *)(& control_block);
#line 102
  __cil_tmp17 = (unsigned int )argp;
#line 102
  __cil_tmp18 = (unsigned int )32UL;
#line 102
  mfc_get(__cil_tmp16, __cil_tmp17, __cil_tmp18, tag, 0U, 0U);
#line 103
  tmp = __VERIFIER_nondet_int();
#line 103
  __cil_tmp19 = & control_block;
#line 103
  *((unsigned long long *)__cil_tmp19) = (unsigned long long )tmp;
#line 103
  tmp___0 = __VERIFIER_nondet_int();
#line 103
  __cil_tmp20 = (unsigned long )(& control_block) + 8;
#line 103
  *((unsigned long long *)__cil_tmp20) = (unsigned long long )tmp___0;
#line 103
  tmp___1 = __VERIFIER_nondet_int();
#line 103
  __cil_tmp21 = (unsigned long )(& control_block) + 16;
#line 103
  *((unsigned int *)__cil_tmp21) = (unsigned int )tmp___1;
#line 103
  tmp___2 = __VERIFIER_nondet_int();
#line 103
  __cil_tmp22 = (unsigned long )(& control_block) + 20;
#line 103
  *((unsigned int *)__cil_tmp22) = (unsigned int )tmp___2;
#line 103
  tmp___3 = __VERIFIER_nondet_int();
#line 103
  __cil_tmp23 = 0 * 4UL;
#line 103
  __cil_tmp24 = 24 + __cil_tmp23;
#line 103
  __cil_tmp25 = (unsigned long )(& control_block) + __cil_tmp24;
#line 103
  *((unsigned int *)__cil_tmp25) = (unsigned int )tmp___3;
#line 103
  tmp___4 = __VERIFIER_nondet_int();
#line 103
  __cil_tmp26 = 1 * 4UL;
#line 103
  __cil_tmp27 = 24 + __cil_tmp26;
#line 103
  __cil_tmp28 = (unsigned long )(& control_block) + __cil_tmp27;
#line 103
  *((unsigned int *)__cil_tmp28) = (unsigned int )tmp___4;
#line 106
  __cil_tmp29 = 1 << tag;
#line 106
  __cil_tmp30 = (unsigned int )__cil_tmp29;
#line 106
  mfc_write_tag_mask(__cil_tmp30);
#line 107
  mfc_read_tag_status_all();
#line 111
  __cil_tmp31 = (unsigned long )(& control_block) + 16;
#line 111
  __cil_tmp32 = *((unsigned int *)__cil_tmp31);
#line 111
  __cil_tmp33 = __cil_tmp32 / 4096U;
#line 111
  num_chunks = (int )__cil_tmp33;
#line 118
  i = 0;
  }
  {
#line 118
  while (1) {
    while_continue: /* CIL Label */ ;
#line 118
    if (i < num_chunks) {

    } else {
#line 118
      goto while_break;
    }
    {
#line 121
    __cil_tmp34 = tag == 0U;
#line 121
    assert(__cil_tmp34);
#line 125
    __cil_tmp35 = i * 4096;
#line 125
    __cil_tmp36 = (unsigned long )__cil_tmp35;
#line 125
    __cil_tmp37 = __cil_tmp36 * 4UL;
#line 125
    __cil_tmp38 = (unsigned long long )__cil_tmp37;
#line 125
    __cil_tmp39 = & control_block;
#line 125
    __cil_tmp40 = *((unsigned long long *)__cil_tmp39);
#line 125
    in_addr = __cil_tmp40 + __cil_tmp38;
#line 126
    __cil_tmp41 = i * 4096;
#line 126
    __cil_tmp42 = (unsigned long )__cil_tmp41;
#line 126
    __cil_tmp43 = __cil_tmp42 * 4UL;
#line 126
    __cil_tmp44 = (unsigned long long )__cil_tmp43;
#line 126
    __cil_tmp45 = (unsigned long )(& control_block) + 8;
#line 126
    __cil_tmp46 = *((unsigned long long *)__cil_tmp45);
#line 126
    out_addr = __cil_tmp46 + __cil_tmp44;
#line 129
    __cil_tmp47 = 0 * 4UL;
#line 129
    __cil_tmp48 = (unsigned long )(local_buffer_in) + __cil_tmp47;
#line 129
    __cil_tmp49 = (float *)__cil_tmp48;
#line 129
    __cil_tmp50 = (void volatile   *)__cil_tmp49;
#line 129
    __cil_tmp51 = (unsigned int )in_addr;
#line 129
    __cil_tmp52 = 4096UL * 4UL;
#line 129
    __cil_tmp53 = (unsigned int )__cil_tmp52;
#line 129
    mfc_get(__cil_tmp50, __cil_tmp51, __cil_tmp53, tag, 0U, 0U);
#line 133
    __cil_tmp54 = 1 << 3;
#line 133
    __cil_tmp55 = (unsigned int )__cil_tmp54;
#line 133
    mfc_write_tag_mask(__cil_tmp55);
#line 141
    mfc_read_tag_status_all();
#line 152
    __cil_tmp56 = 0 * 4UL;
#line 152
    __cil_tmp57 = (unsigned long )(local_buffer_out) + __cil_tmp56;
#line 152
    __cil_tmp58 = (float *)__cil_tmp57;
#line 152
    __cil_tmp59 = (void volatile   *)__cil_tmp58;
#line 152
    __cil_tmp60 = (unsigned int )out_addr;
#line 152
    __cil_tmp61 = 4096UL * 4UL;
#line 152
    __cil_tmp62 = (unsigned int )__cil_tmp61;
#line 152
    mfc_put(__cil_tmp59, __cil_tmp60, __cil_tmp62, tag, 0U, 0U);
#line 156
    __cil_tmp63 = 1 << 3;
#line 156
    __cil_tmp64 = (unsigned int )__cil_tmp63;
#line 156
    mfc_write_tag_mask(__cil_tmp64);
#line 164
    mfc_read_tag_status_all();
#line 118
    i = i + 1;
    }
  }
  while_break: /* CIL Label */ ;
  }
#line 172
  return (0);
}
}
