Tracing PEX condition paths

Damir Dobric Posts

Next talks:

 

Damir@Phone    

Follow me on Twitter: #ddobric



 

 

Archives

If you want to now how exactly PEX is solving conditions (dynamic symbol execution) in different braches of your code, then you should take a look on following example. The method SomeMethod has differnet branches. For each branch there is one condition, which internally locks slightly different.

[PexMethod]
public int SomeMethod(int x, int y)
{
            if (x + y == 7)
            {
                PexStore.Value<string>("Condition", PexSymbolicValue.GetPathConditionString());
                PexStore.Value<string>("Raw Condition",
PexSymbolicValue.GetRawPathConditionString());
                return 1;
            }
            else if (x == 4)
            {
                PexStore.Value<string>("Condition",
PexSymbolicValue.GetPathConditionString());
                PexStore.Value<string>("Raw Condition",
PexSymbolicValue.GetRawPathConditionString());
                return 2;
            }
            else if (y == 3)
            {
                PexStore.Value<string>("Condition",
PexSymbolicValue.GetPathConditionString());
                PexStore.Value<string>("Raw Condition",
PexSymbolicValue.GetRawPathConditionString());
                return 3;
            }
            else if (y == 5)
            {
                PexStore.Value<string>("Condition",
PexSymbolicValue.GetPathConditionString());
                PexStore.Value<string>("Raw Condition",
PexSymbolicValue.GetRawPathConditionString());
                return 3;
            }
            else
            {
                PexStore.Value<string>("Condition",
PexSymbolicValue.GetPathConditionString());
                PexStore.Value<string>("Raw Condition",
PexSymbolicValue.GetRawPathConditionString());
                return 4;
            }
        }

 

When you explore this method with PEX following result appears:


image

Note that statements PexAssume and PexStore are added by me to explore condition paths. They are not consistent part of the program.


Posted Apr 13 2009, 09:03 PM by Damir Dobric
developers.de is a .Net Community Blog powered by daenet GmbH.