tests/while_overflow.scop

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