tests/while_inc.scop

   1 context: '{  :  }'
   2 arrays:
   3 - context: '{  :  }'
   4   extent: '{ __pet_test_0[t] : t >= 0 }'
   5   value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
   6   element_type: int
   7   element_size: 4
   8   uniquely_defined: 1
   9 - context: '{  :  }'
  10   extent: '{ T[i0] : i0 >= 0 }'
  11   element_type: int
  12   element_size: 4
  13 - context: '{  :  }'
  14   extent: '{ i[] }'
  15   element_type: int
  16   element_size: 4
  17 statements:
  18 - line: 5
  19   domain: '{ S_0[] }'
  20   schedule: '{ S_0[] -> [0] }'
  21   body:
  22     type: binary
  23     operation: =
  24     arguments:
  25     - type: access
  26       relation: '{ S_0[] -> i[] }'
  27       read: 0
  28       write: 1
  29     - type: access
  30       relation: '{ S_0[] -> [0] }'
  31       read: 1
  32       write: 0
  33 - line: 6
  34   domain: '{ [S_1[t] -> [1]] : t >= 0 }'
  35   schedule: '{ S_1[t] -> [1, t, 0] }'
  36   body:
  37     type: binary
  38     operation: =
  39     arguments:
  40     - type: access
  41       relation: '{ S_1[t] -> __pet_test_0[t] }'
  42       read: 0
  43       write: 1
  44     - type: binary
  45       operation: <
  46       arguments:
  47       - type: access
  48         relation: '{ S_1[t] -> i[] }'
  49         read: 1
  50         write: 0
  51       - type: access
  52         relation: '{ S_1[t] -> [100] }'
  53         read: 1
  54         write: 0
  55   arguments:
  56   - type: access
  57     relation: '{ S_1[t] -> __pet_test_0[o0] : o0 <= -1 + t and o0 >= 0 }'
  58     read: 1
  59     write: 0
  60 - line: 7
  61   domain: '{ [S_2[t] -> [1]] : t >= 0 }'
  62   schedule: '{ S_2[t] -> [1, t, 1, 0] }'
  63   body:
  64     type: binary
  65     operation: =
  66     arguments:
  67     - type: access
  68       relation: '{ [S_2[t] -> [i1]] -> T[i1] : i1 >= 0 }'
  69       read: 0
  70       write: 1
  71       arguments:
  72       - type: access
  73         relation: '{ S_2[t] -> i[] }'
  74         read: 1
  75         write: 0
  76     - type: access
  77       relation: '{ S_2[t] -> i[] }'
  78       read: 1
  79       write: 0
  80   arguments:
  81   - type: access
  82     relation: '{ S_2[t] -> __pet_test_0[o0] : o0 <= t and o0 >= 0 }'
  83     read: 1
  84     write: 0
  85 - line: 8
  86   domain: '{ [S_3[t] -> [1]] : t >= 0 }'
  87   schedule: '{ S_3[t] -> [1, t, 1, 1] }'
  88   body:
  89     type: unary
  90     operation: ++
  91     arguments:
  92     - type: access
  93       relation: '{ S_3[t] -> i[] }'
  94       read: 1
  95       write: 1
  96   arguments:
  97   - type: access
  98     relation: '{ S_3[t] -> __pet_test_0[o0] : o0 <= t and o0 >= 0 }'
  99     read: 1
 100     write: 0