Lines Matching full:symbolic
91 The analyzer core performs symbolic execution of the given program. All the
92 input values are represented with symbolic values; further, the engine deduces
111 <li><tt>Environment</tt> - a mapping from source code expressions to symbolic
113 <li><tt>Store</tt> - a mapping from memory locations to symbolic values
114 <li><tt>GenericDataMap</tt> - constraints on symbolic values
129 During symbolic execution, <a href="http://clang.llvm.org/doxygen/classclang_1_1ento_1_1SVal.html">SVal</a>
132 integers, symbolic values, or memory locations (which are memory regions).
133 They are a discriminated union of "values", symbolic and otherwise.
134 If a value isn't symbolic, usually that means there is no symbolic
139 a symbolic value. This happens when the analyzer cannot reason about something
148 is meant to represent abstract, but named, symbolic value. Symbols represent
162 So how do we represent symbolic memory regions? That's what
183 symbolic; it's whatever <tt>x</tt> was bound to at the start of the function.
188 this case is a new symbolic expression, which we might call <tt>$1</tt>). When we
190 and then bind the <tt>SVal</tt> for the RHS (which references the symbolic value <tt>$1</tt>)
191 to the <tt>MemRegion</tt> in the symbolic store.
199 unique names for abstract symbolic values. Some MemRegions represents abstract
200 symbolic chunks of memory, and thus are also based on symbols. SVals are just
225 solver to model symbolic execution.</li>
387 symbolic expression; a map type is the most logical way to implement this. The
388 key for this map will be a pointer to a symbolic expression
389 (<tt>SymbolRef</tt>). If the data type to be associated with the symbolic
