[all-commits] [llvm/llvm-project] 7a9bbe: [analyzer] Fix unary/binary op support for SMT sym...

[rdevshp via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: 7a9bbe00493434ad70bd3de0840c980fd88abde6
      https://github.com/llvm/llvm-project/commit/7a9bbe00493434ad70bd3de0840c980fd88abde6
  Author: rdevshp <rdevshp at gmail.com>
  Date:   2026-07-13 (Mon, 13 Jul 2026)

  Changed paths:
    M clang/include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h
    M clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
    M clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
    M clang/lib/StaticAnalyzer/Core/BasicValueFactory.cpp
    M clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
    A clang/test/Analysis/z3/z3-logicalexpr-eval.c
    M clang/test/Analysis/z3/z3-unarysymexpr.c

  Log Message:
  -----------
  [analyzer] Fix unary/binary op support for SMT symbolic execution (#205078)

SMT symbolic execution: 

The patch fixes unary op support, converts operands of logical operators
to boolean in getBinExpr, and clears the hasComparison flag in
getSymExpr when a boolean operand is converted to a non-bool integer.

This PR allows C functions like 
```
int f(int x, int y) {
  if (~(x && y))
    return 0;
  return 1;
}
```
to be analyzed with `-cc1 -analyze -analyzer-checker=core
-analyzer-constraints=z3`

Fixes #205037.

Assisted-by: Codex



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