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