Initial implementation of intra-procedural property simulation.

* org.eclipse.cdt.codan.extension/plugin.xml: Moved checker to new package.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/CloseOpenedFilesChecker.java: Moved.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionState.java: New file.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/PropertyState.java: New file.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/SymbolicState.java: New file.
* org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/FunctionNameParser.java: New file.
* org.eclipse.ptp.pldt.mpi.analysis.cdt/src/org/eclipse/ptp/pldt/mpi/analysis/cdt/graphs/IBlock.java: Added edge support.
* org.eclipse.ptp.pldt.mpi.analysis.cdt/src/org/eclipse/ptp/pldt/mpi/analysis/cdt/graphs/IControlFlowEdge.java: Store CFG edges.
* org.eclipse.ptp.pldt.mpi.analysis.cdt/src/org/eclipse/ptp/pldt/mpi/analysis/cdt/graphs/IControlFlowGraph.java: Added getEdges.
* org.eclipse.ptp.pldt.mpi.analysis.cdt/src/org/eclipse/ptp/pldt/mpi/analysis/cdt/graphs/impl/Block.java: Store CFG edges.
* org.eclipse.ptp.pldt.mpi.analysis.cdt/src/org/eclipse/ptp/pldt/mpi/analysis/cdt/graphs/impl/ControlFlowEdge.java: New file.
* org.eclipse.ptp.pldt.mpi.analysis.cdt/src/org/eclipse/ptp/pldt/mpi/analysis/cdt/graphs/impl/ControlFlowGraph.java: Compute CFG edges.

8 files changed, 602 insertions, 158 deletions

diff --git a/org.eclipse.cdt.codan.extension/plugin.xml b/org.eclipse.cdt.codan.extension/plugin.xml
index f0ae36c..829c8fd 100644
--- a/org.eclipse.cdt.codan.extension/plugin.xml
+++ b/org.eclipse.cdt.codan.extension/plugin.xml
@@ -4,7 +4,7 @@
    <extension
          point="org.eclipse.cdt.codan.core.checkers">
       <checker
