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

Dominic Chen via llvm-branch-commits llvm-branch-commits at lists.llvm.org
Fri Aug 18 17:09:24 PDT 2017

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

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

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


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)

More information about the llvm-branch-commits mailing list