<div dir="ltr">Hi Aleksei,<div><br></div><div>Once again thanks a lot for your inputs. I have modified the checker to create a chain of ExplodedNodes as you suggested and will test it.</div><div><br></div><div>BTW, I used C.addTransition(state, E) instead of <span style="font-size:12.8px">C.generateNonFatalError</span><span style="font-size:12.8px">Node(InitialState, MarkedNode)) because I did not find a version of </span><span style="font-size:12.8px">generateNonFatalError</span><span style="font-size:12.8px">Node() whose second argument is the predecessor ExplodedNode to which the current node needs to be attached.</span></div><div><span style="font-size:12.8px"><br></span></div><div><span style="font-size:12.8px">Regards,</span></div><div><span style="font-size:12.8px">Venu.</span></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Feb 14, 2017 at 5:20 PM, Aleksei Sidorin <span dir="ltr"><<a href="mailto:a.sidorin@samsung.com" target="_blank">a.sidorin@samsung.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
  
    
  
  <div bgcolor="#FFFFFF" text="#000000">
    <div class="m_-9191505789861700145moz-cite-prefix">Hi Venugopal,<br>
      <br>
      There is a way to do it. The simplest way, as I guess, is to
      create a chain of ExplodedNodes with your states. The code will
      look similar to this:<br>
      <br>
      ProgramStateRef InitialState = C.getState();<br>
      ProgramStateRef MarkedState =
      InitialState->set<...>(...);<br>
      if (ExplodedNode *MarkedNode =
      C.generate[NonFatalError?]<wbr>Node(MarkedState)) {<br>
        ExplodedNode *NonMarkedNode =
      C.generate[NonFatalError?]<wbr>Node(InitialState, MarkedNode))<br>
      }<br>
      <br>
      So, the chain will look like this:<br>
      <InitialState, InitialNode> => <MarkedState,
      MarkedNode> => <InitialState, NonMarkedNode><br>
      <br>
      But if you want to just add some mark to a newly-created node, you
      can not use state at all. Instead, you can just create a node with
      a specified tag.<br>
      <br>
      static SimpleProgramPointTag CustomTag("My marked node!");<br>
      ExplodedNode *NodeWithSpecialTag =
      C.generate[NonFatalError?]<wbr>Node(NewState, C.getPredecessor(),
      &CustomTag);<br>
      <br>
      <br>
      <br>
      13.02.2017 15:57, Venugopal Raghavan пишет:<br>
    </div><div><div class="h5">
    <blockquote type="cite">
      <div dir="ltr">Hi Aleksei,
        <div><br>
        </div>
        <div>Thanks, I have re-written the checker based on your
          suggestion. </div>
        <div><br>
        </div>
        <div>The custom program state that a checker adds to a program
          state gets propagated to succeeding states also unless they
          are explicitly removed. Is there a way to write some data into
          the custom state which is valid only for that state and does
          not get propagated to succeeding states? I did something like
          this:</div>
        <div><br>
        </div>
        <div>
          <div>ProgramStateRef state = C.getState();   // C is
            CheckerContext</div>
          <div>const LocationContext *lctx = C.getLocationContext();</div>
          <div>SVal val = state->getSVal(S, lctx);</div>
          <div>SymbolRef Sym = val.getAsSymbol();  // Symbol I want to
            be added to this state and to this state alone</div>
        </div>
        <div><br>
        </div>
        <div>// Remove existing custom state data</div>
        <div>
          <div>const CustomStateTy &Syms =
            state->get<CustomState>();<br>
          </div>
          <div> for (auto I = Syms.begin(), E = Syms.end(); I != E; ++I)
            {</div>
          <div>     SymbolRef Sym1 = *I;</div>
          <div>    state = state->remove<CustomState>(<wbr>Sym1);</div>
          <div> }</div>
          <div>state = state->add<CustomState>(Sym);  // Add
            the symbol that is needed for the current state</div>
        </div>
        <div><br>
        </div>
        <div>The idea was to remove custom state information from a
          state and then write the information (symbol) corresponding to
          that state. Thus I write the symbol to a state S and that
          creates a new state S1 with that symbol. S itself is not
          modified since states are immutable. Now, the state which
          succeeds S1 (which I call S2) also gets the same symbol
          through state propagation which should however not be
          associated with that state. Hence I try remove the symbol from
          S2 but it does not actually remove it from that S2 but creates
          a new state S3 with the symbol removed (due to the immutable
          nature of states).</div>
        <div><br>
        </div>
        <div>Finally, I would still be left with states such as S2 which
          has information which do not belong to them. Can I fix this in
          some way?</div>
        <div><br>
        </div>
        <div>Not sure if this is a requirement outside the support
          provided by the analyzer or I have created a requirement which
          is unnatural.</div>
        <div><br>
        </div>
        <div>Thanks.</div>
        <div><br>
        </div>
        <div>Regards,</div>
        <div>Venu.</div>
      </div>
      <div class="gmail_extra"><br>
        <div class="gmail_quote">On Thu, Feb 9, 2017 at 8:54 PM, Aleksei
          Sidorin <span dir="ltr"><<a href="mailto:a.sidorin@samsung.com" target="_blank">a.sidorin@samsung.com</a>></span>
          wrote:<br>
          <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
            <div bgcolor="#FFFFFF" text="#000000">
              <div class="m_-9191505789861700145m_-3091663750839211701moz-cite-prefix">Hello
                Venugopal,<br>
                <br>
                Unfortunately, there is no a simple way to get "symbol
                diff". Your approach with sequential iteration seems
                right to me in general.<br>
                About comparison of symbols. If you want just ensure
                that some symbols are same or different (like
                reg_$0<x> and reg_$1<y> which are
                different), you can just compare their pointers
                (SymbolRefs). Symbols are not modifiable, every symbol
                is allocated in the pool and lives here, SymbolRefs just
                point on it. If these pointers are different, symbols
                are different too, and equal otherwise.<br>
                <br>
                <br>
                09.02.2017 18:20, Aleksei Sidorin пишет:<br>
              </div>
              <blockquote type="cite">
                <div class="m_-9191505789861700145m_-3091663750839211701moz-cite-prefix">Hello
                  Venugopal,<br>
                  <br>
                  If you want just ensure that some symbols are same
                  (like reg_$0<x> and reg_$1<y>), you can
                  just compare their pointers (SymbolRefs). Symbols are
                  not modifiable, every symbol is allocated in the pool
                  and lives here, SymbolRefs just point on it. If these
                  pointers are different, symbols are different too, and
                  equal otherwise.<br>
                  <br>
                  <br>
                  09.02.2017 13:03, Venugopal Raghavan пишет:<br>
                </div>
                <div>
                  <div class="m_-9191505789861700145h5">
                    <blockquote type="cite">
                      <div dir="ltr">Hi,
                        <div><br>
                        </div>
                        <div>Apologies, but, I am back again. </div>
                        <div><br>
                        </div>
                        <div>I have two SymbolRef pointers (SymExpr *).
                          One SymbolRef is (reg_$0<x>) + 3$117.
                          The other SymbolRef is (reg_$0<x>) +
                          2$130. x is a variable in my program and these
                          SymbolRefs respresent an assignment of x + y
                          to a variable "a". y has the value 3 along one
                          path to the program point where "a" is
                          assigned and it has the value 2 along a second
                          path to the same point, hence the two
                          SymbolRefs differ in the constants.</div>
                        <div><br>
                        </div>
                        <div>I want to compare these two SymbolRefs and
                          find out where they differ. In this case, I
                          want to be able to say that they differ in the
                          constant value. I thought of using
                          symbol_iterator to iterate over each SymbolRef
                          or SymExpr * in lock-step fashion and find the
                          first point where it differs. But these is no
                          operator== defined in the SymExpr class and
                          hence I am unable to check the equality or
                          otherwise of two symbols in the SymbolRefs.</div>
                        <div><br>
                        </div>
                        <div>Is there a way to compare two SymbolRefs
                          and check for the differences? Otherwise, is
                          there a better way to check whether the
                          symbolic value at the same program point but
                          in two different program states are the same
                          or not, and if they are different, is there a
                          way to identify the difference? Maybe, my
                          approach of comparing two symbolic expressions
                          at a program point is not the right approach
                          in the first place.</div>
                        <div><br>
                        </div>
                        <div>Thanks.</div>
                        <div><br>
                        </div>
                        <div>Regards,</div>
                        <div>Venu.</div>
                      </div>
                      <div class="gmail_extra"><br>
                        <div class="gmail_quote">On Mon, Feb 6, 2017 at
                          2:42 PM, Venugopal Raghavan <span dir="ltr"><<a href="mailto:venur2005@gmail.com" target="_blank">venur2005@gmail.com</a>></span>
                          wrote:<br>
                          <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
                            <div dir="ltr">Hi Aleksei,
                              <div><br>
                              </div>
                              <div>Thanks. That seems to work.</div>
                              <div><br>
                              </div>
                              <div>Regards,</div>
                              <div>Venu.</div>
                            </div>
                            <div class="m_-9191505789861700145m_-3091663750839211701HOEnZb">
                              <div class="m_-9191505789861700145m_-3091663750839211701h5">
                                <div class="gmail_extra"><br>
                                  <div class="gmail_quote">On Mon, Feb
                                    6, 2017 at 2:05 PM, Aleksei Sidorin
                                    <span dir="ltr"><<a href="mailto:a.sidorin@samsung.com" target="_blank">a.sidorin@samsung.com</a>></span>
                                    wrote:<br>
                                    <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
                                      <div bgcolor="#FFFFFF" text="#000000">
                                        <div class="m_-9191505789861700145m_-3091663750839211701m_-1035519723042365625m_4390566528069532645moz-cite-prefix">Hello,<br>
                                          <br>
                                          On the point where PreStmt
                                          callbacks are called, the
                                          expression value is still not
                                          computed so the result of
                                          getSVal() is always UnknownVal
                                          and not a symbol. You should
                                          probably use PostStmt callback
                                          instead.<br>
                                          <br>
                                          <br>
                                          06.02.2017 08:21, Venugopal
                                          Raghavan пишет:<br>
                                        </div>
                                        <div>
                                          <div class="m_-9191505789861700145m_-3091663750839211701m_-1035519723042365625h5">
                                            <blockquote type="cite">
                                              <div dir="ltr">Hi Aleksei,
                                                <div><br>
                                                </div>
                                                <div>Thanks for the
                                                  reply. Unfortunately,
                                                  I am having further
                                                  trouble with my
                                                  checker
                                                  implementation. I have
                                                  the following code in
                                                  my checker (called
                                                  ConstantChecker):</div>
                                                <div><br>
                                                </div>
                                                <div>
                                                  <div> void
                                                    ConstantChecker::checkPreStmt(<wbr>const
                                                    Stmt *S,
                                                    CheckerContext
                                                    &C) const {</div>
                                                  <div>       
                                                    ProgramStateRef
                                                    state =
                                                    C.getState();</div>
                                                  <div>        const
                                                    LocationContext
                                                    *lctx =
                                                    C.getLocationContext();</div>
                                                  <div>        SVal val
                                                    =
                                                    state->getSVal(S,
                                                    lctx);</div>
                                                  <div>        SymbolRef
                                                    Sym =
                                                    val.getAsSymbol();
                                                      </div>
                                                </div>
                                                <div>        // Stmt 1</div>
                                                <div>                   
                                                    .</div>
                                                <div>                   
                                                    .</div>
                                                <div>                   
                                                    .</div>
                                                <div>}</div>
                                                <div>       </div>
                                                <div>My input test case
                                                  for the checker is
                                                  test1.c and I run the
                                                  command clang -cc1
                                                  -analyze
                                                  -analyzer-checker=optin.perfor<wbr>mance.PathSpecificConstants
                                                  test1.c where
                                                  PathSpecificConstants
                                                  is the name of my
                                                  checker:</div>
                                                <div><br>
                                                </div>
                                                <div>
                                                  <div>test(int x) {</div>
                                                  <div>   int y;</div>
                                                  <div>   int a;</div>
                                                  <div>   if (x > 0)
                                                    {</div>
                                                  <div>     y = 2;</div>
                                                  <div>   }</div>
                                                  <div>   else {</div>
                                                  <div>     y = 3;</div>
                                                  <div>   }</div>
                                                  <div>   a = x + y;</div>
                                                  <div>   printf("a =
                                                    %d\n", a);</div>
                                                  <div>}</div>
                                                </div>
                                                <div><br>
                                                </div>
                                                <div>When I print "Sym"
                                                  in gdb at the break
                                                  point Stmt 1, I always
                                                  get Sym as 0x0. This
                                                  probably means that
                                                  val is never a symbol
                                                  for my test case and
                                                  hence
                                                  val.getAsSymbol()
                                                  fails. I do not
                                                  understand this. I
                                                  would have thought
                                                  that at least the
                                                  expression x + y would
                                                  be represented by a
                                                  symbolic value such as
                                                  $0. I tried doing
                                                  const MemRegion *mem =
                                                  val.getAsRegion() also
                                                  at that  point and
                                                  tried to print out mem
                                                  in gdb. That also has
                                                  a value 0x0 except for
                                                  the printf statement.
                                                  I cannot understand
                                                  this too. I would have
                                                  expected variables
                                                  such as "x", "y" and
                                                  "a" to be associated
                                                  with a memory region
                                                  and hence mem to have
                                                  a non-null value at
                                                  least at the points
                                                  where y and a are
                                                  being assigned to.</div>
                                                <div><br>
                                                </div>
                                                <div>My plan was to use
                                                  Sym as the index into
                                                  a custom map that I
                                                  have created where I
                                                  am storing the values
                                                  of constants seen in
                                                  the test case. I am
                                                  unable to get this
                                                  plan working since Sym
                                                  is always 0x0.</div>
                                                <div><br>
                                                </div>
                                                <div>I have gone through
                                                  the Checker Developer
                                                  Manual. I am sorry to
                                                  be asking specific
                                                  questions about my
                                                  code in this fashion,
                                                  but, unfortunately, I
                                                  am stuck at this
                                                  point.</div>
                                                <div><br>
                                                </div>
                                                <div>Thanks.</div>
                                                <div><br>
                                                </div>
                                                <div>Regards,</div>
                                                <div>Venugopal Raghavan.</div>
                                              </div>
                                              <div class="gmail_extra"><br>
                                                <div class="gmail_quote">On
                                                  Wed, Feb 1, 2017 at
                                                  11:13 PM, Aleksei
                                                  Sidorin <span dir="ltr"><<a href="mailto:a.sidorin@samsung.com" target="_blank">a.sidorin@samsung.com</a>></span>
                                                  wrote:<br>
                                                  <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
                                                    <div bgcolor="#FFFFFF" text="#000000">
                                                      <div class="m_-9191505789861700145m_-3091663750839211701m_-1035519723042365625m_4390566528069532645m_4335525358519862662moz-cite-prefix">Hello
                                                        Venugopal,<br>
                                                        <br>
                                                        You will need to
                                                        extract all the
                                                        information from
                                                        ExplodedNodes.<br>
                                                        For example,
                                                        state is a part
                                                        of ExplodedNode.
                                                        So, you can
                                                        iterate over
                                                        ExplodedNodes of
                                                        graph using smth
                                                        like:<br>
                                                        for (auto Iter =
                                                        G.nodes_begin(),
                                                        E =
                                                        G.nodes_end(); I
                                                        != E; ++I) {<br>
                                                         
                                                        ProgramStateRef
                                                        State =
                                                        I->getState();<br>
                                                          // Do the
                                                        stuff with State<br>
                                                        }<br>
                                                        <br>
                                                        <br>
                                                        <br>
                                                        <br>
                                                        01.02.2017
                                                        12:19, Venugopal
                                                        Raghavan пишет:<br>
                                                      </div>
                                                      <div>
                                                        <div class="m_-9191505789861700145m_-3091663750839211701m_-1035519723042365625m_4390566528069532645h5">
                                                          <blockquote type="cite">
                                                          <div dir="ltr">Hi,
                                                          <div><br>
                                                          </div>
                                                          <div>I am
                                                          registering my
                                                          own map in the
                                                          program state
                                                          using the the
                                                          following:</div>
                                                          <div><br>
                                                          </div>
                                                          <div>REGISTER_MAP_WITH_PROGRAMSTATE<wbr>(ConstantMap,
                                                          SymbolRef,
                                                          VariableConstVal)<br>
                                                          </div>
                                                          <div><br>
                                                          </div>
                                                          <div>where
                                                          VariableConstVal
                                                          is the
                                                          structure
                                                          containing the
                                                          information I
                                                          want in this
                                                          map. </div>
                                                          <div><br>
                                                          </div>
                                                          <div>I am
                                                          populating
                                                          this map in
                                                          the
                                                          callback checkPostStmt()
                                                          using state =
state->set<ConstantMap>(sym, ...) while the state graph is
                                                          being
                                                          constructed.</div>
                                                          <div><br>
                                                          </div>
                                                          <div>At the
                                                          end of
                                                          analysis, I
                                                          want to now
                                                          read the
                                                          information
                                                          stored in this
                                                          map in the
                                                          callback checkEndAnalysis(Expl<wbr>odedGraph
                                                          &G,
                                                          BugReporter
                                                          &B,
                                                          ExprEngine
                                                          &Eng).
                                                          However, I am
                                                          not sure how
                                                          to get the
                                                          SymbolRef
                                                          associated
                                                          with an
                                                          ExplodedNode
                                                          which is what
                                                          I get when I
                                                          iterate over
                                                          the
                                                          ExplodedGraph
                                                          at the end of
                                                          the analysis.</div>
                                                          <div><br>
                                                          </div>
                                                          <div>How can I
                                                          get the
                                                          SymbolRef that
                                                          I can use to
                                                          index into my
                                                          map? In
                                                          checkPostStmt(stmt*
                                                          S,
                                                          CheckerContext
                                                          &C), I
                                                          used the
                                                          following code
                                                          to get the
                                                          SymbolRef that
                                                          I can use to
                                                          store the
                                                          information in
                                                          the map:</div>
                                                          <div><br>
                                                          </div>
                                                          <div>
                                                          <div>  SVal
                                                          val =
                                                          state->getSVal(S,
                                                          lctx);</div>
                                                          <div> 
                                                          SymbolRef Sym
                                                          =
                                                          val.getAsSymbol();</div>
                                                          </div>
                                                          <div><br>
                                                          </div>
                                                          <div>but in
                                                          checkEndAnalysis(ExplodedGraph
                                                          &G,
                                                          BugReporter
                                                          &B,
                                                          ExprEngine
                                                          &Eng) I do
                                                          not seem to
                                                          have a handle
                                                          to stmt* to
                                                          get the SVal.</div>
                                                          <div><br>
                                                          </div>
                                                          <div>I guess
                                                          my question is
                                                          probably not
                                                          phrased very
                                                          well, but I
                                                          hope some one
                                                          can make some
                                                          sense out of
                                                          it. Also, I
                                                          guess I have a
                                                          long way to go
                                                          before I
                                                          understand the
                                                          data
                                                          structures in
                                                          the analyzer
                                                          well. I
                                                          checked the
                                                          other
                                                          checkers, but
                                                          none of them
                                                          seem to
                                                          exhibit
                                                          exactly my
                                                          requirement.</div>
                                                          <div><br>
                                                          </div>
                                                          <div>Thanks.</div>
                                                          <div><br>
                                                          </div>
                                                          <div>Regards,</div>
                                                          <div>Venugopal
                                                          Raghavan.</div>
                                                          </div>
                                                          <div class="gmail_extra"><br>
                                                          <div class="gmail_quote">On
                                                          Wed, Jan 25,
                                                          2017 at 3:19
                                                          PM, Venugopal
                                                          Raghavan <span dir="ltr"><<a href="mailto:venur2005@gmail.com" target="_blank">venur2005@gmail.com</a>></span>
                                                          wrote:<br>
                                                          <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
                                                          <div dir="ltr">Hi
                                                          Aleksei,
                                                          <div><br>
                                                          </div>
                                                          <div>Thanks. I
                                                          will check
                                                          this.</div>
                                                          <div><br>
                                                          </div>
                                                          <div>Regards,</div>
                                                          <div>Venu.</div>
                                                          </div>
                                                          <div class="m_-9191505789861700145m_-3091663750839211701m_-1035519723042365625m_4390566528069532645m_4335525358519862662HOEnZb">
                                                          <div class="m_-9191505789861700145m_-3091663750839211701m_-1035519723042365625m_4390566528069532645m_4335525358519862662h5">
                                                          <div class="gmail_extra"><br>
                                                          <div class="gmail_quote">On
                                                          Wed, Jan 25,
                                                          2017 at 3:15
                                                          PM, Aleksei
                                                          Sidorin <span dir="ltr"><<a href="mailto:a.sidorin@samsung.com" target="_blank">a.sidorin@samsung.com</a>></span>
                                                          wrote:<br>
                                                          <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
                                                          <div bgcolor="#FFFFFF" text="#000000">
                                                          <div class="m_-9191505789861700145m_-3091663750839211701m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944m_8180934762430575759moz-cite-prefix">Hello
                                                          Venugopal,<br>
                                                          <br>
                                                          During
                                                          analysis, you
                                                          have access to
                                                          a single path
                                                          only. But
                                                          after the
                                                          analysis is
                                                          done, you can
                                                          summarize
                                                          information
                                                          across
                                                          different
                                                          paths using
                                                          checkEndAnalysis()
                                                          callback. You
                                                          will get full
                                                          ExplodedGraph
                                                          built for the
                                                          function so
                                                          you will be
                                                          able to look
                                                          into its every
                                                          node.<br>
                                                          <br>
                                                          <br>
                                                          25.01.2017
                                                          09:25,
                                                          Venugopal
                                                          Raghavan via
                                                          cfe-dev пишет:<br>
                                                          </div>
                                                          <blockquote type="cite">
                                                          <div>
                                                          <div class="m_-9191505789861700145m_-3091663750839211701m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944h5">
                                                          <div dir="ltr">Hi,
                                                          <div><br>
                                                          </div>
                                                          <div>Firstly,
                                                          apologies for
                                                          the long email
                                                          below.</div>
                                                          <div><br>
                                                          </div>
                                                          <div>I am new
                                                          to the Clang
                                                          Static
                                                          Analyzer
                                                          (CLA). My
                                                          interest in
                                                          CLA was more
                                                          to see if I
                                                          can solve
                                                          quickly
                                                          path-sensitive
                                                          data-flow
                                                          analysis
                                                          problems than
                                                          as a vehicle
                                                          to build
                                                          bug-finding
                                                          checkers. I
                                                          needed the
                                                          solutions to
                                                          such data flow
                                                          problems to
                                                          extract some
                                                          behavioral
                                                          properties
                                                          from some test
                                                          cases I have.
                                                          For example,
                                                          consider the
                                                          following
                                                          piece of code:</div>
                                                          <div><br>
                                                          </div>
                                                          <div>if (cond)
                                                          {</div>
                                                          <div>   x = 4;</div>
                                                          <div>}</div>
                                                          <div>else {</div>
                                                          <div>   x = 5;</div>
                                                          <div>}</div>
                                                          <div><br>
                                                          </div>
                                                          <div>L: .... =
                                                          ...x..; // Use
                                                          of variable x</div>
                                                          <div><br>
                                                          </div>
                                                          <div>I want to
                                                          identify
                                                          program
                                                          locations such
                                                          as "L" in the
                                                          code above
                                                          where x is not
                                                          a constant if
                                                          you aggregate
                                                          data-flow
                                                          information
                                                          across paths,
                                                          but, on the
                                                          other hand, is
                                                          actually a
                                                          constant if
                                                          you have
                                                          path-specific
                                                          data flow
                                                          information.
                                                          Since CFA does
                                                          path-specific
                                                          analysis, I
                                                          was curious to
                                                          know if it
                                                          would help me
                                                          with such
                                                          tasks. The
                                                          "bug-report" I
                                                          want at
                                                          location L is
                                                          that x has a
                                                          value 4, given
                                                          the path
                                                          constraint for
                                                          the path
                                                          including the
                                                          "then-path" of
                                                          the if
                                                          statement and
                                                          that x has a
                                                          value 5 along
                                                          the else-path.</div>
                                                          <div><br>
                                                          </div>
                                                          <div>I started
                                                          writing a
                                                          checker to
                                                          accomplish the
                                                          above task,
                                                          but was
                                                          quickly
                                                          blocked by
                                                          some basic
                                                          doubts. My
                                                          rough plan for
                                                          the checker
                                                          was to
                                                          maintain a map
                                                          in
                                                          ProgramState
                                                          which maps
                                                          ProgramPoints
                                                          (or, maybe
                                                          program
                                                          symbols) to
                                                          constants when
                                                          those
                                                          variables
                                                          indeed have
                                                          constant
                                                          values at the
                                                          ProgramPoint.
                                                          For example,
                                                          when CFA
                                                          expands states
                                                          along the
                                                          then-path and
                                                          reaches "L",
                                                          my map would
                                                          say that at
                                                          ProgramPoint
                                                          "L", variable
                                                          x has a
                                                          constant value
                                                          4. Then, when
                                                          CFA expands
                                                          nodes along
                                                          the else-path,
                                                          I guess it
                                                          would again
                                                          create a state
                                                          corresponding
                                                          to L which now
                                                          says that x
                                                          has the
                                                          constant value
                                                          5. I want to
                                                          be able to
                                                          catch this
                                                          scenario where
                                                          the same
                                                          variable at
                                                          the same
                                                          ProgramPoint
                                                          has two
                                                          different
                                                          constant
                                                          values
                                                          depending on
                                                          the path
                                                          taken.</div>
                                                          <div><br>
                                                          </div>
                                                          <div>However,
                                                          the issue is
                                                          that, when the
                                                          state graph
                                                          along the
                                                          else-path is
                                                          expanded, it
                                                          would no
                                                          longer have
                                                          any of the map
                                                          contents that
                                                          was built
                                                          along the
                                                          disjoint
                                                          then-path. How
                                                          then can I get
                                                          access to the
                                                          then-path
                                                          information
                                                          when I am
                                                          expanding the
                                                          path along the
                                                          else-path?
                                                          Since the
                                                          checker is
                                                          also required
                                                          to be
                                                          stateless, I
                                                          cannot
                                                          maintain
                                                          auxiliary
                                                          information in
                                                          the checker
                                                          that is
                                                          persistent
                                                          across
                                                          multiple calls
                                                          to the
                                                          call-back
                                                          function. </div>
                                                          <div><br>
                                                          </div>
                                                          <div>Can you
                                                          help me with
                                                          this question?
                                                          Maybe, I am
                                                          trying to use
                                                          CFA in ways it
                                                          was not meant
                                                          to be used
                                                          viz. as a
                                                          vehicle to
                                                          solve data
                                                          flow problems
                                                          which consults
                                                          information
                                                          cutting across
                                                          paths. Maybe,
                                                          the CFA is
                                                          meant to
                                                          handle
                                                          problems which
                                                          require the
                                                          examination of
                                                          information
                                                          restricted to
                                                          single paths.
                                                          Is that the
                                                          case? Or, am I
                                                          missing
                                                          something?</div>
                                                          <div><br>
                                                          </div>
                                                          <div>Thanks.</div>
                                                          <div><br>
                                                          </div>
                                                          <div>Regards,</div>
                                                          <div>Venugopal
                                                          Raghavan.</div>
                                                          </div>
                                                          <br>
                                                          <fieldset class="m_-9191505789861700145m_-3091663750839211701m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944m_8180934762430575759mimeAttachmentHeader"></fieldset>
                                                          <br>
                                                          </div>
                                                          </div>
                                                          <pre>______________________________<wbr>_________________
cfe-dev mailing list
<a class="m_-9191505789861700145m_-3091663750839211701m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944m_8180934762430575759moz-txt-link-abbreviated" href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a>
<a class="m_-9191505789861700145m_-3091663750839211701m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944m_8180934762430575759moz-txt-link-freetext" href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" target="_blank">http://lists.llvm.org/cgi-bin/<wbr>mailman/listinfo/cfe-dev</a><span class="m_-9191505789861700145m_-3091663750839211701m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944HOEnZb"><font color="#888888">
</font></span></pre><span class="m_-9191505789861700145m_-3091663750839211701m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944HOEnZb"><font color="#888888">
    </font></span></blockquote><span class="m_-9191505789861700145m_-3091663750839211701m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944HOEnZb"><font color="#888888">
    

    <p>

    </p>
    <pre class="m_-9191505789861700145m_-3091663750839211701m_-1035519723042365625m_4390566528069532645m_4335525358519862662m_-1222624000317224944m_8180934762430575759moz-signature" cols="72">-- 
Best regards,
Aleksei Sidorin,
SRR, Samsung Electronics
</pre>
  </font></span></div>

</blockquote></div>
</div>
</div></div></blockquote></div>
</div>



</blockquote>
<p>
</p><pre class="m_-9191505789861700145m_-3091663750839211701m_-1035519723042365625m_4390566528069532645m_4335525358519862662moz-signature" cols="72">-- 
Best regards,
Aleksei Sidorin,
SRR, Samsung Electronics
</pre></div></div></div>
</blockquote></div>
</div>



</blockquote>
<p>
</p><pre class="m_-9191505789861700145m_-3091663750839211701m_-1035519723042365625m_4390566528069532645moz-signature" cols="72">-- 
Best regards,
Aleksei Sidorin,
SRR, Samsung Electronics
</pre></div></div></div>
</blockquote></div>
</div>
</div></div></blockquote></div>
</div>



</blockquote>
<p>
</p><pre class="m_-9191505789861700145m_-3091663750839211701moz-signature" cols="72">-- 
Best regards,
Aleksei Sidorin,
SRR, Samsung Electronics
</pre>


</div></div></blockquote><div><div class="m_-9191505789861700145h5">
<p>
</p><pre class="m_-9191505789861700145m_-3091663750839211701moz-signature" cols="72">-- 
Best regards,
Aleksei Sidorin,
SRR, Samsung Electronics
</pre></div></div></div>
</blockquote></div>
</div>



</blockquote>
<p>
</p><pre class="m_-9191505789861700145moz-signature" cols="72">-- 
Best regards,
Aleksei Sidorin,
SRR, Samsung Electronics
</pre></div></div></div>
</blockquote></div><br></div>