Example
Consider the program below, which reads in a value and fails if the input is 6. If this program is symbolically executed, a special symbolic variable (as distinct from the program's variables) is associated with the values returned from the read function. These symbolic variables, and expressions of them are tracked in a special symbolic state. The symbolic variable, which we call s, is assigned to y in the symbolic state, later when y is multiplied by two, y is updated to contain the expression 2 * s.
At any control transfer instructions, such as the y ==12, a Path Constraint is updated to track which branch was taken. In this example assuming the condition is true, the Path Constraint is updated, from being empty, to contain: 2 * s ==12.
y = read y = 2 * y if (y == 12) fails print("OK")By negating some of the conditions in the Path Constraint, and by using a constraint solver to obtain satisfying assignments to the modified Path Constraint it is possible to generate inputs that explore new parts of the program.
Read more about this topic: Symbolic Execution
Famous quotes containing the word example:
“Our intellect is not the most subtle, the most powerful, the most appropriate, instrument for revealing the truth. It is life that, little by little, example by example, permits us to see that what is most important to our heart, or to our mind, is learned not by reasoning but through other agencies. Then it is that the intellect, observing their superiority, abdicates its control to them upon reasoned grounds and agrees to become their collaborator and lackey.”
—Marcel Proust (1871–1922)