https://github.com/steakhal updated
https://github.com/llvm/llvm-project/pull/95129
___
llvm-branch-commits mailing list
llvm-branch-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-branch-commits
https://github.com/steakhal updated
https://github.com/llvm/llvm-project/pull/95129
___
llvm-branch-commits mailing list
llvm-branch-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-branch-commits
steakhal wrote:
Ah, it mixed the messages... Here it is:
- Removed unused `NumZ3QueriesDoneInEqClass`
- Added a new `crosscheck-with-z3-eqclass-timeout-threshold` config option.
- Removed misleading `// unsat` comment on return statement.
- Removed unnecessary `// sat` comment on return statemen
https://github.com/steakhal updated
https://github.com/llvm/llvm-project/pull/95129
___
llvm-branch-commits mailing list
llvm-branch-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-branch-commits
https://github.com/steakhal updated
https://github.com/llvm/llvm-project/pull/95129
___
llvm-branch-commits mailing list
llvm-branch-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-branch-commits
@@ -17,43 +18,126 @@ using Z3Decision = Z3CrosscheckOracle::Z3Decision;
static constexpr Z3Decision AcceptReport = Z3Decision::AcceptReport;
static constexpr Z3Decision RejectReport = Z3Decision::RejectReport;
+static constexpr Z3Decision RejectEQClass = Z3Decision::RejectEQCl
@@ -101,18 +123,37 @@ void Z3CrosscheckVisitor::Profile(llvm::FoldingSetNodeID
&ID) const {
Z3CrosscheckOracle::Z3Decision Z3CrosscheckOracle::interpretQueryResult(
const Z3CrosscheckVisitor::Z3Result &Query) {
++NumZ3QueriesDone;
+ ++NumZ3QueriesDoneInEqClass;
+ Accum
@@ -101,18 +123,37 @@ void Z3CrosscheckVisitor::Profile(llvm::FoldingSetNodeID
&ID) const {
Z3CrosscheckOracle::Z3Decision Z3CrosscheckOracle::interpretQueryResult(
const Z3CrosscheckVisitor::Z3Result &Query) {
++NumZ3QueriesDone;
+ ++NumZ3QueriesDoneInEqClass;
+ Accum
@@ -101,18 +123,37 @@ void Z3CrosscheckVisitor::Profile(llvm::FoldingSetNodeID
&ID) const {
Z3CrosscheckOracle::Z3Decision Z3CrosscheckOracle::interpretQueryResult(
const Z3CrosscheckVisitor::Z3Result &Query) {
++NumZ3QueriesDone;
+ ++NumZ3QueriesDoneInEqClass;
+ Accum
https://github.com/NagyDonat approved this pull request.
Oops, I vaguely recalled that I already reviewed this, but it turns out I
didn't. Anyway, the change LGTM, I only added a few minor remarks. (We already
discussed a high-level overview of this on Discourse.)
https://github.com/llvm/llvm-
https://github.com/NagyDonat edited
https://github.com/llvm/llvm-project/pull/95129
___
llvm-branch-commits mailing list
llvm-branch-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-branch-commits
@@ -44,21 +47,43 @@ class Z3CrosscheckVisitor final : public BugReporterVisitor
{
/// Holds the constraints in a given path.
ConstraintMap Constraints;
Z3Result &Result;
+ const AnalyzerOptions &Opts;
};
/// The oracle will decide if a report should be accepted or r
steakhal wrote:
Ping. @NagyDonat @Xazax-hun @haoNoQ
https://github.com/llvm/llvm-project/pull/95129
___
llvm-branch-commits mailing list
llvm-branch-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-branch-commits
steakhal wrote:
I've tested this change on 200+ projects, and the overall effect is:
- 0 new issues appear
- 276 issues disappear (because we drop the report eqclass)
The three most affected checker categories (all of them are spread across
usually 20+ projects):
- null-deref-like diagnos
https://github.com/steakhal updated
https://github.com/llvm/llvm-project/pull/95129
___
llvm-branch-commits mailing list
llvm-branch-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-branch-commits
https://github.com/steakhal updated
https://github.com/llvm/llvm-project/pull/95129
___
llvm-branch-commits mailing list
llvm-branch-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-branch-commits
llvmbot wrote:
@llvm/pr-subscribers-clang
Author: Balazs Benics (steakhal)
Changes
This patch is a functional change.
https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520
As a result of this patch, individual Z3 queries in refutation will be
bound by 300ms. Every report e
https://github.com/steakhal created
https://github.com/llvm/llvm-project/pull/95129
This patch is a functional change.
https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520
As a result of this patch, individual Z3 queries in refutation will be
bound by 300ms. Every report equiva
18 matches
Mail list logo
