Categories

  • Android開発
    android marketで目指せ億万長者(ウソ)
  • cocos2d
    pythonでも使えるゲームフレームワーク
  • Google
    ここには未来を開くためのAPIがたくさん用意されている。
  • GoogleAppEngine
    どこまでもスケールアウトするクラウドサービス。使いこなすのが大変
  • Hack
    様々な電子機器を本来の用途とは別の用途に使ってみる。
  • iPhone開発
    app storeで目指せ億万長者(ウソ)
  • python
    LightWeightLanguageで一番難しいがLispにも通じるところがある面白い言語。
  • TIPS
    覚えておくともしかしたら役に立つかもしれないチョットしたこと。
  • うまくいきません
    やってみたけど、うまくいかなかった失敗記事
  • ネット世界
  • 夢見るソフトウェア
    こんなのいいな、できたらいいな、いつかつくろう
  • 開発環境
    開発するまえに環境を整えた記録、次に同じことをするためめの忘備録
無料ブログはココログ
My Photo

« August 2012 | Main | January 2013 »

October 26, 2012

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

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

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

静的コード解析

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

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

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

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

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

C言語とC++

 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

« August 2012 | Main | January 2013 »