tests/while.scop

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