ヤマタニの履歴(No.12)

先ず，「VirtualBox?+Vagrantを使いUbuntu 14.04を動かす」のは，ここを参考にしてください． http://blog.kondoyoshiyuki.com/2014/06/12/windows7-vagrant-ubuntu14-04/ （Perl本の翻訳などを行っている近藤さん解説）

これを参考に32ビットの場合， ?VirtualBox?のインストール

?Vagrantのインストール

?ubuntuのインストールコマンドプロンプトから vagrant box add ubuntu14.04.32 https://cloud-images.ubuntu.com/vagrant/trusty/current/trusty-server-cloudimg-i386-vagrant-disk1.box

適当な作業ディレクトリを作り mkdir myhost32 cd myhost32

vagrant init ubuntu14.04.32

デフォルトメモリーでは小さいので，このディレクトリに作られたVagrantfile のメモリー設定を変更４５行目からコメントアウト

config.vm.provider "virtualbox" do |vb|
   # Don't boot with headless mode
   vb.gui = true

   # Use VBoxManage to customize the VM. For example to change memory:
   vb.customize ["modifyvm", :id, "--memory", "1024"]
 end

ホストコマンドプロンプトから vagrant up vagrant ssh これでubuntuにログインできる

?crestの設定（vagreant ssh　後）ここから，ubuntuの中です． sudo apt-get install unzip m4 sudo apt-get install opam opam init

opam install cil　　　　　＃なぜかfindlibがインストールされていない

cd wget http://download.camlcity.org/download/findlib-1.5.1.tar.gz tar zxvf findlib-1.5.1.tar.gz cd findlib-1.5.1/ ./configure make all sudo make install

cd wget https://github.com/jburnim/crest/archive/v0.1.2.zip unzip v0.1.2.zip cd crest-0.1.2/ cd cil ./conffigure make make install

cd ここでホスト側での作業 http://yices.csl.sri.com/cgi-bin/yices-newlicense.cgi?file=yices-1.0.38-i686-pc-linux-gnu-static-gmp.tar.gz からlicense Termsに合意してDL これを　myhost32/にコピーすると　ubuntuの/vagrant/にコピーされている

ゲスト側

cp /vagrant/yices-1.0.38-i686-pc-linux-gnu-static-gmp.tar.gz ./ tar zxvf yices-1.0.38-i686-pc-linux-gnu-static-gmp.tar.gz これでyicesが展開される

Makefileの修正 cd crest-0.1.2/ cd src cp Makefile /vagrant/

ホストPC側のエディターで　myhost32/Makefike のパス変更最初の行を書き換える YICES_DIR=/home/vagrant/yices-1.0.38 格納後ゲスト側で cp /Vagrant/Makefile ./ make make install

cd .. cd test

ここで確認

../bin/crestc uniform_test.c 何やらワーニングが出るが Read 8 branches. Read 13 nodes. Wrote 6 branch edges.

次は実行 $ ../bin/run_crest ./uniform_test 10 -dfs Iteration 0 (0s): covered 0 branches [0 reach funs, 0 reach branches]. Iteration 1 (0s): covered 1 branches [1 reach funs, 8 reach branches]. Iteration 2 (0s): covered 3 branches [1 reach funs, 8 reach branches]. Iteration 3 (0s): covered 5 branches [1 reach funs, 8 reach branches]. Iteration 4 (0s): covered 7 branches [1 reach funs, 8 reach branches]. GOAL! Iteration 5 (0s): covered 8 branches [1 reach funs, 8 reach branches].

以上，ネットの状況にもよりますが，１?２時間で出来ます．

ヤマタニ/Understand

ヤマタニ の履歴(No.12)

Memo†

卒研までの流れ†

Schedule†

Theme†

Goal†

Approach†

Keyword†

Symposium†

2013年度（B4）†

Part-Time job†

Paper I've read†

Reference†

Study†

Papers†

Tools†

CREST†

ヤマタニの履歴(No.12)