[all-commits] [llvm/llvm-project] b3b0d0: Reland "[analyzer][NFC] Reorganize Z3 report refut...

[Balazs Benics via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: b3b0d09ccee52472691570072ac0e30f1addbb0a
      https://github.com/llvm/llvm-project/commit/b3b0d09ccee52472691570072ac0e30f1addbb0a
  Author: Balazs Benics <benicsbalazs at gmail.com>
  Date:   2024-07-01 (Mon, 01 Jul 2024)

  Changed paths:
    M clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
    A clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h
    M clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
    M clang/lib/StaticAnalyzer/Core/BugReporter.cpp
    M clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
    M clang/lib/StaticAnalyzer/Core/CMakeLists.txt
    A clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
    A clang/test/Analysis/z3/crosscheck-statistics.c
    M clang/unittests/StaticAnalyzer/CMakeLists.txt
    A clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp
    M llvm/include/llvm/Support/SMTAPI.h
    M llvm/lib/Support/Z3Solver.cpp

  Log Message:
  -----------
  Reland "[analyzer][NFC] Reorganize Z3 report refutation" (#97265)

This is exactly as originally landed in #95128,
but now the minimal Z3 version was increased to meet this change in #96682.

https://discourse.llvm.org/t/bump-minimal-z3-requirements-from-4-7-1-to-4-8-9/79664/4

---

This change keeps existing behavior, namely that if we hit a Z3 timeout
we will accept the report as "satisfiable".

This prepares for the commit "Harden safeguards for Z3 query times".
https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520

(cherry picked from commit 89c26f6c7b0a6dfa257ec090fcf5b6e6e0c89aab)



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