tests/while_overflow.scop

   1 start: 74
   2 end: 177
   3 context: '[N] -> {  : N <= 2147483647 and N >= -2147483648 }'
   4 arrays:
   5 - context: '{  :  }'
   6   extent: '[N] -> { __pet_test_0[t] : t >= 0 }'
   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: '[N] -> { s[] }'
  13   element_type: int
  14   element_size: 4
  15 statements:
  16 - line: 11
  17   domain: '[N] -> { S_0[] }'
  18   schedule: '{ S_0[] -> [0] }'
  19   body:
  20     type: binary
  21     operation: =
  22     arguments:
  23     - type: access
  24       relation: '[N] -> { S_0[] -> s[] }'
  25       read: 0
  26       write: 1
  27     - type: access
  28       relation: '[N] -> { S_0[] -> [0] }'
  29       read: 1
  30       write: 0
  31 - line: 12
  32   domain: '[N] -> { [S_1[t] -> [1]] : t >= 0 }'
  33   schedule: '{ S_1[t] -> [1, t, 0] }'
  34   body:
  35     type: binary
  36     operation: =
  37     arguments:
  38     - type: access
  39       relation: '[N] -> { S_1[t] -> __pet_test_0[t] }'
  40       read: 0
  41       write: 1
  42     - type: call
  43       name: t
  44   arguments:
  45   - type: access
  46     relation: '[N] -> { S_1[t] -> __pet_test_0[o0] : o0 >= 0 and o0 <= -1 + t }'
  47     read: 1
  48     write: 0
  49 - line: 14
  50   domain: '[N] -> { [S_2[t, i] -> [1]] : t >= 0 and i >= 0 and N <= 1073741823 and
  51     i <= -1 + 2N }'
  52   schedule: '[N] -> { S_2[t, i] -> [1, t, 1, 0, i] }'
  53   body:
  54     type: binary
  55     operation: =
  56     arguments:
  57     - type: access
  58       relation: '[N] -> { S_2[t, i] -> s[] }'
  59       read: 0
  60       write: 1
  61     - type: binary
  62       operation: +
  63       arguments:
  64       - type: access
  65         relation: '[N] -> { S_2[t, i] -> s[] }'
  66         read: 1
  67         write: 0
  68       - type: access
  69         relation: '[N] -> { S_2[t, i] -> [1] }'
  70         read: 1
  71         write: 0
  72   arguments:
  73   - type: access
  74     relation: '[N] -> { S_2[t, i] -> __pet_test_0[o0] : o0 >= 0 and o0 <= t }'
  75     read: 1
  76     write: 0