tests/for_while_inc2.scop

   1 start: 83
   2 end: 234
   3 indent: "\t"
   4 context: '[n] -> {  : n <= 2147483647 and n >= -2147483648 }'
   5 arrays:
   6 - context: '{  :  }'
   7   extent: '[n] -> { __pet_test_0[x1, t] : x1 <= -1 + n and x1 >= 0 and 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] -> { x2[] }'
  14   element_type: int
  15   element_size: 4
  16   declared: 1
  17 - context: '{  :  }'
  18   extent: '[n] -> { s[] }'
  19   element_type: int
  20   element_size: 4
  21 statements:
  22 - line: 12
  23   domain: '[n] -> { S1[x1] : x1 <= -1 + n and x1 >= 0 }'
  24   schedule: '[n] -> { S1[x1] -> [0, x1, 0] }'
  25   body:
  26     type: expression
  27     expr:
  28       type: op
  29       operation: =
  30       arguments:
  31       - type: access
  32         index: '[n] -> { S1[x1] -> s[] }'
  33         reference: __pet_ref_0
  34         read: 0
  35         write: 1
  36       - type: call
  37         name: f
  38 - line: 13
  39   domain: '[n] -> { S_5[x1] : x1 <= -1 + n and x1 >= 0 }'
  40   schedule: '[n] -> { S_5[x1] -> [0, x1, 1, 0] }'
  41   body:
  42     type: expression
  43     expr:
  44       type: op
  45       operation: kill
  46       arguments:
  47       - type: access
  48         relation: '[n] -> { S_5[x1] -> x2[] }'
  49         index: '[n] -> { S_5[x1] -> x2[] }'
  50         reference: __pet_ref_1
  51         kill: 1
  52 - line: 13
  53   domain: '[n] -> { S_1[x1] : x1 <= -1 + n and x1 >= 0 }'
  54   schedule: '[n] -> { S_1[x1] -> [0, x1, 1, 1] }'
  55   body:
  56     type: expression
  57     expr:
  58       type: op
  59       operation: =
  60       arguments:
  61       - type: access
  62         index: '[n] -> { S_1[x1] -> x2[] }'
  63         reference: __pet_ref_2
  64         read: 0
  65         write: 1
  66       - type: int
  67         value: 0
  68 - line: 13
  69   domain: '[n] -> { [S_2[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }'
  70   schedule: '[n] -> { S_2[x1, t] -> [0, x1, 1, 2, t, 0] }'
  71   body:
  72     type: expression
  73     expr:
  74       type: op
  75       operation: =
  76       arguments:
  77       - type: access
  78         index: '[n] -> { S_2[x1, t] -> __pet_test_0[(x1), (t)] }'
  79         reference: __pet_ref_4
  80         read: 0
  81         write: 1
  82       - type: call
  83         name: P
  84         arguments:
  85         - type: access
  86           index: '[n] -> { S_2[x1, t] -> [(x1)] }'
  87           reference: __pet_ref_5
  88           read: 1
  89           write: 0
  90         - type: access
  91           index: '[n] -> { S_2[x1, t] -> x2[] }'
  92           reference: __pet_ref_6
  93           read: 1
  94           write: 0
  95   arguments:
  96   - type: access
  97     index: '[n] -> { S_2[x1, t] -> __pet_test_0[(x1), ((-1 + t) : t >= 1)] }'
  98     reference: __pet_ref_3
  99     read: 1
 100     write: 0
 101 - line: 14
 102   domain: '[n] -> { [S2[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }'
 103   schedule: '[n] -> { S2[x1, t] -> [0, x1, 1, 2, t, 1, 0] }'
 104   body:
 105     type: expression
 106     expr:
 107       type: op
 108       operation: =
 109       arguments:
 110       - type: access
 111         index: '[n] -> { S2[x1, t] -> s[] }'
 112         reference: __pet_ref_8
 113         read: 0
 114         write: 1
 115       - type: call
 116         name: g
 117         arguments:
 118         - type: access
 119           index: '[n] -> { S2[x1, t] -> s[] }'
 120           reference: __pet_ref_9
 121           read: 1
 122           write: 0
 123   arguments:
 124   - type: access
 125     index: '[n] -> { S2[x1, t] -> __pet_test_0[(x1), (t)] }'
 126     reference: __pet_ref_7
 127     read: 1
 128     write: 0
 129 - line: 13
 130   domain: '[n] -> { [S_4[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }'
 131   schedule: '[n] -> { S_4[x1, t] -> [0, x1, 1, 2, t, 2] }'
 132   body:
 133     type: expression
 134     expr:
 135       type: op
 136       operation: +=
 137       arguments:
 138       - type: access
 139         index: '[n] -> { S_4[x1, t] -> x2[] }'
 140         reference: __pet_ref_11
 141         read: 0
 142         write: 1
 143       - type: access
 144         index: '[n] -> { S_4[x1, t] -> s[] }'
 145         reference: __pet_ref_12
 146         read: 1
 147         write: 0
 148   arguments:
 149   - type: access
 150     index: '[n] -> { S_4[x1, t] -> __pet_test_0[(x1), (t)] }'
 151     reference: __pet_ref_10
 152     read: 1
 153     write: 0
 154 - line: 13
 155   domain: '[n] -> { S_6[x1] : x1 <= -1 + n and x1 >= 0 }'
 156   schedule: '[n] -> { S_6[x1] -> [0, x1, 1, 3] }'
 157   body:
 158     type: expression
 159     expr:
 160       type: op
 161       operation: kill
 162       arguments:
 163       - type: access
 164         relation: '[n] -> { S_6[x1] -> x2[] }'
 165         index: '[n] -> { S_6[x1] -> x2[] }'
 166         reference: __pet_ref_13
 167         kill: 1
 168 - line: 16
 169   domain: '[n] -> { R[x1] : x1 <= -1 + n and x1 >= 0 }'
 170   schedule: '[n] -> { R[x1] -> [0, x1, 2] }'
 171   body:
 172     type: expression
 173     expr:
 174       type: call
 175       name: h
 176       arguments:
 177       - type: access
 178         index: '[n] -> { R[x1] -> s[] }'
 179         reference: __pet_ref_14
 180         read: 1
 181         write: 0
 182 implications:
 183 - satisfied: 1
 184   extension: '[n] -> { __pet_test_0[x1, t] -> __pet_test_0[x1, t''] : t'' <= t and
 185     x1 >= 0 and x1 <= -1 + n and t'' >= 0 }'