tests/for_while_unsigned2.scop

   1 context: '[n] -> {  : n <= 2147483647 and n >= -2147483648 }'
   2 arrays:
   3 - context: '{  :  }'
   4   extent: '[n] -> { __pet_test_0[x1, x2] : exists (e0 = [(x2)/3]: 3e0 = x2 and x1
   5     >= 0 and x1 <= -1 + n and x2 <= 9) }'
   6   value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
   7   element_type: int
   8   element_size: 4
   9   uniquely_defined: 1
  10 - context: '{  :  }'
  11   extent: '[n] -> { a[i0, i1] : i1 <= 255 and i0 >= 0 and i1 >= 0 }'
  12   element_type: int
  13   element_size: 4
  14 - context: '{  :  }'
  15   extent: '[n] -> { s[] }'
  16   element_type: int
  17   element_size: 4
  18 statements:
  19 - line: 12
  20   domain: '[n] -> { S1[x1] : x1 >= 0 and x1 <= -1 + n }'
  21   schedule: '[n] -> { S1[x1] -> [0, x1, 0] }'
  22   body:
  23     type: binary
  24     operation: =
  25     arguments:
  26     - type: access
  27       relation: '[n] -> { S1[x1] -> s[] }'
  28       read: 0
  29       write: 1
  30     - type: call
  31       name: f
  32 - line: 13
  33   domain: '[n] -> { [S_1[x1, x2] -> [1]] : exists (e0 = [(x2)/3]: 3e0 = x2 and x1
  34     >= 0 and x1 <= -1 + n and x2 <= 9) }'
  35   schedule: '[n] -> { S_1[x1, x2] -> [0, x1, 1, -x2, 0] }'
  36   body:
  37     type: binary
  38     operation: =
  39     arguments:
  40     - type: access
  41       relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, x2] }'
  42       read: 0
  43       write: 1
  44     - type: call
  45       name: P
  46       arguments:
  47       - type: access
  48         relation: '[n] -> { S_1[x1, x2] -> [x1] }'
  49         read: 1
  50         write: 0
  51       - type: access
  52         relation: '[n] -> { S_1[x1, x2] -> [o0] : exists (e0 = [(-x2 + o0)/256]: 256e0
  53           = -x2 + o0 and o0 <= 255 and o0 >= 0) }'
  54         read: 1
  55         write: 0
  56   arguments:
  57   - type: access
  58     relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, o1] : exists (e0 = [(o1)/3]:
  59       3e0 = o1 and o1 <= 9 and o1 >= 3 + x2) }'
  60     read: 1
  61     write: 0
  62 - line: 15
  63   domain: '[n] -> { [S2[x1, x2, x3] -> [1]] : exists (e0 = [(255 - x2)/256], e1 =
  64     [(x2)/3]: 3e1 = x2 and x3 >= 0 and x1 <= -1 + n and x1 >= 0 and x2 <= 9 and 256e0
  65     >= -x2 + x3 and 256e0 <= 255 - x2 and 256e0 >= -x2) }'
  66   schedule: '[n] -> { S2[x1, x2, x3] -> [0, x1, 1, -x2, 1, 0, x3] }'
  67   body:
  68     type: binary
  69     operation: =
  70     arguments:
  71     - type: access
  72       relation: '[n] -> { S2[x1, x2, x3] -> s[] }'
  73       read: 0
  74       write: 1
  75     - type: call
  76       name: g
  77       arguments:
  78       - type: binary
  79         operation: +
  80         arguments:
  81         - type: access
  82           relation: '[n] -> { S2[x1, x2, x3] -> s[] }'
  83           read: 1
  84           write: 0
  85         - type: access
  86           relation: '[n] -> { S2[x1, x2, x3] -> a[o0, 255 - o0] : exists (e0 = [(x2)/3],
  87             e1 = [(-253x2 - 3o0)/768]: 3e0 = x2 and 768e1 = -253x2 - 3o0 and o0 <=
  88             255 and o0 >= 0) }'
  89           read: 1
  90           write: 0
  91   arguments:
  92   - type: access
  93     relation: '[n] -> { S2[x1, x2, x3] -> __pet_test_0[x1, o1] : exists (e0 = [(o1)/3]:
  94       3e0 = o1 and o1 <= 9 and o1 >= x2) }'
  95     read: 1
  96     write: 0
  97 - line: 17
  98   domain: '[n] -> { R[x1] : x1 >= 0 and x1 <= -1 + n }'
  99   schedule: '[n] -> { R[x1] -> [0, x1, 2] }'
 100   body:
 101     type: call
 102     name: h
 103     arguments:
 104     - type: access
 105       relation: '[n] -> { R[x1] -> s[] }'
 106       read: 1
 107       write: 0