tests/for_while_unsigned.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] -> { s[] }'
  12   element_type: int
  13   element_size: 4
  14 statements:
  15 - line: 12
  16   domain: '[n] -> { S1[x1] : x1 >= 0 and x1 <= -1 + n }'
  17   schedule: '[n] -> { S1[x1] -> [0, x1, 0] }'
  18   body:
  19     type: binary
  20     operation: =
  21     arguments:
  22     - type: access
  23       relation: '[n] -> { S1[x1] -> s[] }'
  24       read: 0
  25       write: 1
  26     - type: call
  27       name: f
  28 - line: 13
  29   domain: '[n] -> { [S_1[x1, x2] -> [1]] : exists (e0 = [(x2)/3]: 3e0 = x2 and x1
  30     >= 0 and x1 <= -1 + n and x2 <= 9) }'
  31   schedule: '[n] -> { S_1[x1, x2] -> [0, x1, 1, -x2, 0] }'
  32   body:
  33     type: binary
  34     operation: =
  35     arguments:
  36     - type: access
  37       relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, x2] }'
  38       read: 0
  39       write: 1
  40     - type: call
  41       name: P
  42       arguments:
  43       - type: access
  44         relation: '[n] -> { S_1[x1, x2] -> [x1] }'
  45         read: 1
  46         write: 0
  47       - type: access
  48         relation: '[n] -> { S_1[x1, x2] -> [o0] : exists (e0 = [(-x2 + o0)/256]: 256e0
  49           = -x2 + o0 and o0 <= 255 and o0 >= 0) }'
  50         read: 1
  51         write: 0
  52   arguments:
  53   - type: access
  54     relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, o1] : exists (e0 = [(o1)/3]:
  55       3e0 = o1 and o1 <= 9 and o1 >= 3 + x2) }'
  56     read: 1
  57     write: 0
  58 - line: 14
  59   domain: '[n] -> { [S2[x1, x2] -> [1]] : exists (e0 = [(x2)/3]: 3e0 = x2 and x1 >=
  60     0 and x1 <= -1 + n and x2 <= 9) }'
  61   schedule: '[n] -> { S2[x1, x2] -> [0, x1, 1, -x2, 1, 0] }'
  62   body:
  63     type: binary
  64     operation: =
  65     arguments:
  66     - type: access
  67       relation: '[n] -> { S2[x1, x2] -> s[] }'
  68       read: 0
  69       write: 1
  70     - type: call
  71       name: g
  72       arguments:
  73       - type: access
  74         relation: '[n] -> { S2[x1, x2] -> s[] }'
  75         read: 1
  76         write: 0
  77   arguments:
  78   - type: access
  79     relation: '[n] -> { S2[x1, x2] -> __pet_test_0[x1, o1] : exists (e0 = [(o1)/3]:
  80       3e0 = o1 and o1 <= 9 and o1 >= x2) }'
  81     read: 1
  82     write: 0
  83 - line: 16
  84   domain: '[n] -> { R[x1] : x1 >= 0 and x1 <= -1 + n }'
  85   schedule: '[n] -> { R[x1] -> [0, x1, 2] }'
  86   body:
  87     type: call
  88     name: h
  89     arguments:
  90     - type: access
  91       relation: '[n] -> { R[x1] -> s[] }'
  92       read: 1
  93       write: 0