Jessie2
(fork of the Jessie plugin for Frama-C)¶

Jessie2 is a fork of the Jessie plug-in that allows deductive verification of C programs annotated with ACSL and is primarily targeted at Linux kernel modules source code. It uses the language and tools of the Why3 verification platform. Unlike original Jessie, Jessie2 is not distributed as a part of the Why2 verification platform and is compiled/installed separately.
Note: For now, this fork requires modified version of the Frama-C source code analysis platform, based on the Neon 20140301 version of the original platform.

Installation¶

Using OPAM¶

• Install OPAM as described on the OPAM documentation.
  For example (installing to /usr/local/bin unsing the binary installer):
  

      wget https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh
      chmod +x opam_installer.sh
      sudo ./opam_installer.sh /usr/local/bin
      

• Initialize OPAM to use the OCaml 4.02.1 compiler:
  

      opam init --comp 4.02.1
      eval `opam config env`
      

• Install Git.
  For example on Ubuntu:
  

      sudo apt-get install git
      

• Add ISPRAS OPAM repository at https://forge.ispras.ru/git/astraver.opam-repository.git with Jessie2 and modified Frama-C Neon packages to the OPAM installation
  (ispras is just an arbitrary name of the new repository):
  

      opam repo add ispras https://forge.ispras.ru/git/astraver.opam-repository.git
      

• Install external dependencies for the Jessie2 and Frama-C build i.e. Autoconf, Gtk2 development files and M4.
  Ubuntu example:
  

      sudo apt-get install $(opam install -e ubuntu jessie2)
      

• Build and install the Jessie2 plugin for Frama-C with OPAM (the Frama-C itself will be built and installed automatically). One
  can use the -j option to speed-up compilation on a multi-core machine:
  

      opam install -j 4 jessie2
      

• Build and install either original or patched (negative assumption highlighting and minor explanation fixes) version of the Why3 verification platform:
  

      sudo apt-get install $(opam install -e ubuntu why3) # Install GMP (external dependency) on Ubuntu
      opam install -j 4 why3
      

• The one using Jessie would also likely need SMT solvers e.g. Alt-Ergo (also Z3, CVC4 and others). Alt-Ergo can be installed via OPAM:
  

       opam install alt-ergo altgr-ergo satML-plugin
      

• The Why3 IDE should be initialized to detect available provers (and plugins):
  

      why3 config --detect-provers --detect-plugins
      

Our Repositories¶