tests/while_inc.scop

   1 start: 31
   2 end: 109
   3 context: '{  :  }'
   4 arrays:
   5 - context: '{  :  }'
   6   extent: '{ __pet_test_0[t] : t >= 0 }'
   7   value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
   8   element_type: int
   9   element_size: 4
  10   uniquely_defined: 1
  11 - context: '{  :  }'
  12   extent: '{ T[i0] : i0 >= 0 }'
  13   element_type: int
  14   element_size: 4
  15 - context: '{  :  }'
  16   extent: '{ i[] }'
  17   element_type: int
  18   element_size: 4
  19 statements:
  20 - line: 5
  21   domain: '{ S_0[] }'
  22   schedule: '{ S_0[] -> [0] }'
  23   body:
  24     type: op
  25     operation: =
  26     arguments:
  27     - type: access
  28       relation: '{ S_0[] -> i[] }'
  29       index: '{ S_0[] -> i[] }'
  30       reference: __pet_ref_0
  31       read: 0
  32       write: 1
  33     - type: int
  34       value: 0
  35 - line: 6
  36   domain: '{ [S_1[t] -> [1]] : t >= 0 }'
  37   schedule: '{ S_1[t] -> [1, t, 0] }'
  38   body:
  39     type: op
  40     operation: =
  41     arguments:
  42     - type: access
  43       relation: '{ S_1[t] -> __pet_test_0[t] }'
  44       index: '{ S_1[t] -> __pet_test_0[(t)] }'
  45       reference: __pet_ref_2
  46       read: 0
  47       write: 1
  48     - type: op
  49       operation: <
  50       arguments:
  51       - type: access
  52         relation: '{ S_1[t] -> i[] }'
  53         index: '{ S_1[t] -> i[] }'
  54         reference: __pet_ref_3
  55         read: 1
  56         write: 0
  57       - type: int
  58         value: 100
  59   arguments:
  60   - type: access
  61     relation: '{ S_1[t] -> __pet_test_0[-1 + t] : t >= 1 }'
  62     index: '{ S_1[t] -> __pet_test_0[((-1 + t) : t >= 1)] }'
  63     reference: __pet_ref_1
  64     read: 1
  65     write: 0
  66 - line: 7
  67   domain: '{ [S_2[t] -> [1]] : t >= 0 }'
  68   schedule: '{ S_2[t] -> [1, t, 1, 0] }'
  69   body:
  70     type: op
  71     operation: =
  72     arguments:
  73     - type: access
  74       relation: '{ [S_2[t] -> [i1]] -> T[i1] : i1 >= 0 }'
  75       index: '{ [S_2[t] -> [i1]] -> T[((i1) : i1 >= 0)] }'
  76       reference: __pet_ref_6
  77       read: 0
  78       write: 1
  79       arguments:
  80       - type: access
  81         relation: '{ S_2[t] -> i[] }'
  82         index: '{ S_2[t] -> i[] }'
  83         reference: __pet_ref_5
  84         read: 1
  85         write: 0
  86     - type: access
  87       relation: '{ S_2[t] -> i[] }'
  88       index: '{ S_2[t] -> i[] }'
  89       reference: __pet_ref_7
  90       read: 1
  91       write: 0
  92   arguments:
  93   - type: access
  94     relation: '{ S_2[t] -> __pet_test_0[t] }'
  95     index: '{ S_2[t] -> __pet_test_0[(t)] }'
  96     reference: __pet_ref_4
  97     read: 1
  98     write: 0
  99 - line: 8
 100   domain: '{ [S_3[t] -> [1]] : t >= 0 }'
 101   schedule: '{ S_3[t] -> [1, t, 1, 1] }'
 102   body:
 103     type: op
 104     operation: ++
 105     arguments:
 106     - type: access
 107       relation: '{ S_3[t] -> i[] }'
 108       index: '{ S_3[t] -> i[] }'
 109       reference: __pet_ref_9
 110       read: 1
 111       write: 1
 112   arguments:
 113   - type: access
 114     relation: '{ S_3[t] -> __pet_test_0[t] }'
 115     index: '{ S_3[t] -> __pet_test_0[(t)] }'
 116     reference: __pet_ref_8
 117     read: 1
 118     write: 0
 119 implications:
 120 - satisfied: 1
 121   extension: '{ __pet_test_0[t] -> __pet_test_0[t''] : t'' <= t and t'' >= 0 }'