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         index: '[n] -> { S1[x1] -> s[] }'
  33         reference: __pet_ref_0
  34         read: 0
  35         write: 1
  36       - type: call
  37         name: f
  38 - line: 13
  39   domain: '[n] -> { [S_1[x1, x2] -> [1]] : exists (e0 = floor((x2)/3): 3e0 = x2 and
  40     x1 <= -1 + n and x1 >= 0 and x2 <= 9) }'
  41   schedule: '[n] -> { S_1[x1, x2] -> [0, x1, 1, -x2, 0] }'
  42   body:
  43     type: expression
  44     expr:
  45       type: op
  46       operation: =
  47       arguments:
  48       - type: access
  49         index: '[n] -> { S_1[x1, x2] -> __pet_test_0[(x1), (x2)] }'
  50         reference: __pet_ref_2
  51         read: 0
  52         write: 1
  53       - type: call
  54         name: P
  55         arguments:
  56         - type: access
  57           index: '[n] -> { S_1[x1, x2] -> [(x1)] }'
  58           reference: __pet_ref_3
  59           read: 1
  60           write: 0
  61         - type: access
  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     index: '[n] -> { S_1[x1, x2] -> __pet_test_0[(x1), ((3 + x2) : x2 <= 6)] }'
  69     reference: __pet_ref_1
  70     read: 1
  71     write: 0
  72 - line: 15
  73   domain: '[n] -> { [S2[x1, x2, x3] -> [1]] : exists (e0 = floor((x2)/256), e1 = floor((x2)/3):
  74     3e1 = x2 and x3 >= 0 and x1 >= 0 and x1 <= -1 + n and x2 <= 9 and 256e0 <= x2
  75     - x3 and 256e0 <= x2 and 256e0 >= -255 + x2) }'
  76   schedule: '[n] -> { S2[x1, x2, x3] -> [0, x1, 1, -x2, 1, 0, x3] }'
  77   body:
  78     type: expression
  79     expr:
  80       type: op
  81       operation: =
  82       arguments:
  83       - type: access
  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: op
  92           operation: +
  93           arguments:
  94           - type: access
  95             index: '[n] -> { S2[x1, x2, x3] -> s[] }'
  96             reference: __pet_ref_7
  97             read: 1
  98             write: 0
  99           - type: access
 100             index: '[n] -> { S2[x1, x2, x3] -> a[(x2 - 256*floor((x2)/256)), (255
 101               - x2 + 256*floor((x2)/256))] }'
 102             reference: __pet_ref_8
 103             read: 1
 104             write: 0
 105   arguments:
 106   - type: access
 107     index: '[n] -> { S2[x1, x2, x3] -> __pet_test_0[(x1), (x2)] }'
 108     reference: __pet_ref_5
 109     read: 1
 110     write: 0
 111 - line: 17
 112   domain: '[n] -> { R[x1] : x1 <= -1 + n and x1 >= 0 }'
 113   schedule: '[n] -> { R[x1] -> [0, x1, 2] }'
 114   body:
 115     type: expression
 116     expr:
 117       type: call
 118       name: h
 119       arguments:
 120       - type: access
 121         index: '[n] -> { R[x1] -> s[] }'
 122         reference: __pet_ref_9
 123         read: 1
 124         write: 0
 125 implications:
 126 - satisfied: 1
 127   extension: '[n] -> { __pet_test_0[x1, x2] -> __pet_test_0[x1, x2''] : exists (e0
 128     = floor((x2'')/3): 3e0 = x2'' and x2'' >= x2 and x1 >= 0 and x1 <= -1 + n and
 129     x2'' <= 9) }'