tests/for_while_unsigned.scop

   1 start: 83
   2 end: 244
   3 context: '[n] -> {  : n <= 2147483647 and n >= -2147483648 }'
   4 arrays:
   5 - context: '{  :  }'
   6   extent: '[n] -> { __pet_test_0[x1, x2] : exists (e0 = floor((x2)/3): 3e0 = x2 and
   7     x1 <= -1 + n and x1 >= 0 and x2 <= 9) }'
   8   value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
   9   element_type: int
  10   element_size: 4
  11   uniquely_defined: 1
  12 - context: '{  :  }'
  13   extent: '[n] -> { s[] }'
  14   element_type: int
  15   element_size: 4
  16 statements:
  17 - line: 12
  18   domain: '[n] -> { S1[x1] : x1 <= -1 + n and x1 >= 0 }'
  19   schedule: '[n] -> { S1[x1] -> [0, x1, 0] }'
  20   body:
  21     type: binary
  22     operation: =
  23     arguments:
  24     - type: access
  25       relation: '[n] -> { S1[x1] -> s[] }'
  26       index: '[n] -> { S1[x1] -> s[] }'
  27       reference: __pet_ref_0
  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 = floor((x2)/3): 3e0 = x2 and
  34     x1 <= -1 + n and x1 >= 0 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       index: '[n] -> { S_1[x1, x2] -> __pet_test_0[(x1), (x2)] }'
  43       reference: __pet_ref_2
  44       read: 0
  45       write: 1
  46     - type: call
  47       name: P
  48       arguments:
  49       - type: access
  50         relation: '[n] -> { S_1[x1, x2] -> [x1] }'
  51         index: '[n] -> { S_1[x1, x2] -> [(x1)] }'
  52         reference: __pet_ref_3
  53         read: 1
  54         write: 0
  55       - type: access
  56         relation: '[n] -> { S_1[x1, x2] -> [o0] : exists (e0 = floor((-x2 + o0)/256):
  57           256e0 = -x2 + o0 and o0 <= 255 and o0 >= 0) }'
  58         index: '[n] -> { S_1[x1, x2] -> [(x2 - 256*floor((x2)/256))] }'
  59         reference: __pet_ref_4
  60         read: 1
  61         write: 0
  62   arguments:
  63   - type: access
  64     relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, 3 + x2] : x2 <= 6 }'
  65     index: '[n] -> { S_1[x1, x2] -> __pet_test_0[(x1), ((3 + x2) : x2 <= 6)] }'
  66     reference: __pet_ref_1
  67     read: 1
  68     write: 0
  69 - line: 14
  70   domain: '[n] -> { [S2[x1, x2] -> [1]] : exists (e0 = floor((x2)/3): 3e0 = x2 and
  71     x1 <= -1 + n and x1 >= 0 and x2 <= 9) }'
  72   schedule: '[n] -> { S2[x1, x2] -> [0, x1, 1, -x2, 1, 0] }'
  73   body:
  74     type: binary
  75     operation: =
  76     arguments:
  77     - type: access
  78       relation: '[n] -> { S2[x1, x2] -> s[] }'
  79       index: '[n] -> { S2[x1, x2] -> s[] }'
  80       reference: __pet_ref_6
  81       read: 0
  82       write: 1
  83     - type: call
  84       name: g
  85       arguments:
  86       - type: access
  87         relation: '[n] -> { S2[x1, x2] -> s[] }'
  88         index: '[n] -> { S2[x1, x2] -> s[] }'
  89         reference: __pet_ref_7
  90         read: 1
  91         write: 0
  92   arguments:
  93   - type: access
  94     relation: '[n] -> { S2[x1, x2] -> __pet_test_0[x1, x2] }'
  95     index: '[n] -> { S2[x1, x2] -> __pet_test_0[(x1), (x2)] }'
  96     reference: __pet_ref_5
  97     read: 1
  98     write: 0
  99 - line: 16
 100   domain: '[n] -> { R[x1] : x1 <= -1 + n and x1 >= 0 }'
 101   schedule: '[n] -> { R[x1] -> [0, x1, 2] }'
 102   body:
 103     type: call
 104     name: h
 105     arguments:
 106     - type: access
 107       relation: '[n] -> { R[x1] -> s[] }'
 108       index: '[n] -> { R[x1] -> s[] }'
 109       reference: __pet_ref_8
 110       read: 1
 111       write: 0
 112 implications:
 113 - satisfied: 1
 114   extension: '[n] -> { __pet_test_0[x1, x2] -> __pet_test_0[x1, x2''] : exists (e0
 115     = floor((x2'')/3): 3e0 = x2'' and x1 >= 0 and x1 <= -1 + n and x2'' >= x2 and
 116     x2'' <= 9) }'