-            class="org.eclipse.cdt.codan.extension.CloseOpenedFilesChecker"
+            class="org.eclipse.cdt.codan.extension.checkers.CloseOpenedFilesChecker"
             id="org.eclipse.cdt.codan.extension.CloseOpenedFilesChecker"
             name="Closing unopened file">
          <problem
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/Activator.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/Activator.java
index 4deea76..487f0ba 100644
--- a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/Activator.java
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/Activator.java
@@ -1,3 +1,13 @@
+/*******************************************************************************
+ * Copyright (c) 2009 Elliott Baron
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v1.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v10.html
+ *
+ * Contributors:
+ *    Elliott Baron - initial API and implementation
+ *******************************************************************************/
 package org.eclipse.cdt.codan.extension;
 
 import org.eclipse.core.runtime.IStatus;
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/CloseOpenedFilesChecker.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/CloseOpenedFilesChecker.java
deleted file mode 100644
index 8acdc81..0000000
--- a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/CloseOpenedFilesChecker.java
+++ /dev/null
@@ -1,157 +0,0 @@
-/*******************************************************************************
- * Copyright (c) 2009 Elliott Baron
- * All rights reserved. This program and the accompanying materials
- * are made available under the terms of the Eclipse Public License v1.0
- * which accompanies this distribution, and is available at
- * http://www.eclipse.org/legal/epl-v10.html
- *
- * Contributors:
- *    Elliott Baron - initial API and implementation
- *******************************************************************************/
-package org.eclipse.cdt.codan.extension;
-
-import java.io.File;
-import java.net.URI;
-import java.text.MessageFormat;
-import java.util.ArrayList;
-import java.util.List;
-
-import org.eclipse.cdt.codan.core.model.AbstractIndexAstChecker;
-import org.eclipse.cdt.core.dom.ast.ASTVisitor;
-import org.eclipse.cdt.core.dom.ast.IASTBinaryExpression;
-import org.eclipse.cdt.core.dom.ast.IASTDeclarator;
-import org.eclipse.cdt.core.dom.ast.IASTExpression;
-import org.eclipse.cdt.core.dom.ast.IASTFunctionCallExpression;
-import org.eclipse.cdt.core.dom.ast.IASTIdExpression;
-import org.eclipse.cdt.core.dom.ast.IASTInitializerExpression;
-import org.eclipse.cdt.core.dom.ast.IASTName;
-import org.eclipse.cdt.core.dom.ast.IASTNode;
-import org.eclipse.cdt.core.dom.ast.IASTStatement;
-import org.eclipse.cdt.core.dom.ast.IASTTranslationUnit;
-import org.eclipse.cdt.core.dom.ast.IBinding;
-import org.eclipse.core.resources.IProject;
-import org.eclipse.core.resources.IResource;
-import org.eclipse.core.resources.IWorkspaceRoot;
-import org.eclipse.core.resources.ResourcesPlugin;
-import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.GraphCreator;
-import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.IBlock;
-import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.ICallGraph;
-import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.ICallGraphNode;
-import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.IControlFlowGraph;
-import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.impl.ControlFlowGraph;
-
-public class CloseOpenedFilesChecker extends AbstractIndexAstChecker {
-	private static final String ERR_ID = Activator.PLUGIN_ID + ".CloseOpenedFilesProblem";
-
-	public void processAst(IASTTranslationUnit ast) {
-		// traverse the AST using the visitor pattern
-		CloseOpenedFilesVisitor visitor = new CloseOpenedFilesVisitor();
-		
-		GraphCreator creator = new GraphCreator();
-		
-		// Retrieve resource corresponding to this translation unit
-		String path = ast.getFilePath();
-		URI fileURI = new File(path).toURI();
-		IWorkspaceRoot wsRoot = ResourcesPlugin.getWorkspace().getRoot();
-		IResource[] resources = wsRoot.findFilesForLocationURI(fileURI);
-		if (resources != null && resources.length > 0) {
-			IProject proj = resources[0].getProject();
-			
-			// Create call graph for project
-			ICallGraph cg = creator.createCallGraph(proj);
-			creator.computeCallGraph(cg);
-			
-			// Create control flow graph
-			ICallGraphNode cgRoot = cg.topEntry();
-			IASTStatement fnBody = cgRoot.getFuncDef().getBody();
-			IControlFlowGraph cfg = new ControlFlowGraph(fnBody);
-			cfg.buildCFG();
-			cfg.print();
-			
-			ast.accept(visitor);			
-		}		
-	}
-
-
-	private void reportProblem(IASTName closeFD) {
-		String message = MessageFormat.format("File descriptor \"{0}\" has not been opened", closeFD.toString());
-		reportProblem(ERR_ID, closeFD, message);
-	}
-
-	
-	class CloseOpenedFilesVisitor extends ASTVisitor {
-		
-		public static final String OPEN = "open";
-		public static final String CLOSE = "close";
-		
-		private List<IASTName> openedFDs;
-
-		public CloseOpenedFilesVisitor() {
-			openedFDs = new ArrayList<IASTName>();
-			shouldVisitExpressions = true;
-		}
-		
-		@Override
-		public int visit(IASTExpression expression) {
-			if (expression instanceof IASTFunctionCallExpression) {
-				IASTFunctionCallExpression callExpression = (IASTFunctionCallExpression) expression;
-				IASTExpression funcName = callExpression.getFunctionNameExpression();
-				if (funcName instanceof IASTIdExpression) {
-					IASTName name = ((IASTIdExpression) funcName).getName();
-					String simpleName = String.valueOf(name.getSimpleID());
-					if (simpleName.equals(OPEN)) {
-						IASTNode parent = callExpression.getParent();
-						// Handle initialization in declaration
-						if (parent instanceof IASTInitializerExpression) {
-							parent = parent.getParent();
-							if (parent instanceof IASTDeclarator) {
-								openedFDs.add(((IASTDeclarator) parent).getName());
-							}
-						}
-						// Assignment after declaration
-						else if (parent instanceof IASTBinaryExpression) {
-							IASTExpression op2 = ((IASTBinaryExpression) parent).getOperand2();
-							int operator = ((IASTBinaryExpression) parent).getOperator();
-							if (callExpression.equals(op2) && operator == IASTBinaryExpression.op_assign) { 
-								IASTExpression op1 = ((IASTBinaryExpression) parent).getOperand1();
-								if (op1 instanceof IASTIdExpression) {
-									openedFDs.add(((IASTIdExpression) op1).getName());
-								}
-							}
-						}
-					}
-					else if (simpleName.equals(CLOSE)) {
-						IASTExpression paramExpression = callExpression.getParameterExpression();
-						if (paramExpression instanceof IASTIdExpression) {
-							IASTName fd = ((IASTIdExpression) paramExpression).getName();
-							// Add only if no matching opened FD
-							boolean match = false;
-							for (int i = 0; !match && i < openedFDs.size(); i++) {
-								IASTName opened = openedFDs.get(i);
-								match = matchingFileDescriptors(fd, opened);
-							}
-							
-							if (!match) {
-								reportProblem(fd);
-							}
-						}
-					}
-				}
-				
-				return PROCESS_SKIP;
-			}
-			else {
-				return PROCESS_CONTINUE;
-			}
-		}
-		
-		private boolean matchingFileDescriptors(IASTName closeFD, IASTName openFD) {
-			// FIXME elaborate
-			IBinding closeBinding = closeFD.getBinding();
-			IBinding openBinding = openFD.getBinding();
-			
-			return openBinding != null && closeBinding != null && openBinding.equals(closeBinding);
-		}
-	}
-
-}
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionState.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionState.java
new file mode 100644
index 0000000..ffefec7
--- /dev/null
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/ExecutionState.java
@@ -0,0 +1,61 @@
+/*******************************************************************************
+ * Copyright (c) 2009 Elliott Baron
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v1.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v10.html
+ *
+ * Contributors:
+ *    Elliott Baron - initial API and implementation
+ *******************************************************************************/
+package org.eclipse.cdt.codan.extension;
+
+import java.util.ArrayList;
+import java.util.List;
+
+import org.eclipse.cdt.core.dom.ast.IASTNode;
+
+public class ExecutionState {
+	private List<IASTNode> nodes;
+	private boolean top;
+	private boolean bottom;
+
+	public ExecutionState() {
+		nodes = new ArrayList<IASTNode>();
+	}
+	
+	public void addClause(IASTNode node) {
+		setTop(false);
+		setBottom(false);
+		nodes.add(node);
+	}
+	
+	public void removeClause(IASTNode node) {
+		nodes.remove(node);
+		if (nodes.size() == 0) {
+			setTop(true);
+			setBottom(false);
+		}
+	}
+	
+	public IASTNode[] getClauses() {
+		return nodes.toArray(new IASTNode[nodes.size()]);
+	}
+	
+	public boolean isTop() {
+		return top;
+	}
+	
+	public boolean isBottom() {
+		return bottom;
+	}
+	
+	public void setTop(boolean top) {
+		this.top = top;
+	}
+	
+	public void setBottom(boolean bottom) {
+		this.bottom = bottom;
+	}
+
+}
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/PropertyState.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/PropertyState.java
new file mode 100644
index 0000000..0b02211
--- /dev/null
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/PropertyState.java
@@ -0,0 +1,19 @@
+/*******************************************************************************
+ * Copyright (c) 2009 Elliott Baron
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v1.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v10.html
+ *
+ * Contributors:
+ *    Elliott Baron - initial API and implementation
+ *******************************************************************************/
+package org.eclipse.cdt.codan.extension;
+
+import org.eclipse.cdt.core.dom.ast.IASTStatement;
+
+public abstract class PropertyState {	
+	
+	public abstract PropertyState transition(IASTStatement stmt);
+	
+}
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/SymbolicState.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/SymbolicState.java
new file mode 100644
index 0000000..0907ce5
--- /dev/null
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/SymbolicState.java
@@ -0,0 +1,40 @@
+/*******************************************************************************
+ * Copyright (c) 2009 Elliott Baron
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v1.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v10.html
+ *
+ * Contributors:
+ *    Elliott Baron - initial API and implementation
+ *******************************************************************************/
+package org.eclipse.cdt.codan.extension;
+
+import java.util.Collections;
+import java.util.Set;
+
+public class SymbolicState {
+	private Set<PropertyState> propertyStates;
+	private ExecutionState executionState;
+	
+	public SymbolicState(Set<PropertyState> propertyStates, ExecutionState executionState) {
+		this.propertyStates = propertyStates;
+		this.executionState = executionState;
+	}
+
+	public ExecutionState getExecutionState() {
+		return executionState;
+	}
+	
+	public void setExecutionState(ExecutionState es) {
+		executionState = es;
+	}
+	
+	public Set<PropertyState> getPropertyStates() {
+		return Collections.unmodifiableSet(propertyStates);
+	}
+	
+	public void setPropertyStates(Set<PropertyState> ps) {
+		propertyStates = ps;
+	}
+}
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/CloseOpenedFilesChecker.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/CloseOpenedFilesChecker.java
new file mode 100644
index 0000000..5ed04cc
--- /dev/null
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/CloseOpenedFilesChecker.java
@@ -0,0 +1,410 @@
+/*******************************************************************************
+ * Copyright (c) 2009 Elliott Baron
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v1.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v10.html
+ *
+ * Contributors:
+ *    Elliott Baron - initial API and implementation
+ *******************************************************************************/
+package org.eclipse.cdt.codan.extension.checkers;
+
+import java.io.File;
+import java.net.URI;
+import java.text.MessageFormat;
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+import java.util.Stack;
+
+import org.eclipse.cdt.codan.core.model.AbstractIndexAstChecker;
+import org.eclipse.cdt.codan.extension.Activator;
+import org.eclipse.cdt.codan.extension.ExecutionState;
+import org.eclipse.cdt.codan.extension.PropertyState;
+import org.eclipse.cdt.codan.extension.SymbolicState;
+import org.eclipse.cdt.core.dom.ast.ASTVisitor;
+import org.eclipse.cdt.core.dom.ast.IASTBinaryExpression;
+import org.eclipse.cdt.core.dom.ast.IASTDeclarator;
+import org.eclipse.cdt.core.dom.ast.IASTExpression;
+import org.eclipse.cdt.core.dom.ast.IASTExpressionStatement;
+import org.eclipse.cdt.core.dom.ast.IASTFunctionCallExpression;
+import org.eclipse.cdt.core.dom.ast.IASTIdExpression;
+import org.eclipse.cdt.core.dom.ast.IASTInitializerExpression;
+import org.eclipse.cdt.core.dom.ast.IASTName;
+import org.eclipse.cdt.core.dom.ast.IASTNode;
+import org.eclipse.cdt.core.dom.ast.IASTStatement;
+import org.eclipse.cdt.core.dom.ast.IASTTranslationUnit;
+import org.eclipse.cdt.core.dom.ast.IBinding;
+import org.eclipse.core.resources.IProject;
+import org.eclipse.core.resources.IResource;
+import org.eclipse.core.resources.IWorkspaceRoot;
+import org.eclipse.core.resources.ResourcesPlugin;
+import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.GraphCreator;
+import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.IBlock;
+import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.ICallGraph;
+import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.ICallGraphNode;
+import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.IControlFlowEdge;
+import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.IControlFlowGraph;
+import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.impl.ControlFlowGraph;
+
+public class CloseOpenedFilesChecker extends AbstractIndexAstChecker {
+	private static final String ERR_ID = Activator.PLUGIN_ID + ".CloseOpenedFilesProblem";
+	
+	private static final String OPEN = "open";
+	private static final String CLOSE = "close";
+	private Stack<IBlock> worklist;
+	
+	// Property simulation state info for CFG's edges
+	private Map<IControlFlowEdge, Set<SymbolicState>> edgeInfo;
+	
+	// Property FSM states
+	private PropertyState uninit;
+	private PropertyState error;
+	private PropertyState opened;
+
+	public CloseOpenedFilesChecker() {
+		worklist = new Stack<IBlock>();
+		edgeInfo = new HashMap<IControlFlowEdge, Set<SymbolicState>>();
+		initFSM();
+	}
+
+	public void processAst(IASTTranslationUnit ast) {
+		// traverse the AST using the visitor pattern
+		CloseOpenedFilesVisitor visitor = new CloseOpenedFilesVisitor();
+
+		GraphCreator creator = new GraphCreator();
+
+		// Retrieve resource corresponding to this translation unit
+		String path = ast.getFilePath();
+		URI fileURI = new File(path).toURI();
+		IWorkspaceRoot wsRoot = ResourcesPlugin.getWorkspace().getRoot();
+		IResource[] resources = wsRoot.findFilesForLocationURI(fileURI);
+		if (resources != null && resources.length > 0) {
+			IProject proj = resources[0].getProject();
+
+			// Create call graph for project
+			ICallGraph cg = creator.createCallGraph(proj);
+			creator.computeCallGraph(cg);
+
+			// Create control flow graph
+			ICallGraphNode cgRoot = cg.topEntry();
+			IASTStatement fnBody = cgRoot.getFuncDef().getBody();
+			IControlFlowGraph cfg = new ControlFlowGraph(fnBody);
+			cfg.buildCFG();
+			//cfg.print();
+
+			solve(cfg);
+
+			//			ast.accept(visitor);
+		}		
+	}
+
+
+	private void solve(IControlFlowGraph cfg) {
+		for (IControlFlowEdge edge : cfg.getEdges()) {
+			IASTNode from = edge.getFrom().getContent();
+			IASTNode to = edge.getTo().getContent();
+			System.out.println((from != null ? from.getRawSignature() : from) + " -> " + (to != null ? to.getRawSignature() : to));
+
+			// Initialize edgeInfo for each edge
+			Set<SymbolicState> set = new HashSet<SymbolicState>();
+			edgeInfo.put(edge, set);
+		}
+
+		// Create edgeInfo for entry edge
+		IControlFlowEdge entryEdge = cfg.getEntry().getOutEdges()[0];
+		Set<SymbolicState> symStates = edgeInfo.get(entryEdge);
+		Set<PropertyState> propStates = new HashSet<PropertyState>();
+		propStates.add(uninit);
+		ExecutionState es = new ExecutionState();
+		es.setTop(true);
+		symStates.add(new SymbolicState(propStates, es));
+
+		worklist.push(entryEdge.getTo());
+
+		while (!worklist.isEmpty()) {
+			IBlock blk = worklist.pop();
+			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);
+			}
+			else if (isBranch(blk)) {
+				// Apply flow function for a branch block
+				Set<SymbolicState> oldStates = edgeInfo.get(blk.getInEdges()[0]);
+				Set<SymbolicState> newStatesTrue = flowBranch(blk, oldStates, true);
+				Set<SymbolicState> newStatesFalse = flowBranch(blk, oldStates, false);
+
+				// Assumes 0th out-edge is true branch, 1st out-edge is false branch 
+				add(blk.getOutEdges()[0], newStatesTrue);
+				add(blk.getOutEdges()[1], newStatesFalse);
+			}
+			else {
+				// Apply flow function for a normal block
+				Set<SymbolicState> newStates = flowOther(blk, edgeInfo.get(blk.getInEdges()[0]));
+				printStates(newStates);
+				
+				// Don't process the null exit block
+				if (!blk.equals(cfg.getExit())) {
+					add(blk.getOutEdges()[0], newStates);
+				}
+			}
+		}
+	}
+
+
+	private void printStates(Set<SymbolicState> states) {
+		StringBuffer buf = new StringBuffer();
+		for (SymbolicState s : states) {
+			buf.append("{");
+			for (PropertyState ps : s.getPropertyStates()) {
+				buf.append("{");
+				if (ps.equals(uninit)) {
+					buf.append("$u");
+				}
+				else if (ps.equals(opened)) {
+					buf.append("o");
+				}
+				else /* error */ {
+					buf.append("$e");
+				}
+				buf.append(", ");
+			}
+			buf.replace(buf.length() - 2, buf.length(), "}, ");
+			if (s.getExecutionState().isTop()) {
+				buf.append("[TOP]");
+			}
+			else if (s.getExecutionState().isBottom()) {
+				buf.append("[BOT]");
+			}
+			else {
+				buf.append("[");
+				ExecutionState es = s.getExecutionState();
+				IASTNode[] nodes = es.getClauses();
+				for (IASTNode n : nodes) {
+					buf.append(n.getRawSignature());
+					buf.append(" ");
+				}
+				buf.replace(buf.length() - 1, buf.length(), "]");
+			}
+			buf.append("}");
+		}
+		System.out.println(buf.toString());		
+	}
+
+	private Set<SymbolicState> flowMerge(IBlock blk, Set<SymbolicState> ss1,
+			Set<SymbolicState> ss2) {
+		ss1.addAll(ss2);
+		return group(ss1);
+	}
+
+	private Set<SymbolicState> flowBranch(IBlock blk, Set<SymbolicState> ss, boolean value) {
+		Set<SymbolicState> ret = new HashSet<SymbolicState>();
+		for (SymbolicState s : ss) {
+			SymbolicState s0 = transferBranch(blk, s, value);
+			if (!s0.getExecutionState().isBottom()) {
+				ret.add(s0);
+			}
+		}
+		return group(ret);
+	}
+
+	private Set<SymbolicState> flowOther(IBlock blk, Set<SymbolicState> ss) {
+		Set<SymbolicState> ret = new HashSet<SymbolicState>();
+		for (SymbolicState s : ss) {
+			SymbolicState s0 = transferOther(blk, s);
+			ret.add(s0);
+		}
+		return group(ret);
+	}
+
+	private Set<SymbolicState> group(Set<SymbolicState> ss) {
+		// FIXME Fully Path Sensitive
+		return ss;
+	}
+
+	private SymbolicState transferBranch(IBlock blk, SymbolicState s, boolean value) {
+		// TODO Auto-generated method stub
+		return s;
+	}
+
+	private SymbolicState transferOther(IBlock blk, SymbolicState s) {
+		IASTNode node = blk.getContent();		
+		
+		if (node instanceof IASTExpressionStatement) {
+			// Process property state transition
+			Set<PropertyState> oldStates = s.getPropertyStates();
+			Set<PropertyState> newStates = new HashSet<PropertyState>();
+			for (PropertyState state : oldStates) {
+				newStates.add(state.transition((IASTStatement) node));
+			}
+			s.setPropertyStates(newStates);
+			
+			// Check if we have an assignment statement
+			IASTExpression expr = ((IASTExpressionStatement) node).getExpression();
+			if (expr instanceof IASTBinaryExpression) {
+				IASTBinaryExpression binExpr = (IASTBinaryExpression) expr;
+				int op = binExpr.getOperator();
+
+				// Check operator is an assignment operator
+				if (op >= IASTBinaryExpression.op_assign
+						&& op <= IASTBinaryExpression.op_binaryOrAssign) {
+					IASTExpression o1 = binExpr.getOperand1();
+					if (o1 instanceof IASTIdExpression) {
+						s.getExecutionState().addClause(((IASTIdExpression) o1).getName());
+					}
+				}
+			}
+		}
+		return s;
+	}
+
+	private void add(IControlFlowEdge edge,
+			Set<SymbolicState> ss) {
+		if (!edgeInfo.get(edge).equals(ss)) {
+			edgeInfo.put(edge, ss);
+			worklist.push(edge.getTo());
+		}
+	}
+	
+	private void initFSM() {
+		uninit = new PropertyState() {			
+			@Override
+			public PropertyState transition(IASTStatement stmt) {
+				PropertyState dest = uninit;
+				if (containsOpen(stmt)) {
+					dest = opened;
+				}
+				else if (containsClose(stmt)) {
+					dest = error;
+				}
+				return dest;
+			}
+		};
+		
+		opened = new PropertyState() {			
+			@Override
+			public PropertyState transition(IASTStatement stmt) {
+				PropertyState dest = opened;
+				if (containsOpen(stmt)) {
+					dest = error;
+				}
+				if (containsClose(stmt)) {
+					dest = uninit;
+				}
+				return dest;
+			}
+		};
+		
+		error = new PropertyState() {
+			
+			@Override
+			public PropertyState transition(IASTStatement stmt) {
+				return error;
+			}
+		};
+	}
+
+	protected boolean containsOpen(IASTStatement stmt) {
+		// TODO Examine more than just name
+		FunctionNameParser parser = new FunctionNameParser(stmt, OPEN);
+		return parser.matches();
+	}
+
+	protected boolean containsClose(IASTStatement stmt) {
+		// TODO Examine more than just name
+		FunctionNameParser parser = new FunctionNameParser(stmt, CLOSE);
+		return parser.matches();
+	}
+
+	private boolean isBranch(IBlock blk) {
+		return blk.getOutEdges().length > 1;
+	}
+
+	private boolean isMerge(IBlock blk) {
+		return blk.getInEdges().length > 1;
+	}
+
+	private void reportProblem(IASTName closeFD) {
+		String message = MessageFormat.format("File descriptor \"{0}\" has not been opened", closeFD.toString());
+		reportProblem(ERR_ID, closeFD, message);
+	}
+
+
+	class CloseOpenedFilesVisitor extends ASTVisitor {
+
+		private List<IASTName> openedFDs;
+
+		public CloseOpenedFilesVisitor() {
+			openedFDs = new ArrayList<IASTName>();
+			shouldVisitExpressions = true;
+		}
+
+		@Override
+		public int visit(IASTExpression expression) {
+			if (expression instanceof IASTFunctionCallExpression) {
+				IASTFunctionCallExpression callExpression = (IASTFunctionCallExpression) expression;
+				IASTExpression funcName = callExpression.getFunctionNameExpression();
+				if (funcName instanceof IASTIdExpression) {
+					IASTName name = ((IASTIdExpression) funcName).getName();
+					String simpleName = String.valueOf(name.getSimpleID());
+					if (simpleName.equals(OPEN)) {
+						IASTNode parent = callExpression.getParent();
+						// Handle initialization in declaration
+						if (parent instanceof IASTInitializerExpression) {
+							parent = parent.getParent();
+							if (parent instanceof IASTDeclarator) {
+								openedFDs.add(((IASTDeclarator) parent).getName());
+							}
+						}
+						// Assignment after declaration
+						else if (parent instanceof IASTBinaryExpression) {
+							IASTExpression op2 = ((IASTBinaryExpression) parent).getOperand2();
+							int operator = ((IASTBinaryExpression) parent).getOperator();
+							if (callExpression.equals(op2) && operator == IASTBinaryExpression.op_assign) { 
+								IASTExpression op1 = ((IASTBinaryExpression) parent).getOperand1();
+								if (op1 instanceof IASTIdExpression) {
+									openedFDs.add(((IASTIdExpression) op1).getName());
+								}
+							}
+						}
+					}
+					else if (simpleName.equals(CLOSE)) {
+						IASTExpression paramExpression = callExpression.getParameterExpression();
+						if (paramExpression instanceof IASTIdExpression) {
+							IASTName fd = ((IASTIdExpression) paramExpression).getName();
+							// Add only if no matching opened FD
+							boolean match = false;
+							for (int i = 0; !match && i < openedFDs.size(); i++) {
+								IASTName opened = openedFDs.get(i);
+								match = matchingFileDescriptors(fd, opened);
+							}
+
+							if (!match) {
+								reportProblem(fd);
+							}
+						}
+					}
+				}
+
+				return PROCESS_SKIP;
+			}
+			else {
+				return PROCESS_CONTINUE;
+			}
+		}
+
+		private boolean matchingFileDescriptors(IASTName closeFD, IASTName openFD) {
+			// FIXME elaborate
+			IBinding closeBinding = closeFD.getBinding();
+			IBinding openBinding = openFD.getBinding();
+
+			return openBinding != null && closeBinding != null && openBinding.equals(closeBinding);
+		}
+	}
+
+}
diff --git a/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/FunctionNameParser.java b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/FunctionNameParser.java
new file mode 100644
index 0000000..ae287f1
--- /dev/null
+++ b/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/FunctionNameParser.java
@@ -0,0 +1,61 @@
+/*******************************************************************************
+ * Copyright (c) 2009 Elliott Baron
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v1.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v10.html
+ *
+ * Contributors:
+ *    Elliott Baron - initial API and implementation
+ *******************************************************************************/
+package org.eclipse.cdt.codan.extension.checkers;
+
+import org.eclipse.cdt.core.dom.ast.ASTVisitor;
+import org.eclipse.cdt.core.dom.ast.IASTExpression;
+import org.eclipse.cdt.core.dom.ast.IASTFunctionCallExpression;
+import org.eclipse.cdt.core.dom.ast.IASTIdExpression;
+import org.eclipse.cdt.core.dom.ast.IASTName;
+import org.eclipse.cdt.core.dom.ast.IASTStatement;
+
+public class FunctionNameParser {
+	private IASTStatement stmt;
+	private String funcName;
+	
+	public FunctionNameParser(IASTStatement stmt, String funcName) {
+		this.stmt = stmt;
+		this.funcName = funcName;
+	}
+	
+	public boolean matches() {
+		FunctionNameVisitor visitor = new FunctionNameVisitor();
+		stmt.accept(visitor);
+		return visitor.getResult();
+	}
+
+	private class FunctionNameVisitor extends ASTVisitor {
+		private boolean result;
+		
+		public FunctionNameVisitor() {
+			shouldVisitExpressions = true;
+		}
+		
+		@Override
+		public int visit(IASTExpression expr) {
+			if (expr instanceof IASTFunctionCallExpression) {
+				IASTFunctionCallExpression callExpression = (IASTFunctionCallExpression) expr;
+				IASTExpression funcName = callExpression.getFunctionNameExpression();
+				if (funcName instanceof IASTIdExpression) {
+					IASTName name = ((IASTIdExpression) funcName).getName();
+					result = name.toString().equals(FunctionNameParser.this.funcName);
+					return PROCESS_SKIP;
+				}
+			}
+			return PROCESS_CONTINUE;
+		}
+		
+		public boolean getResult() {
+			return result;
+		}
+		
+	}
+}