tests/while_break2.scop

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