Example Applications

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.