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: binary
  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: access
  34       relation: '{ S_0[] -> [0] }'
  35       index: '{ S_0[] -> [(0)] }'
  36       reference: __pet_ref_1
  37       read: 1
  38       write: 0
  39 - line: 6
  40   domain: '{ [S_1[t] -> [1]] : t >= 0 }'
  41   schedule: '{ S_1[t] -> [1, t, 0] }'
  42   body:
  43     type: binary
  44     operation: =
  45     arguments:
  46     - type: access
  47       relation: '{ S_1[t] -> __pet_test_0[t] }'
  48       index: '{ S_1[t] -> __pet_test_0[(t)] }'
  49       reference: __pet_ref_3
  50       read: 0
  51       write: 1
  52     - type: binary
  53       operation: <
  54       arguments:
  55       - type: access
  56         relation: '{ S_1[t] -> i[] }'
  57         index: '{ S_1[t] -> i[] }'
  58         reference: __pet_ref_4
  59         read: 1
  60         write: 0
  61       - type: access
  62         relation: '{ S_1[t] -> [100] }'
  63         index: '{ S_1[t] -> [(100)] }'
  64         reference: __pet_ref_5
  65         read: 1
  66         write: 0
  67   arguments:
  68   - type: access
  69     relation: '{ S_1[t] -> __pet_test_0[-1 + t] : t >= 1 }'
  70     index: '{ S_1[t] -> __pet_test_0[((-1 + t) : t >= 1)] }'
  71     reference: __pet_ref_2
  72     read: 1
  73     write: 0
  74 - line: 7
  75   domain: '{ [S_2[t] -> [1]] : t >= 0 }'
  76   schedule: '{ S_2[t] -> [1, t, 1, 0] }'
  77   body:
  78     type: binary
  79     operation: =
  80     arguments:
  81     - type: access
  82       relation: '{ [S_2[t] -> [i1]] -> T[i1] : i1 >= 0 }'
  83       index: '{ [S_2[t] -> [i1]] -> T[((i1) : i1 >= 0)] }'
  84       reference: __pet_ref_8
  85       read: 0
  86       write: 1
  87       arguments:
  88       - type: access
  89         relation: '{ S_2[t] -> i[] }'
  90         index: '{ S_2[t] -> i[] }'
  91         reference: __pet_ref_7
  92         read: 1
  93         write: 0
  94     - type: access
  95       relation: '{ S_2[t] -> i[] }'
  96       index: '{ S_2[t] -> i[] }'
  97       reference: __pet_ref_9
  98       read: 1
  99       write: 0
 100   arguments:
 101   - type: access
 102     relation: '{ S_2[t] -> __pet_test_0[t] }'
 103     index: '{ S_2[t] -> __pet_test_0[(t)] }'
 104     reference: __pet_ref_6
 105     read: 1
 106     write: 0
 107 - line: 8
 108   domain: '{ [S_3[t] -> [1]] : t >= 0 }'
 109   schedule: '{ S_3[t] -> [1, t, 1, 1] }'
 110   body:
 111     type: unary
 112     operation: ++
 113     arguments:
 114     - type: access
 115       relation: '{ S_3[t] -> i[] }'
 116       index: '{ S_3[t] -> i[] }'
 117       reference: __pet_ref_11
 118       read: 1
 119       write: 1
 120   arguments:
 121   - type: access
 122     relation: '{ S_3[t] -> __pet_test_0[t] }'
 123     index: '{ S_3[t] -> __pet_test_0[(t)] }'
 124     reference: __pet_ref_10
 125     read: 1
 126     write: 0
 127 implications:
 128 - satisfied: 1
 129   extension: '{ __pet_test_0[t] -> __pet_test_0[t''] : t'' <= t and t'' >= 0 }'