tests/while_break.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] -> { __pet_test_1[t] : N = 0 and t >= 1; __pet_test_1[0] }'
  11   value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
  12   element_type: int
  13   element_size: 4
  14   uniquely_defined: 1
  15 - context: '{  :  }'
  16   extent: '[N] -> { __pet_test_2[t] : t >= 0 }'
  17   value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
  18   element_type: int
  19   element_size: 4
  20   uniquely_defined: 1
  21 - context: '{  :  }'
  22   extent: '[N] -> { __pet_test_3[t] : t >= 0 }'
  23   value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
  24   element_type: int
  25   element_size: 4
  26   uniquely_defined: 1
  27 - context: '{  :  }'
  28   extent: '[N] -> { a[] }'
  29   element_type: int
  30   element_size: 4
  31 statements:
  32 - line: 10
  33   domain: '[N] -> { S_0[t] : N = 0 and t >= 1; S_0[0] }'
  34   schedule: '{ S_0[t] -> [0, t, 0] }'
  35   body:
  36     type: binary
  37     operation: =
  38     arguments:
  39     - type: access
  40       relation: '[N] -> { S_0[t] -> a[] }'
  41       read: 0
  42       write: 1
  43     - type: access
  44       relation: '[N] -> { S_0[t] -> [5] }'
  45       read: 1
  46       write: 0
  47 - line: 13
  48   domain: '[N] -> { S_1[t] : N = 0 and t >= 1; S_1[0] : N = 0 }'
  49   schedule: '{ S_1[t] -> [0, t, 2] }'
  50   body:
  51     type: binary
  52     operation: =
  53     arguments:
  54     - type: access
  55       relation: '[N] -> { S_1[t] -> a[] }'
  56       read: 0
  57       write: 1
  58     - type: access
  59       relation: '[N] -> { S_1[t] -> [6] }'
  60       read: 1
  61       write: 0
  62 - line: 16
  63   domain: '[N] -> { [S_2[t] -> [0]] : t >= 0 }'
  64   schedule: '{ S_2[t] -> [1, t, 0] }'
  65   body:
  66     type: binary
  67     operation: =
  68     arguments:
  69     - type: access
  70       relation: '[N] -> { S_2[t] -> a[] }'
  71       read: 0
  72       write: 1
  73     - type: access
  74       relation: '[N] -> { S_2[t] -> [5] }'
  75       read: 1
  76       write: 0
  77   arguments:
  78   - type: access
  79     relation: '[N] -> { S_2[t] -> __pet_test_0[o0] : o0 <= -1 + t and o0 >= 0 }'
  80     read: 1
  81     write: 0
  82 - line: 17
  83   domain: '[N] -> { [S_3[t] -> [0]] : t >= 0 }'
  84   schedule: '{ S_3[t] -> [1, t, 1, 0] }'
  85   body:
  86     type: binary
  87     operation: =
  88     arguments:
  89     - type: access
  90       relation: '[N] -> { S_3[t] -> __pet_test_0[t] }'
  91       read: 0
  92       write: 1
  93     - type: call
  94       name: f
  95   arguments:
  96   - type: access
  97     relation: '[N] -> { S_3[t] -> __pet_test_0[o0] : o0 <= -1 + t and o0 >= 0 }'
  98     read: 1
  99     write: 0
 100 - line: 19
 101   domain: '[N] -> { [S_4[t] -> [0]] : t >= 0 }'
 102   schedule: '{ S_4[t] -> [1, t, 2] }'
 103   body:
 104     type: binary
 105     operation: =
 106     arguments:
 107     - type: access
 108       relation: '[N] -> { S_4[t] -> a[] }'
 109       read: 0
 110       write: 1
 111     - type: access
 112       relation: '[N] -> { S_4[t] -> [6] }'
 113       read: 1
 114       write: 0
 115   arguments:
 116   - type: access
 117     relation: '[N] -> { S_4[t] -> __pet_test_0[o0] : o0 <= -1 + t and o0 >= 0; S_4[t]
 118       -> __pet_test_0[t] }'
 119     read: 1
 120     write: 0
 121 - line: 21
 122   domain: '[N] -> { [S_5[t] -> [1]] : N = 0 and t >= 1; [S_5[0] -> [1]] }'
 123   schedule: '{ S_5[t] -> [2, t, 0] }'
 124   body:
 125     type: binary
 126     operation: =
 127     arguments:
 128     - type: access
 129       relation: '[N] -> { S_5[t] -> __pet_test_1[t] }'
 130       read: 0
 131       write: 1
 132     - type: call
 133       name: f
 134   arguments:
 135   - type: access
 136     relation: '[N] -> { S_5[t] -> __pet_test_1[o0] : N = 0 and o0 <= -1 + t and o0
 137       >= 1; S_5[t] -> __pet_test_1[0] : t >= 1 }'
 138     read: 1
 139     write: 0
 140 - line: 22
 141   domain: '[N] -> { [S_6[t] -> [1]] : N = 0 and t >= 1; [S_6[0] -> [1]] }'
 142   schedule: '{ S_6[t] -> [2, t, 1, 0] }'
 143   body:
 144     type: binary
 145     operation: =
 146     arguments:
 147     - type: access
 148       relation: '[N] -> { S_6[t] -> a[] }'
 149       read: 0
 150       write: 1
 151     - type: access
 152       relation: '[N] -> { S_6[t] -> [5] }'
 153       read: 1
 154       write: 0
 155   arguments:
 156   - type: access
 157     relation: '[N] -> { S_6[t] -> __pet_test_1[o0] : N = 0 and o0 <= t and o0 >= 1;
 158       S_6[t] -> __pet_test_1[0] }'
 159     read: 1
 160     write: 0
 161 - line: 25
 162   domain: '[N] -> { [S_7[t] -> [1]] : N = 0 and t >= 1; [S_7[0] -> [1]] : N = 0 }'
 163   schedule: '{ S_7[t] -> [2, t, 1, 2] }'
 164   body:
 165     type: binary
 166     operation: =
 167     arguments:
 168     - type: access
 169       relation: '[N] -> { S_7[t] -> a[] }'
 170       read: 0
 171       write: 1
 172     - type: access
 173       relation: '[N] -> { S_7[t] -> [6] }'
 174       read: 1
 175       write: 0
 176   arguments:
 177   - type: access
 178     relation: '[N] -> { S_7[t] -> __pet_test_1[o0] : o0 <= t and o0 >= 1; S_7[t] ->
 179       __pet_test_1[0] }'
 180     read: 1
 181     write: 0
 182 - line: 27
 183   domain: '[N] -> { [S_8[t] -> [1, 0]] : t >= 0 }'
 184   schedule: '{ S_8[t] -> [3, t, 0] }'
 185   body:
 186     type: binary
 187     operation: =
 188     arguments:
 189     - type: access
 190       relation: '[N] -> { S_8[t] -> __pet_test_2[t] }'
 191       read: 0
 192       write: 1
 193     - type: call
 194       name: f
 195   arguments:
 196   - type: access
 197     relation: '[N] -> { S_8[t] -> __pet_test_2[o0] : o0 <= -1 + t and o0 >= 0 }'
 198     read: 1
 199     write: 0
 200   - type: access
 201     relation: '[N] -> { S_8[t] -> __pet_test_3[o0] : o0 <= -1 + t and o0 >= 0 }'
 202     read: 1
 203     write: 0
 204 - line: 28
 205   domain: '[N] -> { [S_9[t] -> [1, 0]] : t >= 0 }'
 206   schedule: '{ S_9[t] -> [3, t, 1, 0] }'
 207   body:
 208     type: binary
 209     operation: =
 210     arguments:
 211     - type: access
 212       relation: '[N] -> { S_9[t] -> a[] }'
 213       read: 0
 214       write: 1
 215     - type: access
 216       relation: '[N] -> { S_9[t] -> [5] }'
 217       read: 1
 218       write: 0
 219   arguments:
 220   - type: access
 221     relation: '[N] -> { S_9[t] -> __pet_test_2[o0] : o0 <= t and o0 >= 0 }'
 222     read: 1
 223     write: 0
 224   - type: access
 225     relation: '[N] -> { S_9[t] -> __pet_test_3[o0] : o0 <= -1 + t and o0 >= 0 }'
 226     read: 1
 227     write: 0
 228 - line: 29
 229   domain: '[N] -> { [S_10[t] -> [1, 0]] : t >= 0 }'
 230   schedule: '{ S_10[t] -> [3, t, 1, 1, 0] }'
 231   body:
 232     type: binary
 233     operation: =
 234     arguments:
 235     - type: access
 236       relation: '[N] -> { S_10[t] -> __pet_test_3[t] }'
 237       read: 0
 238       write: 1
 239     - type: call
 240       name: f
 241   arguments:
 242   - type: access
 243     relation: '[N] -> { S_10[t] -> __pet_test_2[o0] : o0 <= t and o0 >= 0 }'
 244     read: 1
 245     write: 0
 246   - type: access
 247     relation: '[N] -> { S_10[t] -> __pet_test_3[o0] : o0 <= -1 + t and o0 >= 0 }'
 248     read: 1
 249     write: 0
 250 - line: 31
 251   domain: '[N] -> { [S_11[t] -> [1, 0]] : t >= 0 }'
 252   schedule: '{ S_11[t] -> [3, t, 1, 2] }'
 253   body:
 254     type: binary
 255     operation: =
 256     arguments:
 257     - type: access
 258       relation: '[N] -> { S_11[t] -> a[] }'
 259       read: 0
 260       write: 1
 261     - type: access
 262       relation: '[N] -> { S_11[t] -> [6] }'
 263       read: 1
 264       write: 0
 265   arguments:
 266   - type: access
 267     relation: '[N] -> { S_11[t] -> __pet_test_2[o0] : o0 <= t and o0 >= 0 }'
 268     read: 1
 269     write: 0
 270   - type: access
 271     relation: '[N] -> { S_11[t] -> __pet_test_3[o0] : o0 <= -1 + t and o0 >= 0; S_11[t]
 272       -> __pet_test_3[t] }'
 273     read: 1
 274     write: 0