Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

The Caml Hump: Programming languages :: Program analysis


Scientific papers
A generic abstract interpreter [10-Aug-2001, Stable]
We present in extenso the calculation-based development of a generic compositional reachability static analyzer for a simple imperative programming language by abstract interpretation of its formal rule-based/structured small-step operational semantics.
Author: Patrick Cousot.
Scientific software
CCured [26-May-2003, version 1.2.5, Stable] Has a documentation
CCured is a source-to-source translator for C. It analyzes the C program to determine the smallest number of run-time checks that must be inserted in the program to prevent all memory safety violations.
Scientific software
CIL [21-Aug-2002, version 1.3.7, Stable] Has a Godi packageHas a documentation
CIL (C Intermediate Language) is a high-level representation along with a set of tools that permit easy analysis and source-to-source transformation of C programs.
Native OCaml libraries
JavaLib and Sawja [08-Oct-2012, version 2.2.2/1.4, Stable] Has a documentationHas a tutorial
manipulate, and generate valid .class files.Sawja is a library relying on Javalib to provide a high level representation of Java bytecode programs. Its name stands for Static Analysis Workshop for Java. Whereas Javalib is dedicated to isolated classes, Sawja handles bytecode programs with their class hierarchy and control flow algorithms. Moreover, Sawja provides some stackless intermediate representations of code. The transformation algorithm, common to these representations, has been formalized and proved to be semantics-preserving.An Eclipse plugin for Sawja analyses is also available: it allows developers to add an analysis in Eclipse without requiring any additional Java code generation.
Development tools
Jsure [11-Mar-2008, version 1.0.1, Stable] Has a documentation
Jsure is a "lint" for Javascript, which is also known as Ecmascript. It checks syntax and a little bit of semantics.
Author: Berke Durak.
Development tools
OCamlexc [10-Aug-2001, Stable] Has a documentation
A static analyzer of spurious exceptions of OCaml programs.
Development tools
Oug [01-Jul-2010, version 2.0-alpha, Stable] Has a tutorial
Oug is a code analysis tool building reference graphs from OCaml code, that is graphs representing which elements (value, module, class, ...) reference which elements. It comes with the Ouglib library to be able to embed the analyzer in other OCaml applications. From the graph, various outputs can be obtained: list of elements not referenced anywhere (useless elements and so potential dead code), various graphiz graphs, ...
Author: Maxence Guesdon.
Scientific software
Why [29-Sep-2003, version 1.42, Stable] Has a documentation
Why is a software verification tool. Why aims at being a verification conditions generator (VCG) back-end for other verification tools. It provides a powerful input language including higher-order functions, polymorphism, references, arrays and exceptions. It generates proof obligations for many systems: the proof assistants Coq, PVS, HOL Light, Mizar and the decision procedures haRVey and Simplify.


Development tools
AlphaCaml [10-Jun-2005, Beta] Has a Godi packageHas a documentation
AlphaCaml is a tool that turns a so-called ``binding specification'' into an Objective Caml compilation unit. This helps writers of interpreters, compilers, or other programs-that-manipulate-programs deal with alpha-conversion in a safe and concise style.
Scientific software
EasyLanguage to C# translator [25-May-2007, Beta]
An EasyLanguage ( to C# translator.
Author: Joël Reymond.
Scientific software
Flow Caml [03-Jul-2003, version 1.03, Beta] Has a documentationHas a tutorial
A prototype implementation of an information flow analyzer for the Caml language.
Author: Vincent Simonet.
Scientific software
Frama-C [25-Aug-2010, version Boron-20100401, Beta]
Frama-C is a suite of tools dedicated to the analysis of the source code of software written in C.
Author: Frama-C Development team (CEA LIST and INRIA Saclay).
Development tools
OCaml Metrics [02-Jun-2009, version 0.51, Beta]
OCaml Metrics is a simple OCaml code analysis tool. It can compute some metrics of functions and modules: cyclomatic complexity, the number of lines of code, Halstead complexity measures (difficulty, volume and effort) and Maintainability Index. OCaml Metrics generates reports in three formats: HTML, simple XML or plain text. This allows developers to find parts of their projects which need refactoring in order to keep the projects easily maintainable.
Development tools
Olmar [06-Nov-2006, version 0.2, Beta]
Olmar connects Elsa, the Elkhound based C/C++ parser and typechecker, with Ocaml. More precisely, the Olmar extension can translate Elsa's internal abstract syntax tree into a value of an Ocaml variant type. This value can then be further processed with a pure Ocaml program. I prefer to have standalone Ocaml programs. Therefore I let Elsa marshal the abstract syntax tree as an Ocaml value to disk. However, it is also possible to link the Ocaml code into the Elsa executable.
Author: Hendrik Tews.
Scientific software
Phpsa [03-Apr-2006, version 0.1.1, Beta] Has a documentation
PHP string analyzer is a static program analyzer that approximates the string output of a PHP program with a context-free grammar. The analyzer can be used to check properties of a PHP program. For example, it can be used to validate dynamically generated Web pages by a PHP program.
Native OCaml libraries
Yacfe [03-Nov-2008, version 0.2, Beta]
Yet Another C/C++ Front-End, which is an OCaml API to write style-preserving source-to-source transformations such as refactorings on C or C++ source code.
Author: Yoann Padioleau.

Development code

Development tools
DiamondBack Ruby [05-May-2009, version 20090421, Development code] Has a documentationHas a tutorial
Diamondback Ruby (DRuby) is an extension to Ruby that aims to bring the benefits of static typing to Ruby without compromising the expressiveness of the language.
Camlp4 extensions
OCaml-ast-analyze [19-Apr-2005, version 0.1.1, Development code]
Ocaml-ast-analyze should provide an abstraction of the structure required to build pr_*.cmo module for camlp4. The idea is to provide a simple way to build Ocaml abstract syntax tree analyzer. This should be particularly useful for string extraction of Ocaml source code.
Author: Sylvain Le Gall.