tests/while_break2.scop

   1 start: 45
   2 end: 157
   3 context: '[N] -> {  : N <= 2147483647 and N >= -2147483648 }'
   4 arrays:
   5 - context: '{  :  }'
   6   extent: '[N] -> { __pet_test_0[i, t] : N = 0 and i <= 9 and i >= 1 and t >= 0; __pet_test_0[0,
   7     t] : t >= 0 }'
   8   value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
   9   element_type: int
  10   element_size: 4
  11   uniquely_defined: 1
  12 - context: '{  :  }'
  13   extent: '[N] -> { a[] }'
  14   element_type: int
  15   element_size: 4
  16 statements:
  17 - line: 10
  18   domain: '[N] -> { [S_0[i, t] -> [1]] : N = 0 and i <= 9 and i >= 1 and t >= 0; [S_0[0,
  19     t] -> [1]] : t >= 0 }'
  20   schedule: '[N] -> { S_0[i, t] -> [0, i, 0, t, 0] }'
  21   body:
  22     type: op
  23     operation: =
  24     arguments:
  25     - type: access
  26       relation: '[N] -> { S_0[i, t] -> __pet_test_0[i, t] }'
  27       index: '[N] -> { S_0[i, t] -> __pet_test_0[(i), (t)] }'
  28       reference: __pet_ref_1
  29       read: 0
  30       write: 1
  31     - type: call
  32       name: f
  33   arguments:
  34   - type: access
  35     relation: '[N] -> { S_0[i, t] -> __pet_test_0[i, -1 + t] : t >= 1 }'
  36     index: '[N] -> { S_0[i, t] -> __pet_test_0[(i), ((-1 + t) : t >= 1)] }'
  37     reference: __pet_ref_0
  38     read: 1
  39     write: 0
  40 - line: 11
  41   domain: '[N] -> { [S_1[i, t] -> [1]] : N = 0 and i <= 9 and i >= 1 and t >= 0; [S_1[0,
  42     t] -> [1]] : t >= 0 }'
  43   schedule: '[N] -> { S_1[i, t] -> [0, i, 0, t, 1] }'
  44   body:
  45     type: op
  46     operation: =
  47     arguments:
  48     - type: access
  49       relation: '[N] -> { S_1[i, t] -> a[] }'
  50       index: '[N] -> { S_1[i, t] -> a[] }'
  51       reference: __pet_ref_3
  52       read: 0
  53       write: 1
  54     - type: int
  55       value: 5
  56   arguments:
  57   - type: access
  58     relation: '[N] -> { S_1[i, t] -> __pet_test_0[i, t] }'
  59     index: '[N] -> { S_1[i, t] -> __pet_test_0[(i), (t)] }'
  60     reference: __pet_ref_2
  61     read: 1
  62     write: 0
  63 - line: 14
  64   domain: '[N] -> { S_2[i] : N = 0 and i <= 9 and i >= 1; S_2[0] : N = 0 }'
  65   schedule: '[N] -> { S_2[i] -> [0, i, 2] }'
  66   body:
  67     type: op
  68     operation: =
  69     arguments:
  70     - type: access
  71       relation: '[N] -> { S_2[i] -> a[] }'
  72       index: '[N] -> { S_2[i] -> a[] }'
  73       reference: __pet_ref_4
  74       read: 0
  75       write: 1
  76     - type: int
  77       value: 6
  78 implications:
  79 - satisfied: 1
  80   extension: '[N] -> { __pet_test_0[i, t] -> __pet_test_0[i, t''] : N = 0 and i >=
  81     1 and i <= 9 and t'' <= t and t'' >= 0; __pet_test_0[0, t] -> __pet_test_0[0,
  82     t''] : t'' <= t and t'' >= 0 }'