IRISA
Celtique Project

Nit: Nullability Inference Tool
-----------------------

Downloads

Nit 0.5 for Windows can be obtained here and OCaml sources can be obtained here.

About

Nit, the Nullability Inference Tool, infers nullness properties of variables and can prove that a program is NullPointerException free. It allows to find suitable nullability annotations for fields, method parameters, return values and local variables. It works at the bytecode level (on .class files or .jar files) so it can be used on programs where the source is not available. While this can look strange for a programmer, this tool can also be used by other static analyses to improve their precision.

It is developed by Laurent Hubert of project Celtique (formerly Lande) at IRISA.

License

This software is distributed under the GNU General Public License.

News

September 2009
Nit 0.5d is out. This is a bugfix release. Check the CHANGELOG file for all the details.
June 2009
Nit and the brand new Eclipse plugin are at JavaOne, at the INRIA booth.
June 2009
An Eclipse plugin is out. You can find it in the Nit/Eclipse section of the website.
May 2009
Nit 0.5 is out. The major improvements are:
  • the use of JavaLib 1.8 which improves the performances and the precision (call graph computed with RTA instead of CHA);
  • the addition of an output format compatible with the Annotation File Utilities (http://types.cs.washington.edu/annotation-file-utilities/), which should allow to export computed annotations back into the Java source code;
  • the compatibility with Cygwin, which allows to compile and use Nit on Microsoft Windows.
Check the CHANGELOG file for all the details.
October 2008
Nit 0.4 is out. The major improvement is in the use of JavaLib 1.7 which improves performances by more than 7% and reduce memory consumption. Some improvements have also been made on precision. Check the CHANGELOG file for all the details.
August 2008
Nit 0.3 is out. The precision has been greatly improved: the new must-alias analysis is more powerful and a new additional analysis allows to recover information from the instranceof instruction (do not worry if you do not understand: it just means it is more precise). The other good news: it uses even less memory in the general case.
June 2008
A brand new web site with a lot more than before in the documentation section.
June 2008
Nit 0.2 is out. This version contains much more documentation (which is easy as the previous ones were almost undocumented) and a bug found by Fausto Spoto in the statistics computation has been fixed.
May 2008
Nit 0.1.2 is out. It is a bug-fix version.
May 2008
Nit 0.1 is out. It is the first version publicly available.

Related publications

You can find here some publications at the origin of this software.
[1] Laurent Hubert. A Non-Null annotation inferencer for Java bytecode. In Proceedings of the Workshop on Program Analysis for Software Tools and Engineering (PASTE'08), pages 36-42. ACM, November 2008. [ slides | http | .pdf ]
We present a non-null annotations inferencer for the Java bytecode language. This paper proposes extensions to our former analysis in order to deal with the Java bytecode language. We have implemented both analyses and compared their behaviour on several benchmarks. The results show a substantial improvement in the precision and, despite being a whole-program analysis, production applications can be analyzed within minutes.

Keywords: Java, NonNull, annotation, inference, static analysis
[2] Laurent Hubert, Thomas Jensen, and David Pichardie. Semantic foundations and inference of non-null annotations. In Proceedings of the international conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS '08), volume 5051 of LNCS, pages 132-149. Springer Berlin, June 2008. [ slides | http | .pdf ]
This paper proposes a semantics-based automatic null pointer analysis for inferring non-null annotations of fields in object-oriented programs. We prove the analysis correct with respect to a semantics of a minimalistic OO language and complete with respect to the non-null type system proposed by Fähndrich and Leino, in the sense that for every typable program the analysis is able to prove the absence of null dereferences without any hand-written annotations. Experiments with a prototype implementation of the analysis show that the inference is feasible for large programs.

Keywords: Java, NonNull, annotation, inference, static analysis
[3] Laurent Hubert, Thomas Jensen, and David Pichardie. Semantic foundations and inference of non-null annotations. Research Report 6482, INRIA, March 2008. [ http ]
Last modification:
This website uses Google Analytics