<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    <br>
    <br>
    <div class="moz-cite-prefix">On 4/24/18 4:54 PM, Timothy J. Wood
      wrote:<br class="">
    </div>
    <blockquote type="cite"
      cite="mid:D0EA63EF-64FB-4E5F-B4F3-9733E5630CA6@omnigroup.com">
      <div>
        <blockquote type="cite" class="">
          <div class="">On Apr 24, 2018, at 4:44 PM, Artem Dergachev
            <<a href="mailto:noqnoqneo@gmail.com" class=""
              moz-do-not-send="true">noqnoqneo@gmail.com</a>> wrote:</div>
          <br class="Apple-interchange-newline">
          <div class="">
            <div class="">Hmm, ok, the problem may also be there:<br
                class="">
              <br class="">
              <blockquote type="cite" class="">(void)outError; // Added
                as a precaution in reference to <<a
                  href="http://lists.llvm.org/pipermail/cfe-dev/2017-April/053510.html"
                  class="" moz-do-not-send="true">http://lists.llvm.org/pipermail/cfe-dev/2017-April/053510.html</a>><br
                  class="">
              </blockquote>
              <br class="">
              Because in this case you're still doing your check *after*
              the precaution code which is the last use of the variable.<br
                class="">
              <br class="">
              You might want to move (or rather duplicate) your check
              into checkDeadSymbols(). Because once the symbol is dead,
              there's no way the program would be able to constrain it
              or initialize the memory it points to. So you can warn
              immediately when the symbol is dead, based on the
              information that's already available, assuming that we're
              still within the function of interest.<br class="">
              <br class="">
              I believe that the check in checkEndFunction is still
              necessary in case the function of interest is also inlined
              during analysis, because in this case the symbol may
              remain alive for a separate reason (still referenced by
              the caller).<br class="">
              <br class="">
              Note - this is a guess, i didn't actually look at how it
              works. The easiest way for you to understand that is to
              dump the "exploded graph" and see everything for yourself,
              as explained in <a
href="http://clang-analyzer.llvm.org/checker_dev_manual.html#visualizing"
                class="" moz-do-not-send="true">http://clang-analyzer.llvm.org/checker_dev_manual.html#visualizing</a><br
                class="">
            </div>
          </div>
        </blockquote>
        <div><br class="">
        </div>
      </div>
      <br class="">
      <div class="">I was guessing that the `outError` would never go
        out of scope since it is a parameter, but I guess I don’t know
        for sure that it wouldn’t do so as you suggest. I was starting
        to guess that the constraint might only be valid inside the two
        arms of the `if` but that might be misguided.</div>
    </blockquote>
    <br>
    The constraint definitely is supposed to remain after the `if`.
    That's the whole point of the analyzer. That's essentially the
    difference between the exploded graph and your usual CFG.<br>
    <br>
    The constraint itself may disappear when the program no longer
    references the constrained symbol, but the two analysis paths are
    not merged until they lead to (program state, program point) pairs
    that are actually exactly identical in every possible aspect.<br>
    <br>
    <blockquote type="cite"
      cite="mid:D0EA63EF-64FB-4E5F-B4F3-9733E5630CA6@omnigroup.com">
      <div class="">Implementing the `evalAssume` call back, I can that
        it does mark outError a couple times as well, so that’d be a
        second option if checkDeadSymbols doesn’t pan out.</div>
    </blockquote>
    <br>
    I still strongly encourage you to have a look at the exploded graph.
    It'll immediately explain the whole analysis step-by-step to you and
    show you everything that's available on every step and you won't
    have to blindly experiment with random callbacks anymore. Please ask
    if you'll have problems understanding it.<br>
    <br>
    <blockquote type="cite"
      cite="mid:D0EA63EF-64FB-4E5F-B4F3-9733E5630CA6@omnigroup.com">
      <div class=""><br class="">
      </div>
      <div class="">Thanks, this gives me a couple paths to try.</div>
      <div class=""><br class="">
      </div>
      <div class="">-tim</div>
      <div class=""><br class="">
      </div>
    </blockquote>
    <br>
  </body>
</html>