<div dir="ltr">Hi all,<div><br></div><div>This is my first report to the community, comparing the results with and without the Z3 refutation when analyzing a number of projects.</div><div><br></div><div>~</div><div><br></div><div>First of all, I'd like to thank Réka Kovács as the first version of the refutation using Z3 was created by her (<a href="https://reviews.llvm.org/D45517">https://reviews.llvm.org/D45517</a>)! Thank you very much!</div><div><br></div><div>After applying patch D45517, you can use the refutation check by using -analyzer-config crosscheck-with-z3=true. Obviously, you need a version of clang built with Z3.</div><div><br></div><div>~</div><div><br></div><div>I'm currently analyzing 7 C projects (unfortunately, there's a bug preventing us from analyzing FFmpeg):</div><div><br></div><div>1. Tmux</div><div>2. Redis </div><div>3. OpenSSL</div><div>4. Twin</div><div>5. Git</div><div>6. Postgresql</div><div>7. Sqlite3</div><div><br></div><div>In short, the refutation check slows down the verification by ~20%. It removed 6 FPs from Redis, 6 FPs from git and 1 FP from Sqlite3 (FP means false positive). Surprisingly enough, some analysis were faster with the crosscheck, but I'm not sure why (maybe ccache?).</div><div><br></div><div>Attached is a spreadsheet (report1.ods) with some number (total time, average time per check, # of reported bugs) and a txt with all the raw data from the analysis (raw.txt). I'll add these data to google drive for the next report.</div><div><br></div><div>In order to generate the raw data, you need to use a version of clang with assertions enabled, call scan-build.py with '-analyzer-config serialize-stats=true' and you need to apply patch <a href="https://reviews.llvm.org/D43134">https://reviews.llvm.org/D43134</a>.</div><div><br></div><div>Thank you very much,</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">2018-05-01 15:27 GMT+01:00 Mikhail Ramalho <span dir="ltr"><<a href="mailto:mikhail.ramalho@gmail.com" target="_blank">mikhail.ramalho@gmail.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Hello all,<div><br></div><div>My proposal for GSoC 2018 [0] about Bug Validation in the Clang Static Analyzer using the Z3 SMT Solver was accepted.</div><div><br></div><div>I'll work with George Karpenkov to improve the bug reports that the static analyzer produces by reducing the number of false bugs.</div><div><br></div><div>Thank you,</div><div><br></div><div>[0] <a href="https://docs.google.com/document/d/1-zNSv0l4WyoxYpJUAw8LFnQq_TY4AGjIpPu1VPkmO-g" target="_blank">https://docs.google.com/do<wbr>cument/d/1-zNSv0l4WyoxYpJUAw8L<wbr>FnQq_TY4AGjIpPu1VPkmO-g</a><span class="gmail-HOEnZb"><font color="#888888"><br clear="all"><div><br></div>-- <br><div class="gmail-m_1835488271327190244m_-1529477061806271292gmail_signature"><div dir="ltr"><div><br></div><div>Mikhail Ramalho.</div></div></div>
</font></span></div></div>
</blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><br></div><div>Mikhail Ramalho.</div></div></div>
</div>