cbmc

CBMC(C Bounded Model Checker) を試した。

windows+cygwin では、うまくできなかった。Parsing のエラーが出た。

Ubuntu ではすぐにできた。以下にインストールメモを残す。

まずは、インストール。

> apt-get install cbmc

例として、以下のファイル file1.c を作る。

int puts(const char *s) { }

int main(int argc, char **argv) {
  int i;
  if(argc>=1)
    puts(argv[2]);
}

以下で実行する。

> cbmc file1.c --show-claims --bounds-check --pointer-check

すると、以下が出力される。

file file1.c: Parsing
Converting
Type-checking file1
Generating GOTO Program
Adding CPROVER library
Function Pointer Removal
Partial Inlining
Generic Property Instrumentation
Pointer Analysis
Adding Pointer Checks
Claim main.1:
file file1.c line 6 function main
dereference failure: array `argv' upper bound
!(1 + argc <= 2)