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