<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="">(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="">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><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="">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="">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="">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="">cfe-dev@lists.llvm.org</a><br class="">http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev<br class=""></blockquote></blockquote></blockquote></blockquote><br class=""></div></div></blockquote></div><br class=""></div></body></html>