tests/for_while_inc.scop

   1 start: 83
   2 end: 234
   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((-1 + x2)/2): 2e0 =
   8     -1 + x2 and 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((-1 + x2)/2): 2e0 =
  37     -1 + x2 and 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] -> [x2] }'
  62           index: '[n] -> { S_1[x1, x2] -> [(x2)] }'
  63           reference: __pet_ref_4
  64           read: 1
  65           write: 0
  66   arguments:
  67   - type: access
  68     relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, -2 + x2] : x2 >= 11 }'
  69     index: '[n] -> { S_1[x1, x2] -> __pet_test_0[(x1), ((-2 + x2) : x2 >= 11)] }'
  70     reference: __pet_ref_1
  71     read: 1
  72     write: 0
  73 - line: 14
  74   domain: '[n] -> { [S2[x1, x2] -> [1]] : exists (e0 = floor((-1 + x2)/2): 2e0 = -1
  75     + x2 and x1 <= -1 + n and x1 >= 0 and x2 >= 9) }'
  76   schedule: '[n] -> { S2[x1, x2] -> [0, x1, 1, x2, 1, 0] }'
  77   body:
  78     type: expression
  79     expr:
  80       type: op
  81       operation: =
  82       arguments:
  83       - type: access
  84         relation: '[n] -> { S2[x1, x2] -> s[] }'
  85         index: '[n] -> { S2[x1, x2] -> s[] }'
  86         reference: __pet_ref_6
  87         read: 0
  88         write: 1
  89       - type: call
  90         name: g
  91         arguments:
  92         - type: access
  93           relation: '[n] -> { S2[x1, x2] -> s[] }'
  94           index: '[n] -> { S2[x1, x2] -> s[] }'
  95           reference: __pet_ref_7
  96           read: 1
  97           write: 0
  98   arguments:
  99   - type: access
 100     relation: '[n] -> { S2[x1, x2] -> __pet_test_0[x1, x2] }'
 101     index: '[n] -> { S2[x1, x2] -> __pet_test_0[(x1), (x2)] }'
 102     reference: __pet_ref_5
 103     read: 1
 104     write: 0
 105 - line: 16
 106   domain: '[n] -> { R[x1] : x1 <= -1 + n and x1 >= 0 }'
 107   schedule: '[n] -> { R[x1] -> [0, x1, 2] }'
 108   body:
 109     type: expression
 110     expr:
 111       type: call
 112       name: h
 113       arguments:
 114       - type: access
 115         relation: '[n] -> { R[x1] -> s[] }'
 116         index: '[n] -> { R[x1] -> s[] }'
 117         reference: __pet_ref_8
 118         read: 1
 119         write: 0
 120 implications:
 121 - satisfied: 1
 122   extension: '[n] -> { __pet_test_0[x1, x2] -> __pet_test_0[x1, x2''] : exists (e0
 123     = floor((-1 + x2'')/2): 2e0 = -1 + x2'' and x2'' <= x2 and x1 >= 0 and x1 <= -1
 124     + n and x2'' >= 9) }'