[PATCH] D45517: [analyzer] False positive refutation with Z3

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho updated this revision to Diff 148828.
mikhail.ramalho retitled this revision from "[analyzer] WIP: False positive refutation with Z3" to "[analyzer] False positive refutation with Z3".
mikhail.ramalho added a comment.

Added test cases and updated the analyzer-config tests with the new crosscheck flag.

Currently, there is one test failing that does not fail when building without the crosscheck:

  llvm/tools/clang/test/Driver/response-file.c:18:10: error: expected string not found in input
  // LONG: extern int it_works;
           ^
  <stdin>:1:1: note: scanning from here
  clang version 7.0.0 (trunk 333352) (llvm/trunk 333374)
  ^
  <stdin>:8:3: note: possible intended match here
  Selected GCC installation: /usr/lib/gcc/x86_64-redhat-linux/6.4.1
    ^


https://reviews.llvm.org/D45517

Files:
  include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
  include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
  include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h
  lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
  lib/StaticAnalyzer/Core/BugReporter.cpp
  lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
  lib/StaticAnalyzer/Core/ProgramState.cpp
  lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
  test/Analysis/analyzer-config.c
  test/Analysis/analyzer-config.cpp
  test/Analysis/z3-crosscheck.c

-------------- next part --------------
A non-text attachment was scrubbed...
Name: D45517.148828.patch
Type: text/x-patch
Size: 14327 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20180528/e3ad0d55/attachment.bin>