<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Hi Julian,<div class=""><br class=""></div><div class="">I think you would need to recompile Clang+LLVM yourself to do that (it’s not very difficult, the documentation is pretty good).</div><div class="">Then you would need to make sure that CMake during the configuration pass can find Z3, there’s a corresponding variable you need to</div><div class="">set (I don’t remember which one though, but I think it would be trivial to find).</div><div class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Oct 4, 2017, at 7:29 AM, Julian Löffler <<a href="mailto:loefflju@informatik.uni-freiburg.de" class="">loefflju@informatik.uni-freiburg.de</a>> wrote:</div><br class="Apple-interchange-newline"><div class="">
  
    <meta http-equiv="Content-Type" content="text/html; charset=utf-8" class="">
  
  <div text="#000000" bgcolor="#FFFFFF" class="">
    Hi George,<br class="">
    <br class="">
    <br class="">
    How is the z3 mode enabled tho?<br class="">
    If I download the latest release binaries:
    <a class="moz-txt-link-freetext" href="http://releases.llvm.org/download.html#5.0.0">http://releases.llvm.org/download.html#5.0.0</a><br class="">
    <br class="">
    and run e.g :<br class="">
    clang-5.0 -cc1 -w -analyze -DANALYZER_CM_Z3 -analyzer-constraints=z3
    -analyzer-checker=core,debug.ExprInspection <br class="">
    <br class="">
    I'll get an error: <br class="">
    fatal error: error in backend: Clang was not compiled with Z3
    support!<br class="">
    <br class="">
    <br class="">
    Kind regards, <br class="">
    Julian<br class="">
    <br class="">
    <br class="">
    <br class="">
    <div class="moz-cite-prefix">On 03/10/2017 00:21, George Karpenkov
      wrote:<br class="">
    </div>
    <blockquote type="cite" cite="mid:019A78FE-3B1F-4033-95C0-EE931AE59D4C@apple.com" class="">
      <meta http-equiv="Content-Type" content="text/html; charset=utf-8" class="">
      (re-adding cfe-dev)
      <div class=""><br class="">
      </div>
      <div class="">Hi Julian,</div>
      <div class=""><br class="">
      </div>
      <div class="">Artem’s reply above in this thread indicates that
        currently float modeling is not performed:</div>
      <div class=""><br class="">
      </div>
      <div class="">> Finally, the analyzer isn't conducting symbolic
        floating-point arithmetic at all yet, only integers. A step in
        the direction of improving it can be found in <a href="https://reviews.llvm.org/D28954" class="" moz-do-not-send="true">https://reviews.llvm.org/D28954</a> .</div>
      <div class=""><br class="">
      </div>
      <div class="">You might have more luck using Z3-mode and the
        mentioned patch.</div>
      <div class=""><br class="">
      </div>
      <div class="">George</div>
      <div class="">
        <div class=""><br class="">
          <blockquote type="cite" class="">
            <div class="">On Sep 25, 2017, at 8:50 AM, Julian Löffler
              <<a href="mailto:loefflju@informatik.uni-freiburg.de" class="" moz-do-not-send="true">loefflju@informatik.uni-freiburg.de</a>>
              wrote:</div>
            <br class="Apple-interchange-newline">
            <div class="">
              <div class="">Hey there,<br class="">
                <br class="">
                What is strange to me, that Clang/scanbuild does not
                recognize the following:<br class="">
                <br class="">
                Program:<br class="">
                <br class="">
                #include <math.h><br class="">
                <br class="">
                extern void clang_analyzer_warnIfReached();<br class="">
                <br class="">
                int main(){<br class="">
                  float x = NAN;<br class="">
                  // NAN == NAN --> False.<br class="">
                  if(x == x){<br class="">
                     clang_analyzer_warnIfReached();<br class="">
                  }<br class="">
                }<br class="">
                <br class="">
                The clang_analyzer_warnIfReached() should not be
                reachable, but is reachable.<br class="">
                <br class="">
                <br class="">
                On 19/09/2017 19:03, George Karpenkov wrote:<br class="">
                <blockquote type="cite" class="">Hi Julian,<br class="">
                  <br class="">
                  <blockquote type="cite" class="">On Sep 19, 2017, at
                    3:43 AM, Julian Löffler <<a href="mailto:loefflju@informatik.uni-freiburg.de" class="" moz-do-not-send="true">loefflju@informatik.uni-freiburg.de</a>>
                    wrote:<br class="">
                    <br class="">
                    Hey George,<br class="">
                    <br class="">
                    Thanks a lot for the additional information.<br class="">
                    <br class="">
                    Using prototypes works as expected I think.<br class="">
                    <br class="">
                    However, do you think clang is a good tool to
                    analyze reachability of certain program-points?<br class="">
                    <br class="">
                    Currently we model requirements of a math-lib in the
                    form of small programs for each function, where we
                    analyze if we can reach error-states. (i.e. states
                    where the requirement can be injured). The question
                    is if we should rather use Clang  on the source
                    code.<br class="">
                  </blockquote>
                  Clang static analyzer is neither sound, nor complete,
                  so you will not be able to verify<br class="">
                  that a certain program point is definitely not
                  reachable.<br class="">
                  There are many sources of imprecision: functions are
                  inlined only if they are smaller than a certain size,<br class="">
                  program is analyzed one translation unit at a time,
                  and many others.<br class="">
                  <br class="">
                  However, unlike more academic tools clang static
                  analyzer<br class="">
                  gives you a push-button technology: you can just run
                  it on an *arbitrary* codebase, and in a very timely
                  manner<br class="">
                  get a list of found bugs.<br class="">
                  As far as I am aware that would be very difficult to
                  achieve with e.g. Ultimate Atomizer and similar tools.<br class="">
                  <br class="">
                  <blockquote type="cite" class="">Usually we do that
                    using trace abstraction and abstract interpretation,
                    anyway I did not find a hint what clang static
                    analyzer is doing exactly.<br class="">
                    So if you have a clue which analysis-methods Clang
                    static analyzer uses, I'd be glad to hear it^^<br class="">
                  </blockquote>
                  I believe it would be closest to symbolic execution.<br class="">
                  <br class="">
                  George<br class="">
                  <br class="">
                  <blockquote type="cite" class=""><br class="">
                    Thanks a lot and kind regards,<br class="">
                    <br class="">
                    Julian<br class="">
                    <br class="">
                    <br class="">
                    On 19.09.2017 03:02, George Karpenkov wrote:<br class="">
                    <blockquote type="cite" class="">Hi Julian,<br class="">
                      <br class="">
                      Artem has mentioned a few good points, to that I
                      would like to add that:<br class="">
                      <br class="">
                      a) Using uninitialized values as non-det inputs
                      from the user like CBMC<br class="">
                      does is usually not a good thing to do, as
                      uninitialized values are not simply<br class="">
                      non-deterministic, and can cause undefined
                      behavior.<br class="">
                      <br class="">
                      b) In order to get Clang static analyzer to model
                      non-deterministic input from user<br class="">
                      it is enough to define a function prototype
                      without implementation which would return<br class="">
                      desired type.<br class="">
                      <br class="">
                      Regards,<br class="">
                      George<br class="">
                      <br class="">
                      <blockquote type="cite" class="">On Sep 16, 2017,
                        at 7:07 AM, Julian Löffler via cfe-dev <<a href="mailto:cfe-dev@lists.llvm.org" class="" moz-do-not-send="true">cfe-dev@lists.llvm.org</a>>
                        wrote:<br class="">
                        <br class="">
                        Greetings,<br class="">
                        <br class="">
                        I wonder how one can obtain that Clang Static
                        Analyzer recognizes non-deterministic-floats.<br class="">
                        <br class="">
                        Usually you can simulate them in c as follows:<br class="">
                        <br class="">
                        float nondet_float(){<br class="">
                            float x;<br class="">
                            return x;<br class="">
                        }<br class="">
                        <br class="">
                        float myFloat = nondet_float();<br class="">
                        <br class="">
                        Such that tools like CBMC will handle such
                        variables as non-det floats, which are assumed
                        to be every possible value.<br class="">
                        <br class="">
                        Is that behavior somehow possible in Clang
                        Static Analyzer?<br class="">
                        Or is it generally impossible for Static code
                        analyzers to do such things?<br class="">
                        <br class="">
                        Regards,<br class="">
                        Julian<br class="">
                        _______________________________________________<br class="">
                        cfe-dev mailing list<br class="">
                        <a href="mailto:cfe-dev@lists.llvm.org" class="" moz-do-not-send="true">cfe-dev@lists.llvm.org</a><br class="">
<a class="moz-txt-link-freetext" href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev">http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a><br class="">
                      </blockquote>
                    </blockquote>
                  </blockquote>
                </blockquote>
                <br class="">
              </div>
            </div>
          </blockquote>
        </div>
        <br class="">
      </div>
    </blockquote>
    <br class="">
  </div>

</div></blockquote></div><br class=""></div></body></html>