tests/unsigned_break2.scop

   1 context: '{  :  }'
   2 arrays:
   3 - context: '{  :  }'
   4   extent: '{ __pet_test_0[k] : k >= 252 and k <= 261 }'
   5   value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
   6   element_type: int
   7   element_size: 4
   8   uniquely_defined: 1
   9 - context: '{  :  }'
  10   extent: '{ a[] }'
  11   element_type: int
  12   element_size: 4
  13 statements:
  14 - line: 11
  15   domain: '{ [S_0[k] -> [0]] : exists (e0 = [(257 - k)/256]: k >= 252 and k <= 261
  16     and 256e0 <= 255 - k and 256e0 >= 2 - k); [S_0[256] -> [0]] }'
  17   schedule: '{ S_0[k] -> [0, k, 0] }'
  18   body:
  19     type: binary
  20     operation: =
  21     arguments:
  22     - type: access
  23       relation: '{ S_0[k] -> a[] }'
  24       read: 0
  25       write: 1
  26     - type: access
  27       relation: '{ S_0[k] -> [5] }'
  28       read: 1
  29       write: 0
  30   arguments:
  31   - type: access
  32     relation: '{ S_0[k] -> __pet_test_0[o0] : o0 >= 252 and o0 <= -1 + k }'
  33     read: 1
  34     write: 0
  35 - line: 12
  36   domain: '{ [S_1[k] -> [0]] : k >= 252 and k <= 261 }'
  37   schedule: '{ S_1[k] -> [0, k, 1, 0] }'
  38   body:
  39     type: binary
  40     operation: =
  41     arguments:
  42     - type: access
  43       relation: '{ S_1[k] -> __pet_test_0[k] }'
  44       read: 0
  45       write: 1
  46     - type: call
  47       name: f
  48   arguments:
  49   - type: access
  50     relation: '{ S_1[k] -> __pet_test_0[o0] : o0 >= 252 and o0 <= -1 + k }'
  51     read: 1
  52     write: 0
  53 - line: 14
  54   domain: '{ [S_2[k] -> [0]] : k >= 252 and k <= 261 }'
  55   schedule: '{ S_2[k] -> [0, k, 2] }'
  56   body:
  57     type: binary
  58     operation: =
  59     arguments:
  60     - type: access
  61       relation: '{ S_2[k] -> a[] }'
  62       read: 0
  63       write: 1
  64     - type: access
  65       relation: '{ S_2[k] -> [o0] : exists (e0 = [(-k + o0)/256]: 256e0 = -k + o0
  66         and o0 <= 255 and o0 >= 0) }'
  67       read: 1
  68       write: 0
  69   arguments:
  70   - type: access
  71     relation: '{ S_2[k] -> __pet_test_0[o0] : o0 >= 252 and o0 <= -1 + k; S_2[k] ->
  72       __pet_test_0[k] }'
  73     read: 1
  74     write: 0