tests/while_overflow.scop

   1 start: 74
   2 end: 177
   3 indent: "\t"
   4 context: '[N] -> {  : -2147483648 <= N <= 2147483647 }'
   5 schedule: '{ domain: "[N] -> { S_2[t, i] : N <= 1073741823 and t >= 0 and 0 <= i <
   6   2N; S_0[]; S_3[]; S_1[t] : t >= 0 }", child: { sequence: [ { filter: "[N] -> { S_0[]
   7   }" }, { filter: "[N] -> { S_2[t, i]; S_1[t] }", child: { schedule: "[N] -> L_0[{
   8   S_2[t, i] -> [(t)]; S_1[t] -> [(t)] }]", child: { sequence: [ { filter: "[N] ->
   9   { S_1[t] }" }, { filter: "[N] -> { S_2[t, i] }", child: { schedule: "[N] -> L_1[{
  10   S_2[t, i] -> [(i)] }]" } } ] } } }, { filter: "[N] -> { S_3[] }" } ] } }'
  11 arrays:
  12 - context: '{  :  }'
  13   extent: '[N] -> { __pet_test_0[t] : t >= 0 }'
  14   value_bounds: '{ [i0] : 0 <= 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] -> [__pet_test_0 = 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 > 0)] }'
  56     reference: __pet_ref_1
  57     read: 1
  58     write: 0
  59 - line: 14
  60   domain: '[N] -> { [S_2[t, i] -> [__pet_test_0 = 1]] : N <= 1073741823 and t >= 0
  61     and 0 <= i < 2N }'
  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 - line: -1
  90   domain: '[N] -> { S_3[] }'
  91   body:
  92     type: expression
  93     expr:
  94       type: op
  95       operation: kill
  96       arguments:
  97       - type: access
  98         killed: '[N] -> { S_3[] -> s[] }'
  99         index: '[N] -> { S_3[] -> s[] }'
 100         reference: __pet_ref_6
 101         kill: 1
 102 implications:
 103 - satisfied: 1
 104   extension: '{ __pet_test_0[t] -> __pet_test_0[t''] : 0 <= t'' <= t }'