https://github.com/vabridgers closed
https://github.com/llvm/llvm-project/pull/108900
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
@@ -278,6 +278,13 @@ class SMTConstraintManager : public
clang::ento::SimpleConstraintManager {
if (const SymbolCast *SC = dyn_cast(Sym))
return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
+// If a UnarySymExpr is encountered, the Z3
+// wrapper doe
https://github.com/vabridgers updated
https://github.com/llvm/llvm-project/pull/108900
>From d48964b43ddc1bdc8a3c51198cbf08677287bd74 Mon Sep 17 00:00:00 2001
From: einvbri
Date: Tue, 17 Sep 2024 01:25:20 +0200
Subject: [PATCH] [analyzer] Indicate UnarySymExpr is not supported by Z3
Random tes
https://github.com/vabridgers updated
https://github.com/llvm/llvm-project/pull/108900
>From 1790ebab722f53b5dba3ef7cd2afb7cf2549f245 Mon Sep 17 00:00:00 2001
From: einvbri
Date: Tue, 17 Sep 2024 01:25:20 +0200
Subject: [PATCH 1/2] [analyzer] Indicate UnarySymExpr is not supported by Z3
Random
@@ -278,6 +278,13 @@ class SMTConstraintManager : public
clang::ento::SimpleConstraintManager {
if (const SymbolCast *SC = dyn_cast(Sym))
return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
+// If a UnarySymExpr is encountered, the Z3
+// wrapper doe
https://github.com/NagyDonat edited
https://github.com/llvm/llvm-project/pull/108900
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
https://github.com/NagyDonat approved this pull request.
LGTM with some additional bikeshedding in a comment that could be shorter IMO.
https://github.com/llvm/llvm-project/pull/108900
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lis
vabridgers wrote:
Hi @NagyDonat , I think all comments have been addressed. Please review at your
convenience. Thank you!
https://github.com/llvm/llvm-project/pull/108900
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/
https://github.com/vabridgers updated
https://github.com/llvm/llvm-project/pull/108900
>From 754ae098e55cd9ea6f7ebeed37aad761598af0f2 Mon Sep 17 00:00:00 2001
From: einvbri
Date: Tue, 17 Sep 2024 01:25:20 +0200
Subject: [PATCH] [analyzer] Indicate UnarySymExpr is not supported by Z3
Random tes
steakhal wrote:
> > I'm okay with the PR, but this leaves me wonder how did you end up with
> > this crash? How did you manage to avoid all the zillion other ways to crash
> > the Z3 solver? Have you experienced such issues?
>
> Thanks Balazs, TBH I'm not sure we've found all the ways to crash
vabridgers wrote:
> I'm okay with the PR, but this leaves me wonder how did you end up with this
> crash? How did you manage to avoid all the zillion other ways to crash the Z3
> solver? Have you experienced such issues?
Thanks Balazs, TBH I'm not sure we've found all the ways to crash the Z3
steakhal wrote:
I'm okay with the PR, but this leaves me wonder how did you end up with this
crash?
How did you manage to avoid all the zillion other ways to crash the Z3 solver?
Have you experienced such issues?
https://github.com/llvm/llvm-project/pull/108900
@@ -278,6 +278,13 @@ class SMTConstraintManager : public
clang::ento::SimpleConstraintManager {
if (const SymbolCast *SC = dyn_cast(Sym))
return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
+// If a UnarySymExpr is encountered, the Z3
+// wrapper doe
vabridgers wrote:
Hi @NagyDonat , yes this is only exposed when z3 is used as the constraint
manager. This crash does not occur when using z3-refutation.
https://github.com/llvm/llvm-project/pull/108900
___
cfe-commits mailing list
cfe-commits@lists.
@@ -0,0 +1,16 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify
%s \
+// RUN: -analyzer-constraints=z3
+
+// REQUIRES: Z3
+//
+// This LIT covers a crash associated with this test.
+// The expectation is to not crash!
+//
+
+long a;
+void b() {
@@ -0,0 +1,16 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify
%s \
+// RUN: -analyzer-constraints=z3
+
+// REQUIRES: Z3
+//
+// This LIT covers a crash associated with this test.
+// The expectation is to not crash!
vabridgers
https://github.com/vabridgers updated
https://github.com/llvm/llvm-project/pull/108900
>From 33621d8862e6d1b98dc88aa0452faced0e3e5f17 Mon Sep 17 00:00:00 2001
From: einvbri
Date: Tue, 17 Sep 2024 01:25:20 +0200
Subject: [PATCH] [analyzer] Indicate UnarySymExpr is not supported by Z3
Random tes
https://github.com/NagyDonat edited
https://github.com/llvm/llvm-project/pull/108900
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
https://github.com/NagyDonat edited
https://github.com/llvm/llvm-project/pull/108900
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
https://github.com/NagyDonat edited
https://github.com/llvm/llvm-project/pull/108900
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
@@ -0,0 +1,16 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify
%s \
+// RUN: -analyzer-constraints=z3
+
+// REQUIRES: Z3
+//
+// This LIT covers a crash associated with this test.
+// The expectation is to not crash!
+//
+
+long a;
+void b() {
https://github.com/NagyDonat commented:
Do I understand it correctly that this deficiency affects the standalone Z3
analysis mode (as opposed to the "Z3 refutation" where the analysis is
performed with the native range-based constraint manager, and then the results
are validated with Z3 to dis
@@ -0,0 +1,16 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify
%s \
+// RUN: -analyzer-constraints=z3
+
+// REQUIRES: Z3
+//
+// This LIT covers a crash associated with this test.
+// The expectation is to not crash!
NagyDonat
vabridgers wrote:
Maybe this CR could be easily improved to handle this case correctly rather
than avoiding the crash, just wanted to see if it's better to get this change
in for now avoiding the crash or get some advice on how to fix this correctly.
https://github.com/llvm/llvm-project/pull/
llvmbot wrote:
@llvm/pr-subscribers-clang
@llvm/pr-subscribers-clang-static-analyzer-1
Author: None (vabridgers)
Changes
Random testing found that the Z3 wrapper does not support UnarySymExpr, which
was added recently and not included in the original Z3 wrapper. For now, just
avoid submi
https://github.com/vabridgers created
https://github.com/llvm/llvm-project/pull/108900
Random testing found that the Z3 wrapper does not support UnarySymExpr, which
was added recently and not included in the original Z3 wrapper. For now, just
avoid submitting expressions to Z3 to avoid compile
26 matches
Mail list logo
