Astrée is a well-known tool based on abstract interpretation ables to perform sound analysis (https://doi.org/10.1007/978-3-540-31987-0_3). Another industrial tool that could be interesting for C/C++ analysis is CodeSonar

Coverity, Svace, ... are standard and first to come answers. But I would first ask about defects that you need to detect, maybe these tools do not support this analysis.

You can have a look at IKOS (https://github.com/NASA-SW-VnV/ikos), a static analyzer for C and C++ based on abstract interpretation.

Dear Vard Antinyan,

I can suggest 2 well documented static analyzers to detect at least code violations in C:

1) Frama-c a powerful framework (rich set of plugins ) such that:

- It automatically detects bugs by enabling some plugins (e.g. rte for runtime errors, eva to enable value analysis based on abstract interpretation , ...etc) https://frama-c.com/html/documentation.html

-it allows to write custom rules (as annotations in C source) to be checked during the analysis or you can even write your own plugin (using OCaml language) if needed.

2) Clang Static Analyzer which implements path-sensitive, inter-procedural analysis based on symbolic execution technique. Here is the documentation page with the available checkers, including official tool page: https://clang.llvm.org/docs/ClangStaticAnalyzer.html#:~:text=The%20Clang%20Static%20Analyzer%20is,the%20Static%20Analyzer%20documentation%20page.

There cannot be a single best static analysis for C code.

You might look into GCC plugins like Bismon on https://github.com/bstarynk/bismon/ or tools like https://frama-c.com/

BTW, I am seeking partners interested by RefPerSys on http://refpersys.org/