> uberSpark (Composable Verification of Commodity System Software) Documentation

Software Requirements and Dependencies

We assume your are working in: /home/<home-dir>/<work-dir>

Replace <home-dir> with your home-directory name and <work-dir> with any working directory of your choice.

sudo apt-get update
sudo apt-get install git gcc binutils autoconf
sudo apt-get install lib32z1 lib32ncurses5 lib32bz2-1.0 gcc-multilib
sudo apt-get install ocaml ocaml-findlib ocaml-native-compilers
sudo apt-get install graphviz libzarith-ocaml-dev libfindlib-ocaml-dev
wget https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh -O - | sh -s /usr/local/bin
eval `opam config env`
opam switch 4.02.3
opam install menhir
opam install ocamlgraph
opam install ocamlfind
opam install coq
wget http://compcert.inria.fr/release/compcert-3.1.tgz
tar -xvzf compcert-3.1.tgz
cd CompCert-3.1
./configure x86_32-linux
make all
sudo make install
cd ..
wget http://frama-c.com/download/frama-c-Phosphorus-20170501.tar.gz
tar -xvzf frama-c-Phosphorus-20170501.tar.gz
cd frama-c-Phosphorus-20170501
sudo make install
cd ..