VeriFastのDockerイメージを作りました
C言語/Java検証器であるVeriFastのDockerイメージを公開しました。
> https://hub.docker.com/r/eldesh/verifast/
現時点(2017/8/24)での開発ヘッドをビルドしてあります*1。リリース版は公式サイトでバイナリが配布されているのでそちらを使いましょう。
このイメージはgitのコミットハッシュをタグにしてあり、latestタグは無いので明示的にこれを指定してDockerイメージを取得する必要があります。
つまり以下のようにすると
$ docker pull eldesh/verifast:93c7917
取得できます。
使い方
デフォルトではvfideというVeriFastのGUIフロントエンドが起動するので、以下のように環境変数 DISPLAY の設定が必要です。
// 例: ディスプレイ 192.168.1.2:0 を使う $ docker run -e DISPLAY=192.168.1.2:0 eldesh/verifast:93c7917
当然ながらverifastコマンドもインストールされているので、明示すれば使うことが出来ます。
// ボリューム some-vol にあるコードを検査
$ docker run -v some-vol:/src eldesh/verifast:93c7917 verifast /src/hoge.c
ついでにZ3サポートも付いています。
// SMTソルバとしてZ3を使う $ docker run -v some-vol:/src eldesh/verifast:93c7917 verifast -prover z3v4.5 /src/hoge.c
