# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1464077241 -32400
# Node ID 865c1b265e80fb57d057a9315f132d90c5d5e5f2
# Parent  073de2e0c1489b9ab0733870a0d4f037902541bf
Update Dockerfile

diff -r 073de2e0c148 -r 865c1b265e80 cbmc/Dockerfile
--- a/cbmc/Dockerfile	Tue May 24 14:48:43 2016 +0900
+++ b/cbmc/Dockerfile	Tue May 24 17:07:21 2016 +0900
@@ -1,8 +1,10 @@
-from fedora:23
+from gears
 
-RUN dnf update -y && dnf install -y man clang lldb wget zsh git mercurial tar vim && dnf clean all
+RUN dnf update -y && dnf install -y man clang clang-devel gcc lldb wget zsh git mercurial tar vim && dnf clean all
 
+# Install cbmc
 RUN mkdir /root/cbmc
 WORKDIR /root/cbmc
 RUN wget http://www.cprover.org/cbmc/download/cbmc-5-4-linux-64.tgz
 RUN tar xzf cbmc-5-4-linux-64.tgz -C /usr/local/bin
+
diff -r 073de2e0c148 -r 865c1b265e80 cbmc/README
--- a/cbmc/README	Tue May 24 14:48:43 2016 +0900
+++ b/cbmc/README	Tue May 24 17:07:21 2016 +0900
@@ -3,5 +3,9 @@
 CBMC is a Bounded Model Checker for C. (http://www.cprover.org/cbmc/)
 We will compare with cbmc and akasha.
 
+Dockerfile adds cbmc in gears contaier.
+So it needs gears container in http://firefly.cr.ie.u-ryukyu.ac.jp/hg/Gears .
+
+$ docker build -t gears <path/to/gears-Dockerfile>
 $ docker build -t cbmc .
 $ docker run -it cbmc zsh