Author: zaks
Date: Mon Jan 7 18:25:14 2013
New Revision: 171823
URL: http://llvm.org/viewvc/llvm-project?rev=171823&view=rev
Log:
[analyzer] Extend the Representing Values section of the dev manual.
Modified:
cfe/trunk/www/analyzer/checker_dev_manual.html
Modified: cfe/trunk/www/analyzer/checker_dev_manual.html
URL:
http://llvm.org/viewvc/llvm-project/cfe/trunk/www/analyzer/checker_dev_manual.html?rev=171823&r1=171822&r2=171823&view=diff
==============================================================================
--- cfe/trunk/www/analyzer/checker_dev_manual.html (original)
+++ cfe/trunk/www/analyzer/checker_dev_manual.html Mon Jan 7 18:25:14 2013
@@ -116,28 +116,44 @@
<h3>Representing Values</h3>
During symbolic execution, <a
href="http://clang.llvm.org/doxygen/classclang_1_1ento_1_1SVal.html";>SVal</a>
- objects are used to represent the semantic evaluation of expressions. They
can
- represent things like concrete integers, symbolic values, or memory
locations
- (which are memory regions). They are a discriminated union of "values",
- symbolic and otherwise.
+ objects are used to represent the semantic evaluation of expressions.
+ They can represent things like concrete
+ integers, symbolic values, or memory locations (which are memory regions).
+ They are a discriminated union of "values", symbolic and otherwise.
+ If a value isn't symbolic, usually that means there is no symbolic
+ information to track. For example, if the value was an integer, such as
+ <tt>42</tt>, it would be a <a
href="http://clang.llvm.org/doxygen/classclang_1_1ento_1_1nonloc_1_1ConcreteInt.html";>ConcreteInt</a>,
+ and the checker doesn't usually need to track any state with the concrete
+ number. In some cases, <tt>SVal</tt> is not a symbol, but it really should
be
+ a symbolic value. This happens when the analyzer cannot reason about
something
+ (yet). An example is floating point numbers. In such cases, the
+ <tt>SVal</tt> will evaluate to <a
href="http://clang.llvm.org/doxygen/classclang_1_1ento_1_1UnknownVal.html";>UnknownVal<a>.
+ This represents a case that is outside the realm of the analyzer's reasoning
+ capabilities. <tt>SVals</tt> are value objects and their values can be
viewed
+ using the <tt>.dump()</tt> method. Often they wrap persistent objects such
as
+ symbols or regions.
<p>
<a
href="http://clang.llvm.org/doxygen/classclang_1_1ento_1_1SymExpr.html";>SymExpr</a>
(symbol)
- is meant to represent abstract, but named, symbolic value.
- Symbolic values can have constraints associated with them. Symbols represent
+ is meant to represent abstract, but named, symbolic value. Symbols represent
an actual (immutable) value. We might not know what its specific value is,
but
- we can associate constraints with that value as we analyze a path.
+ we can associate constraints with that value as we analyze a path. For
+ example, we might record that the value of a symbol is greater than
+ <tt>0</tt>, etc.
+ <p>
+
<p>
-
<a
href="http://clang.llvm.org/doxygen/classclang_1_1ento_1_1MemRegion.html";>MemRegion</a>
is similar to a symbol.
It is used to provide a lexicon of how to describe abstract memory. Regions
can
layer on top of other regions, providing a layered approach to representing
memory.
For example, a struct object on the stack might be represented by a
<tt>VarRegion</tt>,
but a <tt>FieldRegion</tt> which is a subregion of the <tt>VarRegion</tt>
could
be used to represent the memory associated with a specific field of that
object.
- So how do we represent symbolic memory regions? That's what <a
href="http://clang.llvm.org/doxygen/classclang_1_1ento_1_1SymbolicRegion.html";>SymbolicRegion</a>
- is for. It is a <tt>MemRegion</tt> that has an associated symbol. Since the
+ So how do we represent symbolic memory regions? That's what
+ <a
href="http://clang.llvm.org/doxygen/classclang_1_1ento_1_1SymbolicRegion.html";>SymbolicRegion</a>
+ is for. It is a <tt>MemRegion</tt> that has an associated symbol. Since the
symbol is unique and has a unique name; that symbol names the region.
- <p>
+
+ <P>
Let's see how the analyzer processes the expressions in the following
example:
<p>
<pre class="code_example">
_______________________________________________
cfe-commits mailing list
[email protected]
http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits
