tests/for_while_inc.scop

   1 context: '[n] -> {  : n <= 2147483647 and n >= -2147483648 }'
   2 arrays:
   3 - context: '{  :  }'
   4   extent: '[n] -> { __pet_test_0[x1, x2] : exists (e0 = [(-1 + x2)/2]: 2e0 = -1 +
   5     x2 and x1 >= 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 = [(-1 + x2)/2]: 2e0 = -1 +
  30     x2 and x1 >= 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] -> [x2] }'
  49         read: 1
  50         write: 0
  51   arguments:
  52   - type: access
  53     relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, o1] : exists (e0 = [(-1 +
  54       o1)/2]: 2e0 = -1 + o1 and o1 <= -2 + x2 and o1 >= 9) }'
  55     read: 1
  56     write: 0
  57 - line: 14
  58   domain: '[n] -> { [S2[x1, x2] -> [1]] : exists (e0 = [(-1 + x2)/2]: 2e0 = -1 + x2
  59     and x1 >= 0 and x1 <= -1 + n and x2 >= 9) }'
  60   schedule: '[n] -> { S2[x1, x2] -> [0, x1, 1, x2, 1, 0] }'
  61   body:
  62     type: binary
  63     operation: =
  64     arguments:
  65     - type: access
  66       relation: '[n] -> { S2[x1, x2] -> s[] }'
  67       read: 0
  68       write: 1
  69     - type: call
  70       name: g
  71       arguments:
  72       - type: access
  73         relation: '[n] -> { S2[x1, x2] -> s[] }'
  74         read: 1
  75         write: 0
  76   arguments:
  77   - type: access
  78     relation: '[n] -> { S2[x1, x2] -> __pet_test_0[x1, o1] : exists (e0 = [(-1 + o1)/2]:
  79       2e0 = -1 + o1 and o1 <= x2 and o1 >= 9) }'
  80     read: 1
  81     write: 0
  82 - line: 16
  83   domain: '[n] -> { R[x1] : x1 >= 0 and x1 <= -1 + n }'
  84   schedule: '[n] -> { R[x1] -> [0, x1, 2] }'
  85   body:
  86     type: call
  87     name: h
  88     arguments:
  89     - type: access
  90       relation: '[n] -> { R[x1] -> s[] }'
  91       read: 1
  92       write: 0