We talked in a previous post about Microsoft Pex and how it choose values to explore your code through symbolically executing it and getting all its paths. A code path is the represented by all the conditions that have to be satisfied in order to make the code execution go to this path. Your code conditional statements will lead to different paths according to different input values. Test cases generated by Pex represents the code behavior for specific input values that lead to specific code path.
Within the parameterized unit test You can use the method GetPathConditionString of the PexSymbolicValue class to obtain a textual representation of the current path condition, a predicate (condition) that characterizes an execution path (below, column with title Condition) .
Methods ToRawString and GetRawPathConditionString of the PexSymbolicValue class return expressions representing symbolic values and the path condition, formatted as S-expressions.
As we know, Pex uses the Z3 SMT solver behind the scenes. If you want to get the path conditions before being passed to Z3, do the following:
- Create an environment variable with name z3_logdir and value c:\z3_logdir (or any other directory you want)
- Create an environment variable with name z3_loglevel and value constraintsandmodel .
Now, Pex will create *.z3 files in subdirectories in the z3_logdir you specified in step 1. These files are in Z3 native format and can be later passed to Z3. For more information about this format, refer to Z3 online documentation.
In future posts we will talk more about the Z3 native format and what we can do with it.
