Fixed infinite loop bug for loop structures.

* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/PropertySimulator.java: Added some code to aid debugging.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/TruthAssignment.java: Implement equals and hashCode.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/AbstractOpenCloseChecker.java: Do not create CG for whole project.

3 files changed, 77 insertions, 15 deletions

diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/PropertySimulator.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/PropertySimulator.java
index ba9199f..80e393f 100644
--- a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/PropertySimulator.java
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/PropertySimulator.java
@@ -21,6 +21,7 @@ import java.util.Map.Entry;
 
 import org.eclipse.cdt.core.dom.ast.IASTBinaryExpression;
 import org.eclipse.cdt.core.dom.ast.IASTExpression;
+import org.eclipse.cdt.core.dom.ast.IASTFileLocation;
 import org.eclipse.cdt.core.dom.ast.IASTIdExpression;
 import org.eclipse.cdt.core.dom.ast.IASTLiteralExpression;
 import org.eclipse.cdt.core.dom.ast.IASTName;
@@ -39,12 +40,25 @@ public class PropertySimulator {
 	private IControlFlowGraph cfg;
 	private IPropertyFSM fsm;
 	
+	//XXX
+	private Map<IBlock, Integer> exploreCount; 
 	public PropertySimulator(IControlFlowGraph cfg, IPropertyFSM fsm) {
 		this.cfg = cfg;
 		this.fsm = fsm;
 		worklist = new LinkedList<IBlock>();
 		edgeInfo = new HashMap<IControlFlowEdge, Set<SymbolicState>>();
+		exploreCount = new HashMap<IBlock, Integer>();
+		for (IBlock blk : cfg.getBlocks()) {
+			exploreCount.put(blk, 0);
+		}
 		solve();
+		for (Entry<IBlock, Integer> entry : exploreCount.entrySet()) {
+			if (entry.getValue().equals(0)) {
+				IBlock blk = entry.getKey();
+				System.out.println("Unprocessed block " + blk.getID() + ": ");
+				blk.print();
+			}
+		}
 	}
 
 	private void solve() {
@@ -63,17 +77,26 @@ public class PropertySimulator {
 
 		worklist.add(entryEdge.getTo());
 		// XXX Debug
-		printStates(entryEdge, symStates);
+		System.out.println(printStates(entryEdge, symStates));
 
 		while (!worklist.isEmpty()) {
 			IBlock blk = worklist.remove();
+			if (!blk.equals(cfg.getEntry()) && !blk.equals(cfg.getExit())) {
+				Integer count = exploreCount.get(blk);
+				exploreCount.put(blk, ++count);
+			}
+			
 			if (isMerge(blk)) {
 				// Apply flow function for a merge block
 				Set<SymbolicState> newStates = flowMerge(blk, edgeInfo.get(blk.getInEdges()[0]), edgeInfo.get(blk.getInEdges()[1]));
-				add(blk.getOutEdges()[0], newStates);
 				
-				// XXX Debug
-				System.out.println("MRG: " + printStates(blk.getOutEdges()[0], newStates));
+				// Don't process the null exit block
+				if (!blk.equals(cfg.getExit())) {
+					add(blk.getOutEdges()[0], newStates);
+
+					// XXX Debug
+					System.out.println("MRG: " + printStates(blk.getOutEdges()[0], newStates));
+				}
 			}
 			else if (isBranch(blk)) {
 				// Apply flow function for a branch block
@@ -102,7 +125,26 @@ public class PropertySimulator {
 			}
 		}
 	}
-	
+
+	private void add(IControlFlowEdge edge,
+			Set<SymbolicState> ss) {
+		//XXX
+//		IBlock from = edge.getFrom();
+//		if (from.getContent() != null
+//				&& from.getContent().getRawSignature().contains("nextarg (\">\")")
+//				&& edgeInfo.get(edge).size() > 0) {
+//			System.out.println(printStates(edge, ss));
+//			SymbolicState oldInfo = edgeInfo.get(edge).iterator().next();
+//			SymbolicState newInfo = ss.iterator().next();
+//			System.out.println("equals: " + oldInfo.equals(newInfo));
+//			System.out.println("hashCode: " + (oldInfo.hashCode() == newInfo.hashCode()));
+//		}
+		if (!edgeInfo.get(edge).equals(ss)) {
+			edgeInfo.put(edge, ss);
+			worklist.add(edge.getTo());
+		}
+	}
+
 	public Set<SymbolicState> getEndStates() {
 		IControlFlowEdge exitEdge = cfg.getExit().getInEdges()[0];
 		return edgeInfo.get(exitEdge);
@@ -112,6 +154,20 @@ public class PropertySimulator {
 		StringBuffer buf = new StringBuffer();
 		IASTNode from = edge.getFrom().getContent();
 		IASTNode to = edge.getTo().getContent();
+		if (from != null) {
+			IASTFileLocation loc = from.getFileLocation();
+			if (loc != null) {
+				int start = loc.getStartingLineNumber();
+				int end = loc.getEndingLineNumber();
+				if (start != end) {
+					buf.append("lines " + start + " - " + end);
+				}
+				else {
+					buf.append("line " + start);
+				}
+				buf.append(" ");
+			}
+		}
 		buf.append("{");
 		buf.append(from == null ? from : from.getRawSignature());
 		buf.append(" -> ");
@@ -332,14 +388,6 @@ public class PropertySimulator {
 		return s;
 	}
 
-	private void add(IControlFlowEdge edge,
-			Set<SymbolicState> ss) {
-		if (!edgeInfo.get(edge).equals(ss)) {
-			edgeInfo.put(edge, ss);
-			worklist.add(edge.getTo());
-		}
-	}
-	
 	private boolean isBranch(IBlock blk) {
 		return blk.getOutEdges().length > 1;
 	}
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/TruthAssignment.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/TruthAssignment.java
index a9c50dc..ffc1502 100644
--- a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/TruthAssignment.java
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/TruthAssignment.java
@@ -18,5 +18,19 @@ public class TruthAssignment {
 	public Boolean getValue() {
 		return value;
 	}
+	
+	@Override
+	public boolean equals(Object obj) {
+		if (obj instanceof TruthAssignment) {
+			TruthAssignment other = (TruthAssignment) obj;
+			return blk.equals(other.getOrigin()) && value.equals(other.getValue());
+		}
+		return false;
+	}
+	
+	@Override
+	public int hashCode() {
+		return blk.hashCode() + value.hashCode();
+	}
 
 }
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/AbstractOpenCloseChecker.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/AbstractOpenCloseChecker.java
index f457364..482c5ad 100644
--- a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/AbstractOpenCloseChecker.java
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/AbstractOpenCloseChecker.java
@@ -55,10 +55,10 @@ public abstract class AbstractOpenCloseChecker extends AbstractIndexAstChecker {
 		IWorkspaceRoot wsRoot = ResourcesPlugin.getWorkspace().getRoot();
 		IResource[] resources = wsRoot.findFilesForLocationURI(fileURI);
 		if (resources != null && resources.length > 0) {
-			IProject proj = resources[0].getProject();
+			IResource res = resources[0];
 
 			// Create call graph for project
-			ICallGraph cg = creator.createCallGraph(proj);
+			ICallGraph cg = creator.createCallGraph(res);
 			creator.computeCallGraph(cg);
 
 			// Create control flow graph for each function