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.

Development OS and Base Packages

You will need a working Ubuntu 16.04.x LTS 64-bit environment for development and verification. This can either be a Virtual Machine (VM) (e.g., VirtualBox) or a container (e.g., Windows WSL). As of this writing, the Ubuntu 16.04.x LTS VM ISO image is available at:

http://releases.ubuntu.com/16.04/ubuntu-16.04.6-desktop-amd64.iso

You will need to first perform an update to download the latest package lists from the repositories as shown below:

sudo apt-get update

After the update completes, you will need to install the following base packages required for development as shown below:

sudo apt-get install git gcc binutils autoconf
sudo apt-get install lib32z1 lib32ncurses5 gcc-multilib
sudo apt-get install ocaml ocaml-findlib ocaml-native-compilers
sudo apt-get install graphviz libzarith-ocaml-dev libfindlib-ocaml-dev
sudo apt-get install make unzip

Packages for Generating Documentation

Optionally, you will need to install Latex, Python and Sphinx in order to generate the documentation locally for überSpark. More specifically, you will need to perform the following operations:

sudo apt install python3 python3-pip
sudo apt install texlive-latex-recommended texlive-fonts-recommended
sudo apt install texlive-latex-extra latexmk
    pip3 install -U 'Sphinx==2.2.0'

OCaml Compiler and Base Packages

You will then need to install the OCaml Package manager as shown below:

wget https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh -O - | sh -s /usr/local/bin

After the OCaml Package Manager installs successfully, configure the opam environment and switch to the appropriate OCaml compiler version as shown below:

eval `opam config env`
opam switch 4.02.3

After the opam environment switch, install the following opam packages in order:

opam install zarith.1.3
opam install yojson.1.2.1
opam install menhir.20170712
opam install ocamlgraph.1.8.8
opam install ocamlfind.1.7.3

Coq Proof Assistant

The Coq Proof Assistant is a required package for both CompCert as well as Frama-C. You need to install the Coq Proof Assistant via opam as shown below:

opam install coq.8.6.1

CompCert Certified Compiler

The CompCert compiler is used to compile the C code for verified uberobjects within überSpark. The Compcert version currently supported is v3.0.1 and can be installed as shown below:

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 ..

Frama-C Verification Framework

The Frama-C verification framework is used to discharge uberobject invariants and properties within überSpark. The Frama-C version currently supported is Phosphorus-20170501 and can be installed as shown below:

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
./configure
make
sudo make install
cd ..

You will also need to install Frama-C backend theorem provers such as CVC3, Alt-Ergo and Z3. The WP Frama-C plugin manual referenced below contains a chapter on installing the theorem provers:

http://frama-c.com/download/wp-manual-Phosphorus-20170501.pdf

Note

You will need to install the correct versions of Why3 and the provers as described in the aforementioned Frama-C WP plugin manual. For example, Why3 version 0.87.3 and Alt-ergo version 1.30. This can be done via opam as shown below in the context of Why3:

opam install why3.0.87.3

Note

Opam might show instructions on how to install additional OS dependencies if needed during the installation of Why3 and the provers. Usually such dependencies are satisfied by using opam depext prior to installing Why3 and the provers. An example is shown below in the context of Why3:

opam depext camlzip.1.07
opam depext conf-pkg-config.1.1
opam depext conf-gtksourceview.2