Celtique Project
| About |
| Downloads |
| Documentation |
| Nit/Eclipse |
| FAQ |
| Contacts |
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.
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 ] |