The Caml Hump: Programming languages :: Program analysis

A prototype implementation of an information flow analyzer for the Caml language.

Frama-C is a suite of tools dedicated to the analysis of the source code of software written in C.

Jsure is a "lint" for Javascript, which is also known as Ecmascript. It checks syntax and a little bit of semantics.

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.

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.

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

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.

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.

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.

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.

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.

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.

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.

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.

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.

An EasyLanguage (http://lambda-the-ultimate.org/node/2201) to C# translator.

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.

A static analyzer of spurious exceptions of OCaml programs.