tests/while.scop

   1 start: 83
   2 end: 210
   3 indent: "\t"
   4 context: '[n] -> {  : n <= 2147483647 and n >= -2147483648 }'
   5 arrays:
   6 - context: '{  :  }'
   7   extent: '[n] -> { __pet_test_0[x, t] : x <= -1 + n and x >= 0 and t >= 0 }'
   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[x] : x <= -1 + n and x >= 0 }'
  19   schedule: '[n] -> { S1[x] -> [0, x, 0] }'
  20   body:
  21     type: op
  22     operation: =
  23     arguments:
  24     - type: access
  25       relation: '[n] -> { S1[x] -> s[] }'
  26       index: '[n] -> { S1[x] -> s[] }'
  27       reference: __pet_ref_0
  28       read: 0
  29       write: 1
  30     - type: call
  31       name: f
  32 - line: 13
  33   domain: '[n] -> { [S_1[x, t] -> [1]] : x <= -1 + n and x >= 0 and t >= 0 }'
  34   schedule: '[n] -> { S_1[x, t] -> [0, x, 1, t, 0] }'
  35   body:
  36     type: op
  37     operation: =
  38     arguments:
  39     - type: access
  40       relation: '[n] -> { S_1[x, t] -> __pet_test_0[x, t] }'
  41       index: '[n] -> { S_1[x, t] -> __pet_test_0[(x), (t)] }'
  42       reference: __pet_ref_2
  43       read: 0
  44       write: 1
  45     - type: call
  46       name: P
  47       arguments:
  48       - type: access
  49         relation: '[n] -> { S_1[x, t] -> [x] }'
  50         index: '[n] -> { S_1[x, t] -> [(x)] }'
  51         reference: __pet_ref_3
  52         read: 1
  53         write: 0
  54       - type: access
  55         relation: '[n] -> { S_1[x, t] -> s[] }'
  56         index: '[n] -> { S_1[x, t] -> s[] }'
  57         reference: __pet_ref_4
  58         read: 1
  59         write: 0
  60   arguments:
  61   - type: access
  62     relation: '[n] -> { S_1[x, t] -> __pet_test_0[x, -1 + t] : t >= 1 }'
  63     index: '[n] -> { S_1[x, t] -> __pet_test_0[(x), ((-1 + t) : t >= 1)] }'
  64     reference: __pet_ref_1
  65     read: 1
  66     write: 0
  67 - line: 14
  68   domain: '[n] -> { [S2[x, t] -> [1]] : x <= -1 + n and x >= 0 and t >= 0 }'
  69   schedule: '[n] -> { S2[x, t] -> [0, x, 1, t, 1, 0] }'
  70   body:
  71     type: op
  72     operation: =
  73     arguments:
  74     - type: access
  75       relation: '[n] -> { S2[x, t] -> s[] }'
  76       index: '[n] -> { S2[x, t] -> s[] }'
  77       reference: __pet_ref_6
  78       read: 0
  79       write: 1
  80     - type: call
  81       name: g
  82       arguments:
  83       - type: access
  84         relation: '[n] -> { S2[x, t] -> s[] }'
  85         index: '[n] -> { S2[x, t] -> s[] }'
  86         reference: __pet_ref_7
  87         read: 1
  88         write: 0
  89   arguments:
  90   - type: access
  91     relation: '[n] -> { S2[x, t] -> __pet_test_0[x, t] }'
  92     index: '[n] -> { S2[x, t] -> __pet_test_0[(x), (t)] }'
  93     reference: __pet_ref_5
  94     read: 1
  95     write: 0
  96 - line: 16
  97   domain: '[n] -> { R[x] : x <= -1 + n and x >= 0 }'
  98   schedule: '[n] -> { R[x] -> [0, x, 2] }'
  99   body:
 100     type: call
 101     name: h
 102     arguments:
 103     - type: access
 104       relation: '[n] -> { R[x] -> s[] }'
 105       index: '[n] -> { R[x] -> s[] }'
 106       reference: __pet_ref_8
 107       read: 1
 108       write: 0
 109 implications:
 110 - satisfied: 1
 111   extension: '[n] -> { __pet_test_0[x, t] -> __pet_test_0[x, t''] : t'' <= t and x
 112     >= 0 and x <= -1 + n and t'' >= 0 }'