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_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)] }]" } } ] } } } ] } }'
  11 arrays:
  12 - context: '{  :  }'
  13   extent: '[N] -> { __pet_test_0[t] : t >= 0 }'
  14   value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
  15   element_type: int
  16   element_size: 4
  17   uniquely_defined: 1
  18 - context: '{  :  }'
  19   extent: '[N] -> { s[] }'
  20   element_type: int
  21   element_size: 4
  22 statements:
  23 - line: 11
  24   domain: '[N] -> { S_0[] }'
  25   body:
  26     type: expression
  27     expr:
  28       type: op
  29       operation: =
  30       arguments:
  31       - type: access
  32         index: '[N] -> { S_0[] -> s[] }'
  33         reference: __pet_ref_0
  34         read: 0
  35         write: 1
  36       - type: int
  37         value: 0
  38 - line: 12
  39   domain: '[N] -> { [S_1[t] -> [1]] : t >= 0 }'
  40   body:
  41     type: expression
  42     expr:
  43       type: op
  44       operation: =
  45       arguments:
  46       - type: access
  47         index: '[N] -> { S_1[t] -> __pet_test_0[(t)] }'
  48         reference: __pet_ref_2
  49         read: 0
  50         write: 1
  51       - type: call
  52         name: t
  53   arguments:
  54   - type: access
  55     index: '[N] -> { S_1[t] -> __pet_test_0[((-1 + t) : t >= 1)] }'
  56     reference: __pet_ref_1
  57     read: 1
  58     write: 0
  59 - line: 14
  60   domain: '[N] -> { [S_2[t, i] -> [1]] : i >= 0 and i <= -1 + 2N and N <= 1073741823
  61     and t >= 0 }'
  62   body:
  63     type: expression
  64     expr:
  65       type: op
  66       operation: =
  67       arguments:
  68       - type: access
  69         index: '[N] -> { S_2[t, i] -> s[] }'
  70         reference: __pet_ref_4
  71         read: 0
  72         write: 1
  73       - type: op
  74         operation: +
  75         arguments:
  76         - type: access
  77           index: '[N] -> { S_2[t, i] -> s[] }'
  78           reference: __pet_ref_5
  79           read: 1
  80           write: 0
  81         - type: int
  82           value: 1
  83   arguments:
  84   - type: access
  85     index: '[N] -> { S_2[t, i] -> __pet_test_0[(t)] }'
  86     reference: __pet_ref_3
  87     read: 1
  88     write: 0
  89 implications:
  90 - satisfied: 1
  91   extension: '{ __pet_test_0[t] -> __pet_test_0[t''] : t'' <= t and t'' >= 0 }'