tests/unsigned_break2.scop

   1 start: 50
   2 end: 172
   3 context: '{  :  }'
   4 arrays:
   5 - context: '{  :  }'
   6   extent: '{ __pet_test_0[k] : k >= 252 and k <= 261 }'
   7   value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
   8   element_type: int
   9   element_size: 4
  10   uniquely_defined: 1
  11 - context: '{  :  }'
  12   extent: '{ a[] }'
  13   element_type: int
  14   element_size: 4
  15 statements:
  16 - line: 11
  17   domain: '{ [S_0[k] -> [0]] : (exists (e0 = floor((k)/256): 256e0 = k and k >= 252
  18     and k <= 261)) or (exists (e0 = floor((257 - k)/256): k >= 252 and k <= 261 and
  19     256e0 >= 2 - k and 256e0 <= 255 - k)) }'
  20   schedule: '{ S_0[k] -> [0, k, 0] }'
  21   body:
  22     type: binary
  23     operation: =
  24     arguments:
  25     - type: access
  26       relation: '{ S_0[k] -> a[] }'
  27       index: '{ S_0[k] -> a[] }'
  28       reference: __pet_ref_1
  29       read: 0
  30       write: 1
  31     - type: access
  32       relation: '{ S_0[k] -> [5] }'
  33       index: '{ S_0[k] -> [(5)] }'
  34       reference: __pet_ref_2
  35       read: 1
  36       write: 0
  37   arguments:
  38   - type: access
  39     relation: '{ S_0[k] -> __pet_test_0[-1 + k] : k >= 253 }'
  40     index: '{ S_0[k] -> __pet_test_0[((-1 + k) : k >= 253)] }'
  41     reference: __pet_ref_0
  42     read: 1
  43     write: 0
  44 - line: 12
  45   domain: '{ [S_1[k] -> [0]] : k >= 252 and k <= 261 }'
  46   schedule: '{ S_1[k] -> [0, k, 1, 0] }'
  47   body:
  48     type: binary
  49     operation: =
  50     arguments:
  51     - type: access
  52       relation: '{ S_1[k] -> __pet_test_0[k] }'
  53       index: '{ S_1[k] -> __pet_test_0[(k)] }'
  54       reference: __pet_ref_4
  55       read: 0
  56       write: 1
  57     - type: call
  58       name: f
  59   arguments:
  60   - type: access
  61     relation: '{ S_1[k] -> __pet_test_0[-1 + k] : k >= 253 }'
  62     index: '{ S_1[k] -> __pet_test_0[((-1 + k) : k >= 253)] }'
  63     reference: __pet_ref_3
  64     read: 1
  65     write: 0
  66 - line: 14
  67   domain: '{ [S_2[k] -> [0]] : k >= 252 and k <= 261 }'
  68   schedule: '{ S_2[k] -> [0, k, 2] }'
  69   body:
  70     type: binary
  71     operation: =
  72     arguments:
  73     - type: access
  74       relation: '{ S_2[k] -> a[] }'
  75       index: '{ S_2[k] -> a[] }'
  76       reference: __pet_ref_6
  77       read: 0
  78       write: 1
  79     - type: access
  80       relation: '{ S_2[k] -> [o0] : exists (e0 = floor((-k + o0)/256): 256e0 = -k
  81         + o0 and o0 >= 0 and o0 <= 255) }'
  82       index: '{ S_2[k] -> [(k - 256*floor((k)/256))] }'
  83       reference: __pet_ref_7
  84       read: 1
  85       write: 0
  86   arguments:
  87   - type: access
  88     relation: '{ S_2[k] -> __pet_test_0[k] }'
  89     index: '{ S_2[k] -> __pet_test_0[(k)] }'
  90     reference: __pet_ref_5
  91     read: 1
  92     write: 0
  93 implications:
  94 - satisfied: 0
  95   extension: '{ __pet_test_0[k] -> __pet_test_0[k''] : k'' <= k and k'' >= 252 and
  96     k'' <= 261 }'