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?
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