
<html>

  <head>

    <meta content="text/html; charset=utf-8" http-equiv="Content-Type">

  </head>

  <body text="#000000" bgcolor="#FFFFFF">

    On 31.03.2016 20:20, Gábor Horváth wrote:<br>

    <blockquote

cite="mid:CAPRL4a04YGdY9n61C37xqvU730z1D-4jTo1LZcUH3wiJE40K5Q@mail.gmail.com"

      type="cite">

      <div dir="ltr"><br>

        <div class="gmail_extra">

          <div class="gmail_quote">

            <blockquote class="gmail_quote" style="margin:0px 0px 0px

              0.8ex;border-left:1px solid

              rgb(204,204,204);padding-left:1ex">

              <div text="#000000" bgcolor="#FFFFFF"><span class=""></span>

                Yeah, i guess it works pretty much as expected. In the

                out-of-context analysis, we have two branches for foo(),

                depending on range constraints for symbol

                'reg_$0<x> == reg_$0<y>' - in one branch

                it's [0, 0], in the other branch it's [1, something like

                BOOL_MAX]. When calling foo(&a, &a) from bar(),

                reg_$0<x> gets renamed to &a (as integer),

                reg_$0<y> gets renamed to &a (as integer) (i

                don't remember if we still keep the SymbolRegionAddress

                thing around, because i wanted to replace it with the

                correct nonloc::LocAsInteger eventually, as it seems

                more correct; it is more difficult to work with, but

                imho it is "the" correct actualization), and finally the

                whole symbol gets renamed to '&a (as integer) !=

                &a (as integer)' and collapses to 0 during

                evalBinOp, but because range [0, 0] of 0 does not

                intersect with [1, something like BOOL_MAX], this branch

                is discarded as unreachable. So when applying summary

                in-context we have only one branch.<span class=""><br>

                </span></div>

            </blockquote>

            <div><br>

            </div>

            <div>That is great!<br>

              <br>

            </div>

            <div>What I wanted to emphasize here, do we still get only

              one branch for `<span class="">if (b == &a) {}`?

                Because that condition can be decided regardless of the

                context. </span></div>

          </div>

        </div>

      </div>

    </blockquote>

    <br>

    Yeah, sure, the out-of-context analysis for summary construction is,

    in most senses, just your normal analysis; we may just record stuff

    along the way, but not make significantly different decisions. If

    the condition is resolvable without context, it will be resolved

    without context, just like during normal analysis. So the function

    in your example has exactly two branches.<br>

  </body>

</html>