Tags:Relational domain, Sparse analysis and SSA representation
Abstract:
Relational static analyses allow to keep track of the relations between variables in a program. They rely on relational abstract domains like Octagon or Polyhedra. While expressive, these analyses are often costly. To reduce these computations, we design a flow insensitive static analysis that provides a single relational invariant for a whole program. A specific representation of the program, namely the \emph{Static Single Information} (SSI) form, allows us to preserve a good precision (compare to a flow-sensitive analysis) thanks to the indexing of the variables. We report on the design and the soudness of the analysis, using an abstract interpretation methodology. A prototype has been developped to test the usefulness of the analysis on small programs.