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         relation: '[n] -> { S1[x1] -> s[] }'
  29         index: '[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 = floor((x2)/3): 3e0 = x2 and
  37     x1 <= -1 + n and x1 >= 0 and x2 <= 9) }'
  38   schedule: '[n] -> { S_1[x1, x2] -> [0, x1, 1, -x2, 0] }'
  39   body:
  40     type: expression
  41     expr:
  42       type: op
  43       operation: =
  44       arguments:
  45       - type: access
  46         relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, x2] }'
  47         index: '[n] -> { S_1[x1, x2] -> __pet_test_0[(x1), (x2)] }'
  48         reference: __pet_ref_2
  49         read: 0
  50         write: 1
  51       - type: call
  52         name: P
  53         arguments:
  54         - type: access
  55           relation: '[n] -> { S_1[x1, x2] -> [x1] }'
  56           index: '[n] -> { S_1[x1, x2] -> [(x1)] }'
  57           reference: __pet_ref_3
  58           read: 1
  59           write: 0
  60         - type: access
  61           relation: '[n] -> { S_1[x1, x2] -> [o0] : exists (e0 = floor((-x2 + o0)/256):
  62             256e0 = -x2 + o0 and o0 <= 255 and o0 >= 0) }'
  63           index: '[n] -> { S_1[x1, x2] -> [(x2 - 256*floor((x2)/256))] }'
  64           reference: __pet_ref_4
  65           read: 1
  66           write: 0
  67   arguments:
  68   - type: access
  69     relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, 3 + x2] : x2 <= 6 }'
  70     index: '[n] -> { S_1[x1, x2] -> __pet_test_0[(x1), ((3 + x2) : x2 <= 6)] }'
  71     reference: __pet_ref_1
  72     read: 1
  73     write: 0
  74 - line: 14
  75   domain: '[n] -> { [S2[x1, x2] -> [1]] : exists (e0 = floor((x2)/3): 3e0 = x2 and
  76     x1 <= -1 + n and x1 >= 0 and x2 <= 9) }'
  77   schedule: '[n] -> { S2[x1, x2] -> [0, x1, 1, -x2, 1, 0] }'
  78   body:
  79     type: expression
  80     expr:
  81       type: op
  82       operation: =
  83       arguments:
  84       - type: access
  85         relation: '[n] -> { S2[x1, x2] -> s[] }'
  86         index: '[n] -> { S2[x1, x2] -> s[] }'
  87         reference: __pet_ref_6
  88         read: 0
  89         write: 1
  90       - type: call
  91         name: g
  92         arguments:
  93         - type: access
  94           relation: '[n] -> { S2[x1, x2] -> s[] }'
  95           index: '[n] -> { S2[x1, x2] -> s[] }'
  96           reference: __pet_ref_7
  97           read: 1
  98           write: 0
  99   arguments:
 100   - type: access
 101     relation: '[n] -> { S2[x1, x2] -> __pet_test_0[x1, x2] }'
 102     index: '[n] -> { S2[x1, x2] -> __pet_test_0[(x1), (x2)] }'
 103     reference: __pet_ref_5
 104     read: 1
 105     write: 0
 106 - line: 16
 107   domain: '[n] -> { R[x1] : x1 <= -1 + n and x1 >= 0 }'
 108   schedule: '[n] -> { R[x1] -> [0, x1, 2] }'
 109   body:
 110     type: expression
 111     expr:
 112       type: call
 113       name: h
 114       arguments:
 115       - type: access
 116         relation: '[n] -> { R[x1] -> s[] }'
 117         index: '[n] -> { R[x1] -> s[] }'
 118         reference: __pet_ref_8
 119         read: 1
 120         write: 0
 121 implications:
 122 - satisfied: 1
 123   extension: '[n] -> { __pet_test_0[x1, x2] -> __pet_test_0[x1, x2''] : exists (e0
 124     = floor((x2'')/3): 3e0 = x2'' and x2'' >= x2 and x1 >= 0 and x1 <= -1 + n and
 125     x2'' <= 9) }'