tests/while_overflow.scop

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