Frama-CはC言語のソースコードを解析し、おかしいところをチェックしてくれるツール。Ubuntu,Window XP, Mac OSで動作する。またACSLという、ソースコードにコメントの形で付加する行動記述言語も備えており、例えば以下のように関数の前に記述しておくと、この関数の戻り値\resultの値の条件を示しておくことができる。
|
1 2 3 4 |
/*@ ensures \result >= x && \result >= y; ensures \result == x || \result == y; */ int max (int x, int y) { return (x > y) ? x : y; } |
ソースコードの解析方法は色々なものがあり、それぞれプラグインで提供されており、デフォルトでも実験的なものも含めて１６個くらいある。
Windows XPで使うにはmingwとocaml for mingwがインストールされている環境でmsysから使うことができる。解析の際GCCでプリプロセスを実行するため対象のCソースファイルが含むヘッダがないとエラーになってしまう。
実行は、frama-cコマンドまたはframa-c-guiコマンドで行う。以下はサンプルでついてきたwin_iconv.cに対して行った例。
$ frama-c-gui.exe win_iconv.c
[preprocessing] running gcc -C -E -I. win_iconv.c
Parsing
Cleaning unused parts
Symbolic link
Starting semantical analysis
ソースコードにACSLが記述してある場合、プラグインのValViewerによって評価、解析ををすることができる。