Java parser with control-flow enumeration

Question

Is there an open-source java parsing tool that can enumerate control flow paths through a method and compute range constraints on integer variables? (A Sat-solver would be great as well)

--EDIT --

This is the answer that triggered this question.

This is the commercial version of the tool I'm thinking of.

My question is - what is the closest open source equivalent?

Answer 1

A close approximation to what your asking for is the Java Symbolic PathFinder. From the site:

Symbolic PathFinder

• Performs symbolic execution of Java bytecodes
• Handles complex math constraints, data structures and arrays, multi-threading, preconditions, strings (on-going work)
• Applies to (executable) models and code
• Generates test vectors and test sequences that are guaranteed to achieve user-specified coverage (e.g. path, statement, branch, MC/DC coverage)
• Measures coverage.
• Generates JUnit tests, Antares simulation scripts, etc. (output can be easily customizable)
• During test generation process, checks for errors
• Is flexible, as it allows for easy encoding of different coverage criteria
• Is integrated with simulation environment (on-going work)

As to your second question, there is a native Java SAT solver: sat4j