Presentation

MLcov is a code coverage tool for Objective Caml programs.
It relies on a source code instrumentation technique which allows measuring of Modified Condition/Decision Coverage (MC/DC), the criterion involved in the DO-178B standard to ensure that safety-critical software is tested adequately.

The tool is available as a patch against the version 3.12.0 of the Objective Caml compiler sources.
It is distributed under the CeCILL-B license and is copyrighted by Esterel Technologies.

• Latest version: MLcov 1.2 (2010-11-24)

Build the tool

In this guide, we assume that the user has access to a UNIX shell providing the wget, patch and make commands.
We also assume that you have OCaml 3.12.0 installed, as it may not build with an other version of OCaml...

• The first step is to download and unpack the compiler:
  

  wget http://caml.inria.fr/pub/distrib/ocaml-3.12/ocaml-3.12.0.tar.bz2
  tar xjf ocaml-3.12.0.tar.bz2

• Then download the patch and apply it:
  

  wget http://www.algo-prog.info/mlcov/mlcov-1.2.patch.gz
  gzip -d mlcov-1.2.patch.gz
  cd ocaml-3.12.0
  patch -p1 < ../mlcov-1.2.patch

• Finally, build and install the tool:
  

  touch .depend
  make depend
  make
  sudo make install

Use the tool

Now that we have compiled MLcov, let's try it on a little example!

• For instance, we will use a little solver for the N queens problem (written by Pierre Weis):
  

  wget http://www.algo-prog.info/mlcov/queens.ml

• We instrument the code and compile the instrumented program:
  

  ocamlopt -c -pp mlcov queens.ml
  ocamlopt unix.cmxa mlcovTrace.cmx queens.cmx -o queens_instr

• Then, we can run the instrumented program, process the trace and examine the results:
  

  ./queens_instr
  mlcov -html queens.mlcov
  firefox queens_annot.html queens_summary.html

MLcov is currently used by Esterel Technologies as a verification tool for the certification of a DO-178B level A code generator written in Objective Caml.

Documentation

For more information about MLcov, please consult the PDF documentation:

• MLcov 1.2 - User guide

For further details on the instrumentation algorithm or the use of MLcov in a DO-178B process, you may refer to the following papers:

• Bruno Pagano, Olivier Andrieu, Thomas Moniot, Benjamin Canou, Emmanuel Chailloux, Philippe Wang, Pascal Manoury, Jean-Louis Colaço
  Experience Report: Using Objective Caml to Develop Safety-Critical Embedded Tools in a Certification Framework
  In International Conference on Functional Programming 2009. Proceedings of the 14th ACM SIGPLAN international conference on Functional programming, pp. 215-220.
  http://doi.acm.org/10.1145/1596550.1596582 - ISBN: 978-1-60558-332-7.

• Bruno Pagano, Olivier Andrieu, Benjamin Canou, Emmanuel Chailloux, Jean-Louis Colaço, Thomas Moniot, Philippe Wang
  Certified development tools implementation in Objective Caml (PDF)
  In Practical Aspects of Declarative Languages 2008. Lecture Notes in Computer Science, vol. 4902, pp. 2-17.
  http://dx.doi.org/10.1007/978-3-540-77442-6_2 © Springer-Verlag Berlin Heidelberg 2008.

• Bruno Pagano, Benjamin Canou, Emmanuel Chailloux, Jean-Louis Colaço, Philippe Wang
  Couverture de code Caml pour la réalisation d'outils de développement certifiés (PDF)
  In Journées Francophones des Langages Applicatifs 2007.

Related work: you can also try out ZAMcov for non-intrusive code coverage of Objective Caml programs.

Contact

Main developer: Thomas Moniot.
You can contact me by email:

Bug reports, remarks and questions are welcome!