CBMCの使い方入門:1 - interdb’s blog

"CBMC"というモデル検査ツールの使い方を学ぶ。 組込み分野では有名なツール。すでに開発終了したという人もいる*1が、最新版3.9は2010.12.19リリース。2010年には3.6,3.7,3.8,3.9と4バージョンリリースなので、アクティビティが落ちているようにはみえない。 配列の検査:1 故意に範囲を逸脱して値を代入するプログラムを書く。 cat test1.c #define SIZE 5 int main(int argc, char **argv) { int i; int a[SIZE]; for (i = 0; i <= SIZE; i++) /* 故意に範囲を間違えてみる */ a[i] = i; return 0; } このソースtest1.cをcbmcに読ませ、静的解析を行う。 $ ./cbmc test1.c --bounds-check --pointer-c