Real-Time Path-Sensitive Analysis in the Eclipse CDTCDT , Tools
With this poster, we show that the Eclipse Platform is equipped to statically verify state-based temporal properties like illegal operations on files. Several components are required: a model of the code, an efficient algorithm to process the model, and a framework to allow new properties to be checked. Fortunately, PTP already provides a model in the form of a control flow graph built from the CDT's AST, and the existing analysis framework provides extensibility. We have developed the final component, a plug-in that implements an efficient algorithm based on Property Simulation. Our plug-in processes the model and provides meaningful output for diagnosing potential bugs.
Property Simulation is a path-sensitive static analysis algorithm that can be run in real-time because it heuristically discards uninteresting branches from the control flow. Currently, the CDT's analysis framework provides an AST visitor to traverse the code that cannot accurately model temporal properties. We use Property Simulation to improve on the framework's visitor approach. Our plug-in reliably detects errors along individual paths and describes the conditions under which they occur. In this poster, we briefly show how we have implemented Property Simulation in Eclipse and how our plug-in can aid developers to identify bugs before they are released.
Elliott Baron is a student at the University of Toronto and a committer for the Linux Tools Project. He previously worked for Red Hat as an Eclipse intern for 16 months.