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: expression
  24     expr:
  25       type: op
  26       operation: =
  27       arguments:
  28       - type: access
  29         relation: '[N] -> { S_0[i, t] -> __pet_test_0[i, t] }'
  30         index: '[N] -> { S_0[i, t] -> __pet_test_0[(i), (t)] }'
  31         reference: __pet_ref_1
  32         read: 0
  33         write: 1
  34       - type: call
  35         name: f
  36   arguments:
  37   - type: access
  38     relation: '[N] -> { S_0[i, t] -> __pet_test_0[i, -1 + t] : t >= 1 }'
  39     index: '[N] -> { S_0[i, t] -> __pet_test_0[(i), ((-1 + t) : t >= 1)] }'
  40     reference: __pet_ref_0
  41     read: 1
  42     write: 0
  43 - line: 11
  44   domain: '[N] -> { [S_1[i, t] -> [1]] : N = 0 and i <= 9 and i >= 1 and t >= 0; [S_1[0,
  45     t] -> [1]] : t >= 0 }'
  46   schedule: '{ S_1[i, t] -> [0, i, 0, t, 1] }'
  47   body:
  48     type: expression
  49     expr:
  50       type: op
  51       operation: =
  52       arguments:
  53       - type: access
  54         relation: '[N] -> { S_1[i, t] -> a[] }'
  55         index: '[N] -> { S_1[i, t] -> a[] }'
  56         reference: __pet_ref_3
  57         read: 0
  58         write: 1
  59       - type: int
  60         value: 5
  61   arguments:
  62   - type: access
  63     relation: '[N] -> { S_1[i, t] -> __pet_test_0[i, t] }'
  64     index: '[N] -> { S_1[i, t] -> __pet_test_0[(i), (t)] }'
  65     reference: __pet_ref_2
  66     read: 1
  67     write: 0
  68 - line: 14
  69   domain: '[N] -> { S_2[i] : N = 0 and i <= 9 and i >= 1; S_2[0] : N = 0 }'
  70   schedule: '[N] -> { S_2[i] -> [0, i, 2] }'
  71   body:
  72     type: expression
  73     expr:
  74       type: op
  75       operation: =
  76       arguments:
  77       - type: access
  78         relation: '[N] -> { S_2[i] -> a[] }'
  79         index: '[N] -> { S_2[i] -> a[] }'
  80         reference: __pet_ref_4
  81         read: 0
  82         write: 1
  83       - type: int
  84         value: 6
  85 implications:
  86 - satisfied: 1
  87   extension: '[N] -> { __pet_test_0[i, t] -> __pet_test_0[i, t''] : N = 0 and t''
  88     <= t and i >= 1 and i <= 9 and t'' >= 0; __pet_test_0[0, t] -> __pet_test_0[0,
  89     t''] : t'' <= t and t'' >= 0 }'