tests/while.scop

   1 start: 83
   2 end: 210
   3 context: '[n] -> {  : n <= 2147483647 and n >= -2147483648 }'
   4 arrays:
   5 - context: '{  :  }'
   6   extent: '[n] -> { __pet_test_0[x, t] : x <= -1 + n and x >= 0 and t >= 0 }'
   7   value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
   8   element_type: int
   9   element_size: 4
  10   uniquely_defined: 1
  11 - context: '{  :  }'
  12   extent: '[n] -> { s[] }'
  13   element_type: int
  14   element_size: 4
  15 statements:
  16 - line: 12
  17   domain: '[n] -> { S1[x] : x <= -1 + n and x >= 0 }'
  18   schedule: '[n] -> { S1[x] -> [0, x, 0] }'
  19   body:
  20     type: binary
  21     operation: =
  22     arguments:
  23     - type: access
  24       relation: '[n] -> { S1[x] -> s[] }'
  25       index: '[n] -> { S1[x] -> 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[x, t] -> [1]] : x <= -1 + n and x >= 0 and t >= 0 }'
  33   schedule: '[n] -> { S_1[x, t] -> [0, x, 1, t, 0] }'
  34   body:
  35     type: binary
  36     operation: =
  37     arguments:
  38     - type: access
  39       relation: '[n] -> { S_1[x, t] -> __pet_test_0[x, t] }'
  40       index: '[n] -> { S_1[x, t] -> __pet_test_0[(x), (t)] }'
  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[x, t] -> [x] }'
  49         index: '[n] -> { S_1[x, t] -> [(x)] }'
  50         reference: __pet_ref_3
  51         read: 1
  52         write: 0
  53       - type: access
  54         relation: '[n] -> { S_1[x, t] -> s[] }'
  55         index: '[n] -> { S_1[x, t] -> s[] }'
  56         reference: __pet_ref_4
  57         read: 1
  58         write: 0
  59   arguments:
  60   - type: access
  61     relation: '[n] -> { S_1[x, t] -> __pet_test_0[x, -1 + t] : t >= 1 }'
  62     index: '[n] -> { S_1[x, t] -> __pet_test_0[(x), ((-1 + t) : t >= 1)] }'
  63     reference: __pet_ref_1
  64     read: 1
  65     write: 0
  66 - line: 14
  67   domain: '[n] -> { [S2[x, t] -> [1]] : x <= -1 + n and x >= 0 and t >= 0 }'
  68   schedule: '[n] -> { S2[x, t] -> [0, x, 1, t, 1, 0] }'
  69   body:
  70     type: binary
  71     operation: =
  72     arguments:
  73     - type: access
  74       relation: '[n] -> { S2[x, t] -> s[] }'
  75       index: '[n] -> { S2[x, t] -> s[] }'
  76       reference: __pet_ref_6
  77       read: 0
  78       write: 1
  79     - type: call
  80       name: g
  81       arguments:
  82       - type: access
  83         relation: '[n] -> { S2[x, t] -> s[] }'
  84         index: '[n] -> { S2[x, t] -> s[] }'
  85         reference: __pet_ref_7
  86         read: 1
  87         write: 0
  88   arguments:
  89   - type: access
  90     relation: '[n] -> { S2[x, t] -> __pet_test_0[x, t] }'
  91     index: '[n] -> { S2[x, t] -> __pet_test_0[(x), (t)] }'
  92     reference: __pet_ref_5
  93     read: 1
  94     write: 0
  95 - line: 16
  96   domain: '[n] -> { R[x] : x <= -1 + n and x >= 0 }'
  97   schedule: '[n] -> { R[x] -> [0, x, 2] }'
  98   body:
  99     type: call
 100     name: h
 101     arguments:
 102     - type: access
 103       relation: '[n] -> { R[x] -> s[] }'
 104       index: '[n] -> { R[x] -> s[] }'
 105       reference: __pet_ref_8
 106       read: 1
 107       write: 0
 108 implications:
 109 - satisfied: 1
 110   extension: '[n] -> { __pet_test_0[x, t] -> __pet_test_0[x, t''] : x >= 0 and x <=
 111     -1 + n and t'' <= t and t'' >= 0 }'