|
To understand the automatic symbolization approaches, lets discuss the following examples.
First, we have an uninitialized local variable, a, on line 2. According to C and C++ standards, its value is indeterminate. To ensure the executor can explore every possible path, our approach automatically marks these uninitialized variables as symbolic.
Second, in this example, we see a function call where the source code isnt available to the executor. In these cases, our method automatically symbolises the return value.
Finally, consider a symbolic pointer, p. Rather than allocating memory undera pointer, we use a lazy approach. When the code accesses an index—like p[5] on line 2—we create a single symbolic memory object. This specific object is then used for any subsequent operations. |