[llvm-branch-commits] [cfe-branch] r311213 - Add release notes for r299463.

[Dominic Chen via llvm-branch-commits]

Author: ddcc
Date: Fri Aug 18 17:09:24 2017
New Revision: 311213

URL: http://llvm.org/viewvc/llvm-project?rev=311213&view=rev
Log:
Add release notes for r299463.

Implement z3-based constraint solver backend for clang static analyzer.

Modified:
    cfe/branches/release_50/docs/ReleaseNotes.rst

Modified: cfe/branches/release_50/docs/ReleaseNotes.rst
URL: http://llvm.org/viewvc/llvm-project/cfe/branches/release_50/docs/ReleaseNotes.rst?rev=311213&r1=311212&r2=311213&view=diff
==============================================================================
--- cfe/branches/release_50/docs/ReleaseNotes.rst (original)
+++ cfe/branches/release_50/docs/ReleaseNotes.rst Fri Aug 18 17:09:24 2017
@@ -200,7 +200,13 @@ libclang
 Static Analyzer
 ---------------
 
-...
+- The static analyzer now supports using the
+  `z3 theorem prover <https://github.com/z3prover/z3>`_ from Microsoft Research
+  as an external constraint solver. This allows reasoning over more complex
+  queries, but performance is ~15x slower than the default range-based
+  constraint solver. To enable the z3 solver backend, clang must be built with
+  the ``CLANG_ANALYZER_BUILD_Z3=ON`` option, and the
+  ``-Xanalyzer -analyzer-constraints=z3`` arguments passed at runtime.
 
 Undefined Behavior Sanitizer (UBSan)
 ------------------------------------