<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 Réka,<div class=""><br class=""></div><div class=""><div><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:12.8px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial" class=""><div class=""><div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:12.8px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial" class="">I was thinking about whether the whole ExplodedGraph needs to be re-built if we want to post-process bugs occured in its realm.</div></div></div></div></div></blockquote><div><br class=""></div><div><div class="">Generally all of post-processing is done in the `BugReporterVisitors.cpp` file,</div><div class="">with general entry point being `trackNullOrUndefValue` function for many checkers.</div><div class=""><br class=""></div><div class="">The bug reporter visitor gets access to the last node in the exploded graph, but can generally very easily retrace the past,</div><div class="">by going up the chain of predecessors.</div></div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:12.8px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial" class=""><div class=""><div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:12.8px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial" class=""> After looking at the EGs of some code snippets analyzed using the default solver and then Z3, it seems to me that constraints, but also environment and store contents are changing, so one guess would be a yes.</div></div></div></div></div></blockquote><div><br class=""></div><div>In general, I think it should be possible to get a good increase in precision just by re-analyzing the existing exploded graph.</div><div>From my understanding, many constraints are different because the constraint manager tries to be as efficient as possible,</div><div>and destroys all constraints which can not be processed by the current solver.</div><div>If a further increase in precision is needed, it should not be very difficult to change that destroying logic to keep those constraints as well.</div><div><br class=""></div><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:12.8px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial" class=""><div class=""><div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:12.8px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial" class=""> But again, completely re-building EGs might not be far in slow-down from analyzing with Z3 from the beginning, depending on what portion of the code is buggy.</div></div></div></div></div></blockquote><div><br class=""></div><div>Yes, that’s why post-processing is done.</div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:12.8px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial" class=""><div class=""><div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:12.8px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial" class=""> So one could work with the information already present in the graph (this might need telling the analyzer core not to throw away stuff it does not understand when the false positive refutation option is turned on, if such thing happens?), and re-evaluate those, perhaps around the time we call FindReportInEquivalenceClass()<wbr class="">.</div></div></div></div></div></blockquote><div><br class=""></div><div>As mentioned before, it’s better to do those in your own visitor inside BugReporterVisitors.cpp.</div><div>Visitors get the `BugReport` object, and can call `BugReport::markInvalid` if invalidation is needed.</div><div><br class=""></div><div>Regards,</div><div>George</div></div></div></body></html>