tests/for_while_unsigned2.scop

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