tests/for_while_unsigned2.scop

   1 start: 100
   2 end: 316
   3 indent: "\t"
   4 context: '[n] -> {  : -2147483648 <= n <= 2147483647 }'
   5 schedule: '{ domain: "[n] -> { S_4[]; S1[x1] : 0 <= x1 < n; S_1[x1, x2] : 3*floor((x2)/3)
   6   = x2 and 0 <= x1 < n and x2 <= 9; R[x1] : 0 <= x1 < n; S2[x1, x2, x3] : 3*floor((x2)/3)
   7   = x2 and 0 <= x1 < n and x2 <= 9 and x3 >= 0 and 256*floor((x2)/256) <= x2 - x3
   8   }", child: { sequence: [ { filter: "[n] -> { S1[x1]; S_1[x1, x2]; R[x1]; S2[x1,
   9   x2, x3] }", child: { schedule: "[n] -> L_0[{ S1[x1] -> [(x1)]; S_1[x1, x2] -> [(x1)];
  10   R[x1] -> [(x1)]; S2[x1, x2, x3] -> [(x1)] }]", child: { sequence: [ { filter: "[n]
  11   -> { S1[x1] }" }, { filter: "[n] -> { S_1[x1, x2]; S2[x1, x2, x3] }", child: { schedule:
  12   "[n] -> L_1[{ S_1[x1, x2] -> [(-x2)]; S2[x1, x2, x3] -> [(-x2)] }]", child: { sequence:
  13   [ { filter: "[n] -> { S_1[x1, x2] }" }, { filter: "[n] -> { S2[x1, x2, x3] }", child:
  14   { schedule: "[n] -> L_2[{ S2[x1, x2, x3] -> [(x3)] }]" } } ] } } }, { filter: "[n]
  15   -> { R[x1] }" } ] } } }, { filter: "[n] -> { S_4[] }" } ] } }'
  16 arrays:
  17 - context: '{  :  }'
  18   extent: '[n] -> { __pet_test_0[x1, x2] : 3*floor((x2)/3) = x2 and 0 <= x1 < n and
  19     x2 <= 9 }'
  20   value_bounds: '{ [i0] : 0 <= 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 0 <= i1 <= 255 }'
  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] : 0 <= x1 < n }'
  35   body:
  36     type: expression
  37     expr:
  38       type: op
  39       operation: =
  40       arguments:
  41       - type: access
  42         index: '[n] -> { S1[x1] -> s[] }'
  43         reference: __pet_ref_0
  44         read: 0
  45         write: 1
  46       - type: call
  47         name: f
  48 - line: 13
  49   domain: '[n] -> { [S_1[x1, x2] -> [__pet_test_0 = 1]] : 3*floor((x2)/3) = x2 and
  50     0 <= x1 < n and x2 <= 9 }'
  51   body:
  52     type: expression
  53     expr:
  54       type: op
  55       operation: =
  56       arguments:
  57       - type: access
  58         index: '[n] -> { S_1[x1, x2] -> __pet_test_0[(x1), (x2)] }'
  59         reference: __pet_ref_2
  60         read: 0
  61         write: 1
  62       - type: call
  63         name: P
  64         arguments:
  65         - type: access
  66           index: '[n] -> { S_1[x1, x2] -> [(x1)] }'
  67           reference: __pet_ref_3
  68           read: 1
  69           write: 0
  70         - type: access
  71           index: '[n] -> { S_1[x1, x2] -> [(x2 - 256*floor((x2)/256))] }'
  72           reference: __pet_ref_4
  73           read: 1
  74           write: 0
  75   arguments:
  76   - type: access
  77     index: '[n] -> { S_1[x1, x2] -> __pet_test_0[(x1), ((3 + x2) : x2 <= 6)] }'
  78     reference: __pet_ref_1
  79     read: 1
  80     write: 0
  81 - line: 15
  82   domain: '[n] -> { [S2[x1, x2, x3] -> [__pet_test_0 = 1]] : 3*floor((x2)/3) = x2
  83     and 0 <= x1 < n and x2 <= 9 and x3 >= 0 and 256*floor((x2)/256) <= x2 - x3 }'
  84   body:
  85     type: expression
  86     expr:
  87       type: op
  88       operation: =
  89       arguments:
  90       - type: access
  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             index: '[n] -> { S2[x1, x2, x3] -> s[] }'
 103             reference: __pet_ref_7
 104             read: 1
 105             write: 0
 106           - type: access
 107             index: '[n] -> { S2[x1, x2, x3] -> a[(x2 - 256*floor((x2)/256)), (255
 108               - x2 + 256*floor((x2)/256))] }'
 109             reference: __pet_ref_8
 110             read: 1
 111             write: 0
 112   arguments:
 113   - type: access
 114     index: '[n] -> { S2[x1, x2, x3] -> __pet_test_0[(x1), (x2)] }'
 115     reference: __pet_ref_5
 116     read: 1
 117     write: 0
 118 - line: 17
 119   domain: '[n] -> { R[x1] : 0 <= x1 < n }'
 120   body:
 121     type: expression
 122     expr:
 123       type: call
 124       name: h
 125       arguments:
 126       - type: access
 127         index: '[n] -> { R[x1] -> s[] }'
 128         reference: __pet_ref_9
 129         read: 1
 130         write: 0
 131 - line: -1
 132   domain: '[n] -> { S_4[] }'
 133   body:
 134     type: expression
 135     expr:
 136       type: op
 137       operation: kill
 138       arguments:
 139       - type: access
 140         killed: '[n] -> { S_4[] -> s[] }'
 141         index: '[n] -> { S_4[] -> s[] }'
 142         reference: __pet_ref_10
 143         kill: 1
 144 implications:
 145 - satisfied: 1
 146   extension: '[n] -> { __pet_test_0[x1, x2] -> __pet_test_0[x1'' = x1, x2''] : 3*floor((x2'')/3)
 147     = x2'' and 0 <= x1 < n and x2 <= x2'' <= 9 }'