Example Applications

There are two simple example applications that are currently working and on the repo. One is an exhaustive search for all possible end states in order to display the end state and the conditions for reaching it, the other is an exhaustive search over all execution paths in order to find unused code. These are both available through a simple CLI as well as the API.

Checking all possible end states of program execution: This can be done by picking a simple pathing strategy of taking all possible satisfiable paths and appending every end state and then printing off the end states. This is of course extremely computationally expensive as the number of possible paths increases exponentially with size of the program (assuming there is a reasonable density of branches). However, I have found it useful for making sure small patches are memory safe/ are doing the things I expect them to.

Finding unused code blocks: This uses a similar pathing strategy to the enumeration of end states. It can symbolically execute all satisfiable paths, therefore all reachable blocks in the CFG have been reached, which can be compared against the list of all blocks, and therefore generate a list of all unused blocks.

On the way: depth first and randomized search for reachability.