<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=utf-8">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    <p>As for casts, can you point me to the current code in the
      analyzer that ignores them? Does the following method possibly
      work?</p>
    <p>I introduce another method or a few methods that handle cast
      operations and use them when I process integer expressions. Or
      ideally using one or few default parameters to control if the
      casts should be ignored (the default), so that handling casts
      doesn't disturb the existing solver and checkers.</p>
    <p>Also, I think that I still need to change the current solver not
      to discard constraints involving multiple symbols.</p>
    <p>Is this a practical investigation work? What other issues and
      places should I pay attention to, and what's the best steps to
      start with?</p>
    <br>
    <pre class="moz-signature" cols="72">Thanks,
Lou
 </pre>
    <div class="moz-cite-prefix">On 09/14/2018 05:17 PM, Artem Dergachev
      wrote:<br>
    </div>
    <blockquote type="cite"
      cite="mid:25ee088a-ab7c-8cd9-829c-de757bb6c354@gmail.com">
      <meta http-equiv="Content-Type" content="text/html; charset=utf-8">
      <br>
      Also for integer overflows you may encounter a completely
      different problem that is currently in a worse shape than
      constraint solving, and it's integral cast representation. Static
      analyzer currently models casts by ignoring them, so the solver
      doesn't ever get a hold on this information. You'll need to lift
      this restriction, but it'll immediately upset the existing solver
      and a lot of other entities in the analyzer, so you'll have to
      make them prepared for seeing casted symbols. This may involve
      implementing the trick i mentioned above in all checkers, because
      otherwise many checkers will fail to find most of their bugs.<br>
      <br>
      <blockquote type="cite"
        cite="mid:06c73b46-402a-66e9-313c-08c96b51867e@gmail.com">
        <p><font size="+1"> I can rephrase this to taint propagation and
            integer expression by saying that an expression involving a
            tainted value is likely to cause integer overflow. What is
            the best way to implement this checker if I use this
            strategy? I've noticed that there is a taint propagation
            checker but haven't figured out how to use it in another
            checker. Is there any example code that uses it?<br>
          </font></p>
      </blockquote>
    </blockquote>
    <blockquote type="cite"
      cite="mid:25ee088a-ab7c-8cd9-829c-de757bb6c354@gmail.com"><br>
      In other words, taint problems are "per-path" "may" problems,
      while normal problems are "per-path" "must" problems. And for that
      purpose the existing refutation scheme is enough to solve all the
      problems. You still have problems with casts though.<br>
    </blockquote>
    <br>
  </body>
</html>