[all-commits] [llvm/llvm-project] 9ca62c: [analyzer] Indicate UnarySymExpr is not supported ...

[vabridgers via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: 9ca62c5302633d0220de30f2b2a21d87dee64ac0
      https://github.com/llvm/llvm-project/commit/9ca62c5302633d0220de30f2b2a21d87dee64ac0
  Author: vabridgers <58314289+vabridgers at users.noreply.github.com>
  Date:   2024-09-19 (Thu, 19 Sep 2024)

  Changed paths:
    M clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
    A clang/test/Analysis/z3-unarysymexpr.c

  Log Message:
  -----------
  [analyzer] Indicate UnarySymExpr is not supported by Z3 (#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 compiler
crashes.

Some crash context ...

clang -cc1 -analyze -analyzer-checker=core z3-unarysymexpr.c
-analyzer-constraints=z3

Unsupported expression to reason about!
UNREACHABLE executed at
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h:297!

Stack dump:
3. <root>/clang/test/Analysis/z3-unarysymexpr.c:13:7: Error evaluating
branch #0 <addr> llvm::sys::PrintStackTrace(llvm::raw_ostream&, int) #1
<addr> llvm::sys::RunSignalHandlers() #8 <addr>
clang::ento::SimpleConstraintManager::assumeAux(
llvm::IntrusiveRefCntPtr<clang::ento::ProgramState const>,
clang::ento::NonLoc, bool) #9 <addr>
clang::ento::SimpleConstraintManager::assume(
llvm::IntrusiveRefCntPtr<clang::ento::ProgramState const>,
clang::ento::NonLoc, bool)

Co-authored-by: einvbri <vince.a.bridgers at ericsson.com>



To unsubscribe from these emails, change your notification settings at https://github.com/llvm/llvm-project/settings/notifications