diff options
| author | Dominic Chen <d.c.ddcc@gmail.com> | 2017-08-19 00:09:24 +0000 |
|---|---|---|
| committer | Dominic Chen <d.c.ddcc@gmail.com> | 2017-08-19 00:09:24 +0000 |
| commit | 6fe97e5ae9416b6ec66da3cf03b703b3798206d1 (patch) | |
| tree | c672d43293e1f3d8876721cfda6b929a5217e3f3 | |
| parent | 502461a8c938b8ccd464d8d79e3b098b84cae6d3 (diff) | |
Add release notes for r299463.
Implement z3-based constraint solver backend for clang static analyzer.
git-svn-id: https://llvm.org/svn/llvm-project/cfe/branches/release_50@311213 91177308-0d34-0410-b5e6-96231b3b80d8
| -rw-r--r-- | docs/ReleaseNotes.rst | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/docs/ReleaseNotes.rst b/docs/ReleaseNotes.rst index d6bc7d18f1..a5d459d333 100644 --- a/docs/ReleaseNotes.rst +++ b/docs/ReleaseNotes.rst @@ -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) ------------------------------------ |