<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="">In any case, the float modeling present in a patch seems quite incomplete.<div class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Oct 4, 2017, at 12:31 PM, George Karpenkov <<a href="mailto:ekarpenkov@apple.com" class="">ekarpenkov@apple.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><meta http-equiv="Content-Type" content="text/html; charset=utf-8" class=""><div 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 class=""><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></div></div></blockquote></div><br class=""></div></body></html>