tests/while_overflow.scop

   1 start: 74
   2 end: 177
   3 indent: "\t"
   4 context: '[N] -> {  : N <= 2147483647 and N >= -2147483648 }'
   5 schedule: '{ domain: "[N] -> { S_2[t, i] : N <= 1073741823 and t >= 0 and i >= 0 and
   6   i <= -1 + 2N; S_0[]; S_3[]; S_1[t] : t >= 0 }", child: { sequence: [ { filter: "[N]
   7   -> { S_0[] }" }, { filter: "[N] -> { S_2[t, i]; S_1[t] }", child: { schedule: "[N]
   8   -> L_0[{ S_2[t, i] -> [(t)]; S_1[t] -> [(t)] }]", child: { sequence: [ { filter:
   9   "[N] -> { S_1[t] }" }, { filter: "[N] -> { S_2[t, i] }", child: { schedule: "[N]
  10   -> L_1[{ S_2[t, i] -> [(i)] }]" } } ] } } }, { filter: "[N] -> { S_3[] }" } ] }
  11   }'
  12 arrays:
  13 - context: '{  :  }'
  14   extent: '[N] -> { __pet_test_0[t] : t >= 0 }'
  15   value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
  16   element_type: int
  17   element_size: 4
  18   uniquely_defined: 1
  19 - context: '{  :  }'
  20   extent: '[N] -> { s[] }'
  21   element_type: int
  22   element_size: 4
  23 statements:
  24 - line: 11
  25   domain: '[N] -> { S_0[] }'
  26   body:
  27     type: expression
  28     expr:
  29       type: op
  30       operation: =
  31       arguments:
  32       - type: access
  33         index: '[N] -> { S_0[] -> s[] }'
  34         reference: __pet_ref_0
  35         read: 0
  36         write: 1
  37       - type: int
  38         value: 0
  39 - line: 12
  40   domain: '[N] -> { [S_1[t] -> [1]] : t >= 0 }'
  41   body:
  42     type: expression
  43     expr:
  44       type: op
  45       operation: =
  46       arguments:
  47       - type: access
  48         index: '[N] -> { S_1[t] -> __pet_test_0[(t)] }'
  49         reference: __pet_ref_2
  50         read: 0
  51         write: 1
  52       - type: call
  53         name: t
  54   arguments:
  55   - type: access
  56     index: '[N] -> { S_1[t] -> __pet_test_0[((-1 + t) : t >= 1)] }'
  57     reference: __pet_ref_1
  58     read: 1
  59     write: 0
  60 - line: 14
  61   domain: '[N] -> { [S_2[t, i] -> [1]] : N <= 1073741823 and t >= 0 and i >= 0 and
  62     i <= -1 + 2N }'
  63   body:
  64     type: expression
  65     expr:
  66       type: op
  67       operation: =
  68       arguments:
  69       - type: access
  70         index: '[N] -> { S_2[t, i] -> s[] }'
  71         reference: __pet_ref_4
  72         read: 0
  73         write: 1
  74       - type: op
  75         operation: +
  76         arguments:
  77         - type: access
  78           index: '[N] -> { S_2[t, i] -> s[] }'
  79           reference: __pet_ref_5
  80           read: 1
  81           write: 0
  82         - type: int
  83           value: 1
  84   arguments:
  85   - type: access
  86     index: '[N] -> { S_2[t, i] -> __pet_test_0[(t)] }'
  87     reference: __pet_ref_3
  88     read: 1
  89     write: 0
  90 - line: -1
  91   domain: '[N] -> { S_3[] }'
  92   body:
  93     type: expression
  94     expr:
  95       type: op
  96       operation: kill
  97       arguments:
  98       - type: access
  99         killed: '[N] -> { S_3[] -> s[] }'
 100         index: '[N] -> { S_3[] -> s[] }'
 101         reference: __pet_ref_6
 102         kill: 1
 103 implications:
 104 - satisfied: 1
 105   extension: '{ __pet_test_0[t] -> __pet_test_0[t''] : t'' <= t and t'' >= 0 }'