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