いつの間にかコードを書くより読むことのほうが多くなったのでコード解析ツールを探す

　わけあってC言語のソースを読むことになった。しばらくpythonとかに慣れていると、明示的な型変換とか、なんでもforループとか読んでいてまどろっこしい。この感覚は、C言語に慣れたあとにアセンブラのソースを見た時と共通するものがある。

　というわけで、解析ツールを使おうと思って調べたら、プログラムの静的解析が流行りらしくてバグ取りに使うものがいっぱいあった。メモリーリークとか、バッファーオーバーランの可能性をソースから調べてくれる。メモリーの管理が自分でできないならC言語使わないほうが幸せなのにねと思いつつWikipediaでしらべてみた。

静的コード解析

形式手法は、ソフトウェアやハードウェアの解析に用いられる用語であり、厳密に数学的な手法によって解析結果を得ることを意味する。数学的手法としては、表示的意味論、公理的意味論、操作的意味論、抽象解釈などがある。実行時エラーを全て検出することは不可能であることが証明されており、任意のプログラムが正しく動作するかエラーになるかを判定する機械的手法はない。これは1930年代のアラン・チューリングやライスの研究で判明した（チューリングマシンの停止問題およびライスの定理）。決定不能な問題ではあるが、近似的な解でも有効である。形式的な静的コード解析の実装方法には以下のようなものがある:

• モデル検査は、有限の状態を持つシステムを対象とし、無限に状態を持つシステムを抽象化によって状態数を有限個に減らして行うこともある。
• 抽象解釈は、プログラムの個々の文が抽象機械の状態に何らかの影響を与える様子をモデル化したものである（つまり、ソフトウェアを個々の文の数学的属性と宣言に基づいて「実行」する）。

なんかすごい事やっている。頭の良い人に感謝

リンクがデッドリンクだったり、URLが変わっていたりしたので調べてみた。２０１２−１０−２５時点での最終更新日も書き加えた。やっぱりひとつのプロダクトを１０年以上維持するのは大変なんだな。商用のパッケージは会社で使うとして、個人で使える範囲のものをこれから試してみよう。

Wikipediaに載っていた静的コード解析ツール

C言語とC++

• anyWarp CodeDirector for C/C++ (商用)　日立ソリューションズ
• BLAST  2008-07-11
• Parasoft C++test (商用)　日本支社があったらしい。
• C99parser (GPL) 2012-02-03 GraphViz  でgraph が書ける
• CCured BSDライセンス。2010-06-22 source forge にソースを残すのみ。本体は行方不明
• CodeSonar (商用)　AIコーポレーション
• Coverity Prevent (商用)　日本語でOK
• cppcheck (GPL)　2012-09-01 EclipseやJenkinsなどとのインテグレートもあり
• Cqual (GPL) 2009-07-17
• CScout (CSCOUT Public License) 2011-10-23 ソースコード解析とリファクタリング・ブラウザ。プリプロセッサの構文も扱う。
• Flawfinder (GPL) 最終更新日不明　内部動作の解説あり
• Goanna (商用) visutal studioとのインテグレート
• Fortify SCA [1]^{(商用） SRAやHPなどから販売}
• introspector (GPL)  2006-05-30 C言語用だが、他の言語にも対応中。
• Klocwork Insight （商用）日本語でOK
• MOPS （BSD風ライセンス）2002-05-07
• OpenC++ (ライセンスは複雑) 2004-08-29 東大の千葉滋氏が2001年まで関わっていた 
• QAC ,QAC++ (商用)　IDE統合型
• PGRelief (商用)　富士通ソフトウェアテクノロジーズ
• PMD's Copy/Paste Detector（BSD風ライセンス）2012-01-31 重複ブロック検出
• PolySpace (商用) MathWorks
• PREfast ドライバ開発用 DDK の一部（マイクロソフト）
• Review-C (商用) 終了
• Smatch C言語ソースチェッカー。主にLinuxカーネル 用。
• Sparse (GPL) 2009-10-16
• Stacktool プロジェクト中断
• Splint (GPL)　2010-08-05
• Visual Studio 2005 Team Edition のみ。
• Clang Static Analyzer (BSD風ライセンス) 2012-09-25 MacOS用
• AdLint (GPL)2012-10-12 日本語　Rubyで記述

 SLAM Microsoft research 多くのプロジェクトが参照している

PMDのサイトにあったリンク集　JAVAならいろいろある。

• Checkstyle - Very detailed, supports both Maven and Ant. Uses ANTLR.
• DoctorJ - Uses JavaCC. Checks Javadoc, syntax and calculates metrics.
• ESC/Java - Finds null dereference errors, array bounds errors, type cast errors, and race conditions. Uses Java Modeling Language annotations.
• FindBugs - works on bytecode, uses BCEL. Source code uses templates, nifty stuff!
• Hammurapi - Uses ANTLR, excellent documentation, lots of rules
• Jamit - bytecode analyzer, nice graphs
• JCSC - Does a variety of coding standard checks, uses JavaCC and the GNU Regexp package.
• Jikes - More than a compiler; now it reports code warnings too
• JLint - Written in C++. Uses data flow analysis and a lock graph to do lots of synchronization checks. Operates on class files, not source code.
• JPathFinder - A verification VM written by NASA; supports a subset of the Java packages