Class Name: 
kiasan.examples.gc.GC

Report Rendered: Mon May 04 11:28:33 CDT 2009, by Sireum/Kiasan for Java v0.1.20090504

Methods Covered:
PercentRatio
Class / Method T E Instruction Coverage Branch Coverage Time
306 0
  116/120
  96.67%
  20/22
  90.91%
 1.147s
Total
 306 0
  116/120
  96.67%
  20/22
  90.91%
 1.147s
Source Code:
1   package kiasan.examples.gc;
2   
3   import kiasan.examples.common.LinkedList;
4   
5   public class GC {
6     void collect(final Node r, final LinkedList<Node> ret) {
7       if ((r == null) || ret.contains(r)) {
8         return;
9       }
10      ret.add(r);
11  
12      collect(r.left, ret);
13      collect(r.right, ret);
14    }
15  
16    LinkedList<Node> collectNodes(final Node r) {
17      final LinkedList<Node> ret = new LinkedList<Node>();
18      collect(r, ret);
19      return ret;
20    }
21  
22    boolean equalLists(final LinkedList<Node> nodes, final LinkedList<Node> marked) {
23      return nodes.containsAll(marked) && marked.containsAll(nodes);
24    }
25  
26    //@ requires  (marked != null) && (marked.head != null) && (marked.head.element == null) && marked.isEmpty();
27    //@ ensures this.equalLists(collectNodes(root), marked);
28    public void mark(final Node root, final LinkedList<Node> marked) {
29      Node x;
30      if (root != null) {
31        final LinkedList<Node> pending = new LinkedList<Node>();
32        pending.add(root);
33        while (!pending.isEmpty()) {
34          x = pending.remove();
35          marked.add(x);
36          Node t = x.left;
37          if (t != null) {
38            if (!marked.contains(t)) {
39              pending.add(t);
40            }
41          }
42          // t = null;
43          t = x.right;
44          if (t != null) {
45            if (!marked.contains(t)) {
46              pending.add(t);
47            }
48          }
49        }
50      }
51    }
52  }