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, that is 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¶

• Jessie2 (git clone https://forge.ispras.ru/git/astraver.jessie2.git) has the following branches:
  -- master -- references the latest released version of the Jessie2 plugin (currently `alpha0'')
  -- alpha0 -- references the branch with the `alpha0'' released version of the plugin
  -- other branches are referencing the corresponding released versions
• QA is a submodule of the Jessie2 repository. It contains several new test sets and the corresponding new testing script (in OCaml) that is based on the usage of the Why3 proof replayer.
• Frama-C (git clone https://forge.ispras.ru/git/astraver.frama-c.git) has two branches:
  -- master -- this is a dummy branch with each commit corresponding to an upstream release of Frama-C starting from "Fluorine 3 20130601" (framac|16a2903f)
  -- 20140301 -- references the patched version of Frama-C Fluorine 3 20130601 which is required by Jessie2 (due to several small extensions to the ACSL specification language such as named string literals)
• Why3 (git clone https://forge.ispras.ru/git/astraver.why3.git) has two branches:
  -- master -- a periodically updated mirror of the INRIA official Why3 Git repository''s master branch
  -- patched -- the periodically merged patched version of the Why3 platform with several small unmerged changes (primarily explanation fixes)