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: expression
  23     expr:
  24       type: op
  25       operation: =
  26       arguments:
  27       - type: access
  28         index: '[n] -> { S1[x1] -> s[] }'
  29         reference: __pet_ref_0
  30         read: 0
  31         write: 1
  32       - type: call
  33         name: f
  34 - line: 13
  35   domain: '[n] -> { [S_1[x1, x2] -> [1]] : exists (e0 = floor((x2)/3): 3e0 = x2 and
  36     x1 <= -1 + n and x1 >= 0 and x2 <= 9) }'
  37   schedule: '[n] -> { S_1[x1, x2] -> [0, x1, 1, -x2, 0] }'
  38   body:
  39     type: expression
  40     expr:
  41       type: op
  42       operation: =
  43       arguments:
  44       - type: access
  45         index: '[n] -> { S_1[x1, x2] -> __pet_test_0[(x1), (x2)] }'
  46         reference: __pet_ref_2
  47         read: 0
  48         write: 1
  49       - type: call
  50         name: P
  51         arguments:
  52         - type: access
  53           index: '[n] -> { S_1[x1, x2] -> [(x1)] }'
  54           reference: __pet_ref_3
  55           read: 1
  56           write: 0
  57         - type: access
  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     index: '[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: 14
  69   domain: '[n] -> { [S2[x1, x2] -> [1]] : exists (e0 = floor((x2)/3): 3e0 = x2 and
  70     x1 <= -1 + n and x1 >= 0 and x2 <= 9) }'
  71   schedule: '[n] -> { S2[x1, x2] -> [0, x1, 1, -x2, 1, 0] }'
  72   body:
  73     type: expression
  74     expr:
  75       type: op
  76       operation: =
  77       arguments:
  78       - type: access
  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           index: '[n] -> { S2[x1, x2] -> s[] }'
  88           reference: __pet_ref_7
  89           read: 1
  90           write: 0
  91   arguments:
  92   - type: access
  93     index: '[n] -> { S2[x1, x2] -> __pet_test_0[(x1), (x2)] }'
  94     reference: __pet_ref_5
  95     read: 1
  96     write: 0
  97 - line: 16
  98   domain: '[n] -> { R[x1] : x1 <= -1 + n and x1 >= 0 }'
  99   schedule: '[n] -> { R[x1] -> [0, x1, 2] }'
 100   body:
 101     type: expression
 102     expr:
 103       type: call
 104       name: h
 105       arguments:
 106       - type: access
 107         index: '[n] -> { R[x1] -> s[] }'
 108         reference: __pet_ref_8
 109         read: 1
 110         write: 0
 111 implications:
 112 - satisfied: 1
 113   extension: '[n] -> { __pet_test_0[x1, x2] -> __pet_test_0[x1, x2''] : exists (e0
 114     = floor((x2'')/3): 3e0 = x2'' and x2'' >= x2 and x1 >= 0 and x1 <= -1 + n and
 115     x2'' <= 9) }'