Editing Symbolic execution (section)

==Example==
Consider the program below, which reads in a value and fails if the input is 6.

<syntaxhighlight lang="c" line="1">
int f() {
  ...
  y = read();
  z = y * 2;
  if (z == 12) {
    fail();
  } else {
    printf("OK");
  }
}
</syntaxhighlight>

During a normal execution ("concrete" execution), the program would read a concrete input value (e.g., 5) and assign it to <code>y</code>. Execution would then proceed with the multiplication and the conditional branch, which would evaluate to false and print <code>OK</code>.

During symbolic execution, the program reads a symbolic value (e.g., <code>λ</code>) and assigns it to <code>y</code>. The program would then proceed with the multiplication and assign <code>λ * 2</code> to <code>z</code>. When reaching the <code>if</code> statement, it would evaluate <code>λ * 2 == 12</code>. At this point of the program, <code>λ</code> could take any value, and symbolic execution can therefore proceed along both branches, by "forking" two paths. Each path gets assigned a copy of the program state at the branch instruction as well as a path constraint. In this example, the path constraint is <code>λ * 2 == 12</code> for the <code>if</code> branch and <code>λ * 2 != 12</code> for the <code>else</code> branch. Both paths can be symbolically executed independently. When paths terminate (e.g., as a result of executing <code>fail()</code> or simply exiting), symbolic execution computes a concrete value for <code>λ</code> by solving the accumulated path constraints on each path. These concrete values can be thought of as concrete test cases that can, e.g., help developers reproduce bugs. In this example, the [[constraint solver]] would determine that in order to reach the <code>fail()</code> statement, <code>λ</code> would need to equal 6.