tests/for_while_unsigned2.scop

   1 start: 100
   2 end: 316
   3 context: '[n] -> {  : n <= 2147483647 and n >= -2147483648 }'
   4 arrays:
   5 - context: '{  :  }'
   6   extent: '[n] -> { __pet_test_0[x1, x2] : exists (e0 = floor((x2)/3): 3e0 = x2 and
   7     x1 <= -1 + n and x1 >= 0 and x2 <= 9) }'
   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] -> { a[i0, i1] : i0 >= 0 and i1 <= 255 and i1 >= 0 }'
  14   element_type: int
  15   element_size: 4
  16 - context: '{  :  }'
  17   extent: '[n] -> { s[] }'
  18   element_type: int
  19   element_size: 4
  20 statements:
  21 - line: 12
  22   domain: '[n] -> { S1[x1] : x1 <= -1 + n and x1 >= 0 }'
  23   schedule: '[n] -> { S1[x1] -> [0, x1, 0] }'
  24   body:
  25     type: binary
  26     operation: =
  27     arguments:
  28     - type: access
  29       relation: '[n] -> { S1[x1] -> s[] }'
  30       index: '[n] -> { S1[x1] -> s[] }'
  31       reference: __pet_ref_0
  32       read: 0
  33       write: 1
  34     - type: call
  35       name: f
  36 - line: 13
  37   domain: '[n] -> { [S_1[x1, x2] -> [1]] : exists (e0 = floor((x2)/3): 3e0 = x2 and
  38     x1 <= -1 + n and x1 >= 0 and x2 <= 9) }'
  39   schedule: '[n] -> { S_1[x1, x2] -> [0, x1, 1, -x2, 0] }'
  40   body:
  41     type: binary
  42     operation: =
  43     arguments:
  44     - type: access
  45       relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, x2] }'
  46       index: '[n] -> { S_1[x1, x2] -> __pet_test_0[(x1), (x2)] }'
  47       reference: __pet_ref_2
  48       read: 0
  49       write: 1
  50     - type: call
  51       name: P
  52       arguments:
  53       - type: access
  54         relation: '[n] -> { S_1[x1, x2] -> [x1] }'
  55         index: '[n] -> { S_1[x1, x2] -> [(x1)] }'
  56         reference: __pet_ref_3
  57         read: 1
  58         write: 0
  59       - type: access
  60         relation: '[n] -> { S_1[x1, x2] -> [o0] : exists (e0 = floor((-x2 + o0)/256):
  61           256e0 = -x2 + o0 and o0 <= 255 and o0 >= 0) }'
  62         index: '[n] -> { S_1[x1, x2] -> [(x2 - 256*floor((x2)/256))] }'
  63         reference: __pet_ref_4
  64         read: 1
  65         write: 0
  66   arguments:
  67   - type: access
  68     relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, 3 + x2] : x2 <= 6 }'
  69     index: '[n] -> { S_1[x1, x2] -> __pet_test_0[(x1), ((3 + x2) : x2 <= 6)] }'
  70     reference: __pet_ref_1
  71     read: 1
  72     write: 0
  73 - line: 15
  74   domain: '[n] -> { [S2[x1, x2, x3] -> [1]] : exists (e0 = floor((255 - x2)/256),
  75     e1 = floor((x2)/3): 3e1 = x2 and x3 >= 0 and x1 >= 0 and x1 <= -1 + n and x2 <=
  76     9 and 256e0 >= -x2 + x3 and 256e0 <= 255 - x2 and 256e0 >= -x2) }'
  77   schedule: '[n] -> { S2[x1, x2, x3] -> [0, x1, 1, -x2, 1, 0, x3] }'
  78   body:
  79     type: binary
  80     operation: =
  81     arguments:
  82     - type: access
  83       relation: '[n] -> { S2[x1, x2, x3] -> s[] }'
  84       index: '[n] -> { S2[x1, x2, x3] -> s[] }'
  85       reference: __pet_ref_6
  86       read: 0
  87       write: 1
  88     - type: call
  89       name: g
  90       arguments:
  91       - type: binary
  92         operation: +
  93         arguments:
  94         - type: access
  95           relation: '[n] -> { S2[x1, x2, x3] -> s[] }'
  96           index: '[n] -> { S2[x1, x2, x3] -> s[] }'
  97           reference: __pet_ref_7
  98           read: 1
  99           write: 0
 100         - type: access
 101           relation: '[n] -> { S2[x1, x2, x3] -> a[o0, 255 - o0] : exists (e0 = floor((x2)/3),
 102             e1 = floor((-253x2 - 3o0)/768): 3e0 = x2 and 768e1 = -253x2 - 3o0 and
 103             o0 <= 255 and o0 >= 0) }'
 104           index: '[n] -> { S2[x1, x2, x3] -> a[(x2 - 256*floor((x2)/256)), (255 -
 105             x2 + 256*floor((x2)/256))] }'
 106           reference: __pet_ref_8
 107           read: 1
 108           write: 0
 109   arguments:
 110   - type: access
 111     relation: '[n] -> { S2[x1, x2, x3] -> __pet_test_0[x1, x2] }'
 112     index: '[n] -> { S2[x1, x2, x3] -> __pet_test_0[(x1), (x2)] }'
 113     reference: __pet_ref_5
 114     read: 1
 115     write: 0
 116 - line: 17
 117   domain: '[n] -> { R[x1] : x1 <= -1 + n and x1 >= 0 }'
 118   schedule: '[n] -> { R[x1] -> [0, x1, 2] }'
 119   body:
 120     type: call
 121     name: h
 122     arguments:
 123     - type: access
 124       relation: '[n] -> { R[x1] -> s[] }'
 125       index: '[n] -> { R[x1] -> s[] }'
 126       reference: __pet_ref_9
 127       read: 1
 128       write: 0
 129 implications:
 130 - satisfied: 1
 131   extension: '[n] -> { __pet_test_0[x1, x2] -> __pet_test_0[x1, x2''] : exists (e0
 132     = floor((x2'')/3): 3e0 = x2'' and x1 >= 0 and x1 <= -1 + n and x2'' >= x2 and
 133     x2'' <= 9) }'