Adding a "LegalIntervals" annotation

Skip to first unread message

May 10, 2008, 11:19:59 AM5/10/08
to JSR-305: Annotations for Software Defect Detection

I am new to this JSR305 group.

I am working on defect detection techniques applied to several
programming environments, espacialy on underflow, overflow, DIV/0,
null checking, return value checking etc..

As in restricted languages (ADA for ex), it would be valuable both for
tools and for developpers to be able to specify the authorized values
for functions, arguments, variables.

For example a simple instruction like * on floats leads to an overflow
when both factors are over sqrt(Float.MAX_VALUE).

As a matter of fact up to now, there is no way to detect
"automatically" that this declaration (in :
public static native double cos(double a);
is in fact a value from -1.0 to 1.0, or NaN, mostly because native
declarations cannot be analyzed.

Adding annotation like for example public static native
@LegalIntervals {NaN;[-1.0, 1.0]} double cos(double a); would help
static analysis tools to detect that
float a;
float b = a*cos(a);
can never overflow

See for lots of tricky examples extracted from
Sun jdk6 packages.

This JSR305 sems to be closed now, may be for the future !!
Thanks for your attention.

Bill Pugh

May 27, 2008, 1:48:08 PM5/27/08
One issue with a LegalIntervals annotation is that much of the time
the bounds you would want to express wouldn't be constant.

For example, in List.get(i), you would like to express the fact the
bounds are 0 <= i < this.size().

I guess I'm unconvinced as to whether the ability to specify constant
bounds would be useful enough to warrant including in JSR-305. We will
include something to allow you to specific which arguments must be
nonnegative, which would probably handle about 95+% of the cases.


Reply all
Reply to author
0 new messages