We have implemented an analysis for Java with all of the options described in
the previous two sections.
Our implementation is based on the intermediate representation in the
T. J. Watson Libraries for Analysis (WALA) version 1.3.10 [1]},
which converts a Java bytecode program into static single assignment
(SSA) form [2]}, which is then
analyzed. We use APRON [3]}, [4]} trunk revision 1096 (published on 2016/05/31)
implementation of intervals, and ELINA [5]}, [6]}, snapshot as of
October 4, 2017, for convex polyhedra. Our current
implementation supports all non-floating point numeric
Java values and comprises 14K lines of Scala code.
