tests/for_while_overflow.scop

   1 start: 74
   2 end: 191
   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       index: '[N] -> { S_0[] -> s[] }'
  26       reference: __pet_ref_0
  27       read: 0
  28       write: 1
  29     - type: access
  30       relation: '[N] -> { S_0[] -> [0] }'
  31       index: '[N] -> { S_0[] -> [(0)] }'
  32       reference: __pet_ref_1
  33       read: 1
  34       write: 0
  35 - line: 12
  36   domain: '[N] -> { [S_1[T] -> [1]] : T >= 0 }'
  37   schedule: '{ S_1[T] -> [1, T, 0] }'
  38   body:
  39     type: binary
  40     operation: =
  41     arguments:
  42     - type: access
  43       relation: '[N] -> { S_1[T] -> __pet_test_0[T] }'
  44       index: '[N] -> { S_1[T] -> __pet_test_0[(T)] }'
  45       reference: __pet_ref_3
  46       read: 0
  47       write: 1
  48     - type: call
  49       name: t
  50   arguments:
  51   - type: access
  52     relation: '[N] -> { S_1[T] -> __pet_test_0[-1 + T] : T >= 1 }'
  53     index: '[N] -> { S_1[T] -> __pet_test_0[((-1 + T) : T >= 1)] }'
  54     reference: __pet_ref_2
  55     read: 1
  56     write: 0
  57 - line: 14
  58   domain: '[N] -> { [S_2[T, i] -> [1]] : T >= 0 and i >= 0 and N <= 1073741823 and
  59     i <= -1 + 2N }'
  60   schedule: '[N] -> { S_2[T, i] -> [1, T, 1, 0, i] }'
  61   body:
  62     type: binary
  63     operation: =
  64     arguments:
  65     - type: access
  66       relation: '[N] -> { S_2[T, i] -> s[] }'
  67       index: '[N] -> { S_2[T, i] -> s[] }'
  68       reference: __pet_ref_5
  69       read: 0
  70       write: 1
  71     - type: binary
  72       operation: +
  73       arguments:
  74       - type: access
  75         relation: '[N] -> { S_2[T, i] -> s[] }'
  76         index: '[N] -> { S_2[T, i] -> s[] }'
  77         reference: __pet_ref_6
  78         read: 1
  79         write: 0
  80       - type: access
  81         relation: '[N] -> { S_2[T, i] -> [1] }'
  82         index: '[N] -> { S_2[T, i] -> [(1)] }'
  83         reference: __pet_ref_7
  84         read: 1
  85         write: 0
  86   arguments:
  87   - type: access
  88     relation: '[N] -> { S_2[T, i] -> __pet_test_0[T] }'
  89     index: '[N] -> { S_2[T, i] -> __pet_test_0[(T)] }'
  90     reference: __pet_ref_4
  91     read: 1
  92     write: 0
  93 implications:
  94 - satisfied: 1
  95   extension: '{ __pet_test_0[T] -> __pet_test_0[T''] : T'' <= T and T'' >= 0 }'