Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[analyzer][doc] Mention that Z3 as the constraint solver is highly unstable #3772

Merged
merged 1 commit into from
Oct 24, 2022

Conversation

whisperity
Copy link
Contributor

Closes #3757

cc @dilyanpalauzov @ryao

Hopefully this is a good enough solution we can mention in CodeChecker's documentation until Z3 support in official Clang picks up.

@whisperity whisperity added documentation 📖 Changes to documentation. analyzer 📈 Related to the analyze commands (analysis driver) clang sa 🐉 The Clang Static Analyzer is a source code analysis tool that finds bugs in C-family programs. labels Oct 19, 2022
@whisperity whisperity added this to the release 6.21.0 milestone Oct 19, 2022

To enable the Z3 solver backend, Clang must be built with the
`LLVM_ENABLE_Z3_SOLVER=ON` compile-time option (for versions earlier than
**9.0**, `CLANG_ANALYZER_BUILD_Z3=ON` must be used instead!), and the
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

My understanding is that since 9.0 LLVM must use the option …, while before 9.0 clang must use the opiton ….

The text suggests that in old and new version the flag must be passed to the clang build configuration.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LLVM has been retrofitted with a monorepo structure even for the old (originally pre-monorepo) versions. So there is only one build that you do, for the entirety of the LLVM umbrella project and you have to pass this flag there.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This discussion is a very small nuance, so the suggested text is good enough, as it is.

@gamesh411
Copy link
Collaborator

It's great to mention the Z3 performance limitation, LGTM

@bruntib bruntib merged commit e918ac4 into Ericsson:master Oct 24, 2022
@whisperity whisperity deleted the fix/doc/z3 branch October 28, 2022 08:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
analyzer 📈 Related to the analyze commands (analysis driver) clang sa 🐉 The Clang Static Analyzer is a source code analysis tool that finds bugs in C-family programs. documentation 📖 Changes to documentation.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Z3 constraint solver is not supported by clangsa
4 participants