tests/for_while_unsigned.scop

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