tests/while_overflow.scop

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