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