https://github.com/Snape3058 created https://github.com/llvm/llvm-project/pull/183034
* Fixing #108900 for incorrect "REQUIRES" condition for Z3 * Fixing #168034 for the test failure * Adding more comments about the fixes in #168034 for the tests introduced in #158276 >From 40933c42d7c09fbb8d6f4a479fb37c300c782097 Mon Sep 17 00:00:00 2001 From: Ella Ma <[email protected]> Date: Tue, 24 Feb 2026 10:37:24 +0100 Subject: [PATCH] [analyzer][tests][z3] Fixing the test case bug for testing converting boolean expression to integer * Fixing #108900 for incorrect "REQUIRES" condition for Z3 * Fixing #168034 for the test failure * Adding more comments about the fixes in #168034 for the tests introduced in #158276 --- clang/test/Analysis/z3-unarysymexpr.c | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/clang/test/Analysis/z3-unarysymexpr.c b/clang/test/Analysis/z3-unarysymexpr.c index 82b0fc988a383..efe558c3146e8 100644 --- a/clang/test/Analysis/z3-unarysymexpr.c +++ b/clang/test/Analysis/z3-unarysymexpr.c @@ -1,10 +1,10 @@ // RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify %s \ -// RUN: -analyzer-constraints=z3 +// RUN: -analyzer-constraints=z3 // RUN: %clang_analyze_cc1 -verify %s \ // RUN: -analyzer-checker=core,debug.ExprInspection \ // RUN: -analyzer-config crosscheck-with-z3=true -// REQUIRES: Z3 +// REQUIRES: z3 // // Previously Z3 analysis crashed when it encountered an UnarySymExpr, validate // that this no longer happens. @@ -25,6 +25,10 @@ int negate(int x, int y) { // then causes Z3 to crash. The accompanying patch just strips the negative // operator before submitting to Z3 to avoid the crash. // +// In PR 168034, we fixed this problem by converting boolean expressions to +// bitvec with Z3's ite operator "(ite THE_BOOL_EXPR #x00000000 #x00000001)" +// and actually conducting the negation on the result. +// // TODO: Find the root cause of this and fix it in symbol manager // void c(); @@ -49,9 +53,10 @@ int z3_crash2(int a) { } // Refer to issue 165779 -void z3_crash3(long a) { +long z3_crash3(long a) { if (~-(5 && a)) { long *c; - *c; // expected-warning{{Dereference of undefined pointer value (loaded from variable 'c')}} + return *c; // expected-warning{{Dereference of undefined pointer value (loaded from variable 'c')}} } + return 0; } _______________________________________________ cfe-commits mailing list [email protected] https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
