[all-commits] [llvm/llvm-project] b5b2ae: [analyzer] Add UnarySymExpr

[Gabor Marton via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: b5b2aec1ff51197343dede9741ea377f8314d41b
      https://github.com/llvm/llvm-project/commit/b5b2aec1ff51197343dede9741ea377f8314d41b
  Author: Gabor Marton <gabor.marton at ericsson.com>
  Date:   2022-05-26 (Thu, 26 May 2022)

  Changed paths:
    M clang/include/clang/StaticAnalyzer/Checkers/SValExplainer.h
    M clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
    M clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h
    M clang/include/clang/StaticAnalyzer/Core/PathSensitive/Symbols.def
    M clang/lib/StaticAnalyzer/Checkers/ExprInspectionChecker.cpp
    M clang/lib/StaticAnalyzer/Core/SValBuilder.cpp
    M clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
    M clang/lib/StaticAnalyzer/Core/SymbolManager.cpp
    M clang/test/Analysis/explain-svals.cpp
    M clang/test/Analysis/expr-inspection.cpp
    A clang/test/Analysis/unary-sym-expr.c

  Log Message:
  -----------
  [analyzer] Add UnarySymExpr

This patch adds a new descendant to the SymExpr hierarchy. This way, now
we can assign constraints to symbolic unary expressions. Only the unary
minus and bitwise negation are handled.

Differential Revision: https://reviews.llvm.org/D125318


  Commit: 88abc50398eb26d536518270b91939ce18687305
      https://github.com/llvm/llvm-project/commit/88abc50398eb26d536518270b91939ce18687305
  Author: Gabor Marton <gabor.marton at ericsson.com>
  Date:   2022-05-26 (Thu, 26 May 2022)

  Changed paths:
    M clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
    A clang/test/Analysis/constraint_manager_negate.c
    M clang/test/Analysis/constraint_manager_negate_difference.c
    A clang/test/Analysis/unary-sym-expr-no-crash.c
    M clang/test/Analysis/unary-sym-expr.c

  Log Message:
  -----------
  [analyzer][solver] Handle UnarySymExpr in RangeConstraintSolver

Fixes https://github.com/llvm/llvm-project/issues/55241

Differential Revision: https://reviews.llvm.org/D125395


  Commit: cd5783d3e82b98bfa140853fee95170852fd3c74
      https://github.com/llvm/llvm-project/commit/cd5783d3e82b98bfa140853fee95170852fd3c74
  Author: Gabor Marton <gabor.marton at ericsson.com>
  Date:   2022-05-26 (Thu, 26 May 2022)

  Changed paths:
    M clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
    A clang/test/Analysis/unary-sym-expr-z3-refutation.c
    M clang/test/Analysis/z3-crosscheck.c

  Log Message:
  -----------
  [analyzer][solver] Handle UnarySymExpr in SMTConv

Dependent patch adds UnarySymExpr, now I'd like to handle that for SMT
conversions like refutation.

Differential Revision: https://reviews.llvm.org/D125547


Compare: https://github.com/llvm/llvm-project/compare/ca3d962548b9...cd5783d3e82b