Today I finished generalizing the annotations that pass method arguments as arrays and provide OnlySynchronizedArgument
, NotSynchronizedArgument
, OnlyNullArgument
, NotNullArgument
annotations, and perhaps something more unusual, NumberBoundedArgument
, along with the matching Any
, All
and None
combinations.
Just like all the annotations named above, NumberBoundedArgument
lets you specify the index of the argument you want checked, and then it lets you select several modes:
LESS
, i.e.arg < bound
LESS_EQ
, i.e.arg <= bound
GREATER
, i.e.arg > bound
GREATER_EQ
, i.e.arg >= bound
IN
, i.e.(arg > bound) && (arg < upperBound)
IN_EQ
, i.e.(arg >= bound) && (arg <= upperBound)
OUT
, i.e.(arg < bound) || (arg > upperBound)
OUT_EQ
, i.e.(arg <= bound) || (arg >= upperBound)
where arg
is the argument being compared, bound
is one of the bounds
(either the upper bound for LESS
, LESS\_EQ
, IN
, and IN\_EQ
; or upper bound for GREATER
and GREATER\_EQ
), and upperBound
is the upper bound for IN
, IN\_EQ
, GREATER
and GREATER\_EQ
.
I decided to use bound
both as upper and lower bound for those annotations that only use one bound as that was less confusing. Otherwise, I'd have to remember whether I set ubound
or lbound
for LESS
.
I have also finished XML importing and exporting so that it supports passing arguments, and I fixed a bug that didn't properly join predicate annotations if the invariant was repeated several times.
I also improved violation reporting: If method arguments are passed, then the actual values will also appear in the violation log.
Consider the following nice program that uses NumberBoundedArgument
:
package sample.threadCheck.predicate;
import edu.rice.cs.cunit.threadCheck.predicates.NumberBoundedArgument;
public class TCSample17 {
public static void main(String[] args) {
TCSample17 o = new TCSample17();
System.out.println("main!");
o.succeeds();
o.fails();
System.out.println("end main!");
}
void succeeds() { // these invariants all succeed
lt(0); ltEq(0);
gt(0); gtEq(0);
in(0); inEx(0);
out(0); outEx(3);
}
void fails() { // these invariants all fail
lt(2); ltEq(2);
gt(-1); gtEq(-2);
in(1); inEx(1);
out(2); outEx(0);
}
@NumberBoundedArgument(
mode=NumberBoundedArgument.Mode.LESS,
index = 0, bound = 1)
void lt(int i) {
System.out.println("lt, i = "+i);
}
@NumberBoundedArgument(
mode=NumberBoundedArgument.Mode.LESS\_EQ,
index = 0, bound = 0)
void ltEq(int i) {
System.out.println("ltEq, i = "+i);
}
@NumberBoundedArgument(mode=NumberBoundedArgument.Mode.GREATER,
index = 0,
bound = -1)
void gt(int i) {
System.out.println("gt, i = "+i);
}
@NumberBoundedArgument(
mode=NumberBoundedArgument.Mode.GREATER\_EQ,
index = 0, bound = 0)
void gtEq(int i) {
System.out.println("gtEq, i = "+i);
}
@NumberBoundedArgument(
mode=NumberBoundedArgument.Mode.IN\_EQ,
index = 0, bound = 0, upperBound = 0)
void in(int i) {
System.out.println("in, i = "+i);
}
@NumberBoundedArgument(
mode=NumberBoundedArgument.Mode.IN,
index = 0, bound = -1, upperBound = 1)
void inEx(int i) {
System.out.println("inEx, i = "+i);
}
@NumberBoundedArgument(
mode=NumberBoundedArgument.Mode.OUT\_EQ,
index = 0, bound = 1, upperBound = 3)
void out(int i) {
System.out.println("out, i = "+i);
}
@NumberBoundedArgument(mode=NumberBoundedArgument.Mode.OUT,
index = 0, bound = 0, upperBound = 2)
void outEx(int i) {
System.out.println("outEx, i = "+i);
}
}
When executed, it produces the following log file:
======================================== Log opened 2007-03-05, 02:44:17 CST (GMT-5) ---------------------------------------- Thread Predicate Violation: (9 checks, 1 violation) Current thread 'main', id 1, group 'main' Violated predicate @edu.rice.cs.cunit.threadCheck.predicates.NumberBoundedArgument Method arguments '2' : java.lang.Integer at sample.threadCheck.predicate.TCSample17.lt (TCSample17.java:43) at sample.threadCheck.predicate.TCSample17.fails (TCSample17.java:31) at sample.threadCheck.predicate.TCSample17.main (TCSample17.java:13) ---------------------------------------- Thread Predicate Violation: (10 checks, 2 violations) Current thread 'main', id 1, group 'main' Violated predicate @edu.rice.cs.cunit.threadCheck.predicates.NumberBoundedArgument Method arguments '2' : java.lang.Integer at sample.threadCheck.predicate.TCSample17.ltEq (TCSample17.java:48) at sample.threadCheck.predicate.TCSample17.fails (TCSample17.java:32) at sample.threadCheck.predicate.TCSample17.main (TCSample17.java:13) ---------------------------------------- Thread Predicate Violation: (11 checks, 3 violations) Current thread 'main', id 1, group 'main' Violated predicate @edu.rice.cs.cunit.threadCheck.predicates.NumberBoundedArgument Method arguments '-1' : java.lang.Integer at sample.threadCheck.predicate.TCSample17.gt (TCSample17.java:53) at sample.threadCheck.predicate.TCSample17.fails (TCSample17.java:33) at sample.threadCheck.predicate.TCSample17.main (TCSample17.java:13) ---------------------------------------- Thread Predicate Violation: (12 checks, 4 violations) Current thread 'main', id 1, group 'main' Violated predicate @edu.rice.cs.cunit.threadCheck.predicates.NumberBoundedArgument Method arguments '-2' : java.lang.Integer at sample.threadCheck.predicate.TCSample17.gtEq (TCSample17.java:58) at sample.threadCheck.predicate.TCSample17.fails (TCSample17.java:34) at sample.threadCheck.predicate.TCSample17.main (TCSample17.java:13) ---------------------------------------- Thread Predicate Violation: (13 checks, 5 violations) Current thread 'main', id 1, group 'main' Violated predicate @edu.rice.cs.cunit.threadCheck.predicates.NumberBoundedArgument Method arguments '1' : java.lang.Integer at sample.threadCheck.predicate.TCSample17.in (TCSample17.java:63) at sample.threadCheck.predicate.TCSample17.fails (TCSample17.java:35) at sample.threadCheck.predicate.TCSample17.main (TCSample17.java:13) ---------------------------------------- Thread Predicate Violation: (14 checks, 6 violations) Current thread 'main', id 1, group 'main' Violated predicate @edu.rice.cs.cunit.threadCheck.predicates.NumberBoundedArgument Method arguments '1' : java.lang.Integer at sample.threadCheck.predicate.TCSample17.inEx (TCSample17.java:68) at sample.threadCheck.predicate.TCSample17.fails (TCSample17.java:36) at sample.threadCheck.predicate.TCSample17.main (TCSample17.java:13) ---------------------------------------- Thread Predicate Violation: (15 checks, 7 violations) Current thread 'main', id 1, group 'main' Violated predicate @edu.rice.cs.cunit.threadCheck.predicates.NumberBoundedArgument Method arguments '2' : java.lang.Integer at sample.threadCheck.predicate.TCSample17.out (TCSample17.java:73) at sample.threadCheck.predicate.TCSample17.fails (TCSample17.java:37) at sample.threadCheck.predicate.TCSample17.main (TCSample17.java:13) ---------------------------------------- Thread Predicate Violation: (16 checks, 8 violations) Current thread 'main', id 1, group 'main' Violated predicate @edu.rice.cs.cunit.threadCheck.predicates.NumberBoundedArgument Method arguments '0' : java.lang.Integer at sample.threadCheck.predicate.TCSample17.outEx (TCSample17.java:78) at sample.threadCheck.predicate.TCSample17.fails (TCSample17.java:38) at sample.threadCheck.predicate.TCSample17.main (TCSample17.java:13)
This is a lot more informative than it used to be.