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)