tests/for_while_unsigned2.scop

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