[PATCH] D82856: [analyzer][Z3-refutation] Add statistics for refutation visitor

steakhal abandoned this revision. steakhal added a comment. It might be useful in the future, but right now, I'm not interested in upstreaming this. CHANGES SINCE LAST ACTION https://reviews.llvm.org/D82856/new/ https://reviews.llvm.org/D82856 ___

[PATCH] D82856: [analyzer][Z3-refutation] Add statistics for refutation visitor

steakhal updated this revision to Diff 274510. steakhal added a comment. - adds statistic to undecidable branch CHANGES SINCE LAST ACTION https://reviews.llvm.org/D82856/new/ https://reviews.llvm.org/D82856 Files: clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp Index: clang/lib/Sta

[PATCH] D82856: [analyzer][Z3-refutation] Add statistics for refutation visitor

NoQ added a comment. > I have one question though. Isn't this counting all the reports in an > equivalence class? Yes it is. You have no choice but to run refutation before deduplication; otherwise the otherwise-best report in the class may be false when other reports are true. CHANGES SINCE

[PATCH] D82856: [analyzer][Z3-refutation] Add statistics for refutation visitor

NoQ added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2856-2857 Optional IsSAT = RefutationSolver->check(); if (!IsSAT.hasValue()) return; I strongly recommend a statistic for this branch as well. I.e., how many

[PATCH] D82856: [analyzer][Z3-refutation] Add statistics for refutation visitor

steakhal added a comment. In D82856#2122330 , @xazax.hun wrote: > Yay! This looks good to me and I love statistics, so a huge +1. > I have one question though. Isn't this counting all the reports in an > equivalence class? I.e. if the analyzer finds som

[PATCH] D82856: [analyzer][Z3-refutation] Add statistics for refutation visitor

xazax.hun added a comment. Yay! This looks good to me and I love statistics, so a huge +1. I have one question though. Isn't this counting all the reports in an equivalence class? I.e. if the analyzer finds something multiple times it will only be displayed once but here it will be counted mult

[PATCH] D82856: [analyzer][Z3-refutation] Add statistics for refutation visitor

steakhal created this revision. steakhal added reviewers: NoQ, xazax.hun, Szelethus, martong. Herald added subscribers: cfe-commits, ASDenysPetrov, Charusso, dkrupp, donat.nagy, mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware, whisperity. Herald added a project: clang. This patc