At this point of the program, λ could take any value, and symbolic execution can therefore proceed along both branches, by "forking" two paths.
In this example, the constraint solver would determine that in order to reach the fail() statement, λ would need to equal 6.
Symbolic execution is harder when the same memory location can be accessed through different names (aliasing).
In practice, file operations are implemented as system calls in the kernel, and are outside the control of the symbolic execution tool.
The disadvantage is that the side effects of such calls will clobber all states managed by the symbolic execution engine.
In the example above, the instruction at line 11 would return "some datasome other data" or "some other datasomedata" depending on the sequential ordering of the states.
The advantage is that one would get correct results when symbolically executing programs that interact with the environment.
Tools such as KLEE,[7] Cloud9, and Otter[8] take this approach by implementing models for file system operations, sockets, IPC, etc.
Symbolic execution tools based on virtual machines solve the environment problem by forking the entire VM state.
This approach alleviates the need for writing and maintaining complex models and allows virtually any program binary to be executed symbolically.