tests/for_while.scop

   1 start: 83
   2 end: 231
   3 indent: "\t"
   4 context: '[n] -> {  : n <= 2147483647 and n >= -2147483648 }'
   5 schedule: '{ domain: "[n] -> { S2[x1, x2] : x1 >= 0 and x1 <= -1 + n and x2 >= 0;
   6   S_4[]; S1[x1] : x1 >= 0 and x1 <= -1 + n; S_1[x1, x2] : x1 >= 0 and x1 <= -1 + n
   7   and x2 >= 0; R[x1] : x1 >= 0 and x1 <= -1 + n }", child: { sequence: [ { filter:
   8   "[n] -> { S2[x1, x2]; S1[x1]; S_1[x1, x2]; R[x1] }", child: { schedule: "[n] ->
   9   L_0[{ S2[x1, x2] -> [(x1)]; S1[x1] -> [(x1)]; S_1[x1, x2] -> [(x1)]; R[x1] -> [(x1)]
  10   }]", child: { sequence: [ { filter: "[n] -> { S1[x1] }" }, { filter: "[n] -> { S2[x1,
  11   x2]; S_1[x1, x2] }", child: { schedule: "[n] -> L_1[{ S2[x1, x2] -> [(x2)]; S_1[x1,
  12   x2] -> [(x2)] }]", child: { sequence: [ { filter: "[n] -> { S_1[x1, x2] }" }, {
  13   filter: "[n] -> { S2[x1, x2] }" } ] } } }, { filter: "[n] -> { R[x1] }" } ] } }
  14   }, { filter: "[n] -> { S_4[] }" } ] } }'
  15 arrays:
  16 - context: '{  :  }'
  17   extent: '[n] -> { __pet_test_0[x1, x2] : x1 >= 0 and x1 <= -1 + n and x2 >= 0 }'
  18   value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
  19   element_type: int
  20   element_size: 4
  21   uniquely_defined: 1
  22 - context: '{  :  }'
  23   extent: '[n] -> { s[] }'
  24   element_type: int
  25   element_size: 4
  26 statements:
  27 - line: 12
  28   domain: '[n] -> { S1[x1] : x1 >= 0 and x1 <= -1 + n }'
  29   body:
  30     type: expression
  31     expr:
  32       type: op
  33       operation: =
  34       arguments:
  35       - type: access
  36         index: '[n] -> { S1[x1] -> s[] }'
  37         reference: __pet_ref_0
  38         read: 0
  39         write: 1
  40       - type: call
  41         name: f
  42 - line: 13
  43   domain: '[n] -> { [S_1[x1, x2] -> [1]] : x1 >= 0 and x1 <= -1 + n and x2 >= 0 }'
  44   body:
  45     type: expression
  46     expr:
  47       type: op
  48       operation: =
  49       arguments:
  50       - type: access
  51         index: '[n] -> { S_1[x1, x2] -> __pet_test_0[(x1), (x2)] }'
  52         reference: __pet_ref_2
  53         read: 0
  54         write: 1
  55       - type: call
  56         name: P
  57         arguments:
  58         - type: access
  59           index: '[n] -> { S_1[x1, x2] -> [(x1)] }'
  60           reference: __pet_ref_3
  61           read: 1
  62           write: 0
  63         - type: access
  64           index: '[n] -> { S_1[x1, x2] -> [(x2)] }'
  65           reference: __pet_ref_4
  66           read: 1
  67           write: 0
  68   arguments:
  69   - type: access
  70     index: '[n] -> { S_1[x1, x2] -> __pet_test_0[(x1), ((-1 + x2) : x2 >= 1)] }'
  71     reference: __pet_ref_1
  72     read: 1
  73     write: 0
  74 - line: 14
  75   domain: '[n] -> { [S2[x1, x2] -> [1]] : x1 >= 0 and x1 <= -1 + n and x2 >= 0 }'
  76   body:
  77     type: expression
  78     expr:
  79       type: op
  80       operation: =
  81       arguments:
  82       - type: access
  83         index: '[n] -> { S2[x1, x2] -> s[] }'
  84         reference: __pet_ref_6
  85         read: 0
  86         write: 1
  87       - type: call
  88         name: g
  89         arguments:
  90         - type: access
  91           index: '[n] -> { S2[x1, x2] -> s[] }'
  92           reference: __pet_ref_7
  93           read: 1
  94           write: 0
  95   arguments:
  96   - type: access
  97     index: '[n] -> { S2[x1, x2] -> __pet_test_0[(x1), (x2)] }'
  98     reference: __pet_ref_5
  99     read: 1
 100     write: 0
 101 - line: 16
 102   domain: '[n] -> { R[x1] : x1 >= 0 and x1 <= -1 + n }'
 103   body:
 104     type: expression
 105     expr:
 106       type: call
 107       name: h
 108       arguments:
 109       - type: access
 110         index: '[n] -> { R[x1] -> s[] }'
 111         reference: __pet_ref_8
 112         read: 1
 113         write: 0
 114 - line: -1
 115   domain: '[n] -> { S_4[] }'
 116   body:
 117     type: expression
 118     expr:
 119       type: op
 120       operation: kill
 121       arguments:
 122       - type: access
 123         killed: '[n] -> { S_4[] -> s[] }'
 124         index: '[n] -> { S_4[] -> s[] }'
 125         reference: __pet_ref_9
 126         kill: 1
 127 implications:
 128 - satisfied: 1
 129   extension: '[n] -> { __pet_test_0[x1, x2] -> __pet_test_0[x1, x2''] : x2'' <= x2
 130     and x1 >= 0 and x1 <= -1 + n and x2'' >= 0 }'