tests/for_while_unsigned2.scop

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