CANAPA
From Arnout Engelen
Contents |
[edit] Description
CANAPA, like Houdini, invokes ESC/Java iteratively. Instead of, like Houdini, assuming that everything is non-null and working from there, it runs ESC/Java on the raw Java code, and tries to fix any warnings by doing some fairly conservative inferences. For example, it only works on method parameters, local variables and function results. It never infers the non-nullness of a class attribute.
[edit] Type of Reasoning
CANAPA runs ESC/Java and based on the errors produced by ESC/Java it does a basic dataflow analysis to add non-null annotations. This analysis might, however, add a non-null annotation to a variable that is only non-null under certain conditions.
Possible problem: a bug in the program, or nullness assumption that is correct but complex, might lead to incorrect non-null annotations. Must try and see if that's indeed so much of a problem in practice.
[edit] Scoping
CANAPA only regards method parameters, local variables and function results. This means the analysis can be broken down in small packages, which is a good way to keep the problem from getting out of hand. Changes are propagated across these boundaries because CANAPA performs multiple iterations of the analysis until it reaches a fixedpoint.
[edit] Use
CANAPA can be used as an ECLIPSE plugin. TODO.
[edit] Practical problems faced
- CANAPA adds annotations by parsing the code with JParse, inserting the annotation in the right place, and spitting out the pretty-printed code again. Unfortunately this implementation is overly complex and buggy - which was a pain since it broke the termination property. I replaced this with a Perl script, which is kindof ugly, but sufficient for testing.
- Added a run.sh script for starting Canapa on unix
[edit] Misc Notes
You can pass ESC/Java options directly to Canapa
[edit] Behaviour
For behaviour specific to running modularly, see Algorithm design.
