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