From: Artem Dergachev Date: Thu, 28 Jul 2016 20:13:14 +0000 (+0000) Subject: [analyzer] Update the web manual for checker developers. X-Git-Url: https://granicus.if.org/sourcecode?a=commitdiff_plain;h=cab14a521fafafed727f4e329e53cef270da4af2;p=clang [analyzer] Update the web manual for checker developers. Fix the explanation of how to run tests after migration from autotools to cmake. Significantly expand the "debugging" section with more interesting stuff. Update the table of contents accordingly. Fix paragraphs in the overview section. Differential Revision: https://reviews.llvm.org/D22874 git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@277029 91177308-0d34-0410-b5e6-96231b3b80d8 --- diff --git a/www/analyzer/checker_dev_manual.html b/www/analyzer/checker_dev_manual.html index c674a74284..93c98913fd 100644 --- a/www/analyzer/checker_dev_manual.html +++ b/www/analyzer/checker_dev_manual.html @@ -45,7 +45,13 @@ for developer guidelines and send your questions and proposals to
  • Bug Reports
  • AST Visitors
  • Testing
    • -
  • Useful Commands/Debugging Hints
    • +
  • Useful Commands/Debugging Hints +
  • Additional Sources of Information
  • Useful Links
    • @@ -115,6 +121,8 @@ for developer guidelines and send your questions and proposals to

    Interaction with Checkers

    + +

    Checkers are not merely passive receivers of the analyzer core changes - they actively participate in the ProgramState construction through the GenericDataMap which can be used to store the checker-defined part @@ -123,9 +131,12 @@ for developer guidelines and send your questions and proposals to opportunity to either report a bug or modify the state. (As a rule of thumb, the checker itself should be stateless.) The checkers are called one after another in the predefined order; thus, calling all the checkers adds a chain to the - ExplodedGraph. + ExplodedGraph. +

    Representing Values

    + +

    During symbolic execution, SVal objects are used to represent the semantic evaluation of expressions. They can represent things like concrete @@ -142,7 +153,9 @@ for developer guidelines and send your questions and proposals to This represents a case that is outside the realm of the analyzer's reasoning capabilities. SVals are value objects and their values can be viewed using the .dump() method. Often they wrap persistent objects such as - symbols or regions. + symbols or regions. +

    +

    SymExpr (symbol) is meant to represent abstract, but named, symbolic value. Symbols represent @@ -150,7 +163,7 @@ for developer guidelines and send your questions and proposals to 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 0, etc. -

    +

    MemRegion is similar to a symbol. @@ -163,9 +176,12 @@ for developer guidelines and send your questions and proposals to SymbolicRegion is for. It is a MemRegion that has an associated symbol. Since the symbol is unique and has a unique name; that symbol names the region. +

    -

    +

    Let's see how the analyzer processes the expressions in the following example: +

    + 

       int foo(int x) {
@@ -174,6 +190,8 @@ for developer guidelines and send your questions and proposals to
      ...
   }
    +

    +

    Let's look at how x*2 gets evaluated. When x is evaluated, we first construct an SVal that represents the lvalue of x, in @@ -193,6 +211,7 @@ to the MemRegion in the symbolic store. The second line is similar. When we evaluate x again, we do the same dance, and create an SVal that references the symbol $0. Note, two SVals might reference the same underlying values. +

    To summarize, MemRegions are unique names for blocks of memory. Symbols are @@ -200,6 +219,7 @@ unique names for abstract symbolic values. Some MemRegions represents abstract symbolic chunks of memory, and thus are also based on symbols. SVals are just references to values, and can reference either MemRegions, Symbols, or concrete values (e.g., the number 1). +