tests/for_while_overflow.scop

   1 start: 74
   2 end: 191
   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: op
  22     operation: =
  23     arguments:
  24     - type: access
  25       relation: '[N] -> { S_0[] -> s[] }'
  26       index: '[N] -> { S_0[] -> s[] }'
  27       reference: __pet_ref_0
  28       read: 0
  29       write: 1
  30     - type: int
  31       value: 0
  32 - line: 12
  33   domain: '[N] -> { [S_1[T] -> [1]] : T >= 0 }'
  34   schedule: '{ S_1[T] -> [1, T, 0] }'
  35   body:
  36     type: op
  37     operation: =
  38     arguments:
  39     - type: access
  40       relation: '[N] -> { S_1[T] -> __pet_test_0[T] }'
  41       index: '[N] -> { S_1[T] -> __pet_test_0[(T)] }'
  42       reference: __pet_ref_2
  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     index: '[N] -> { S_1[T] -> __pet_test_0[((-1 + T) : T >= 1)] }'
  51     reference: __pet_ref_1
  52     read: 1
  53     write: 0
  54 - line: 14
  55   domain: '[N] -> { [S_2[T, i] -> [1]] : T >= 0 and i >= 0 and N <= 1073741823 and
  56     i <= -1 + 2N }'
  57   schedule: '[N] -> { S_2[T, i] -> [1, T, 1, 0, i] }'
  58   body:
  59     type: op
  60     operation: =
  61     arguments:
  62     - type: access
  63       relation: '[N] -> { S_2[T, i] -> s[] }'
  64       index: '[N] -> { S_2[T, i] -> s[] }'
  65       reference: __pet_ref_4
  66       read: 0
  67       write: 1
  68     - type: op
  69       operation: +
  70       arguments:
  71       - type: access
  72         relation: '[N] -> { S_2[T, i] -> s[] }'
  73         index: '[N] -> { S_2[T, i] -> s[] }'
  74         reference: __pet_ref_5
  75         read: 1
  76         write: 0
  77       - type: int
  78         value: 1
  79   arguments:
  80   - type: access
  81     relation: '[N] -> { S_2[T, i] -> __pet_test_0[T] }'
  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 }'