example.sh example/jdk/src/java/io/InputStream.java example/src/checkers/typestate/ioexample/Example1.java example/src/checkers/typestate/ioexample/Example2.java example/src/checkers/typestate/ioexample/InputStreamStates.java @@ -3,11 +3,11 @@ export PATH=/Users/adamw/jsr308/soylatte16-i386-1.0.3/bin:$PATH export CLASSPATH=/Users/adamw/jsr308/checkers/checkers.jar:/Users/adamw/jsr308/jsr308-typestate-checker/build export DEBUGOPTS="-J-Xms48m -J-Xdebug -J-Xrunjdwp:transport=dt_socket,server=y,suspend=y,address=5005" -CHECKER=checkers.nullness.NullnessChecker +#CHECKER=checkers.nullness.NullnessChecker #CHECKER=checkers.javari.JavariChecker -#CHECKER=checkers.typestate.TypestateChecker +CHECKER=checkers.typestate.TypestateChecker -#SOURCES=tests/work/work/Test3.java -SOURCES=src/checkers/typestate/Any.java +SOURCES=tests/work/work/Test1.java +#SOURCES=src/checkers/typestate/Any.java javac $DEBUGOPTS -processor $CHECKER -sourcepath src -cp $CLASSPATH -d build $SOURCES debug.sh @@ -152,7 +152,7 @@ public class TypestateFlow extends MainFlow { // First checking if we are in a try-catch-finally. If so, looking for an exception annotation. If // it is present, updating the try bits to be in the new state. - if (tryBits.size() > 0) { + if (tryBits.size() > 0 || catchBits.size() > 0) { AnnotationMirror exceptionAnnotation = typestateUtil.getExceptionParameterValue( declaredAnnotation); @@ -172,7 +172,13 @@ public class TypestateFlow extends MainFlow { if (elementIdx >= 0 && afterAnnotation != null && annotations.contains(afterAnnotation)) { // If the "after" annotation is a state annotation, changing the state of the // element in the flow. - clearStateAnnotation(declaredAnnotation, elementIdx, annos); + + // Clearing any of the old states + for (AnnotationMirror actualAnnotation : actualAnnotations) { + clearStateAnnotation(actualAnnotation, elementIdx, annos); + } + + // Setting the new state annos.set(annotationsTranslation.get(afterAnnotation), elementIdx); } } src/checkers/typestate/TypestateFlow.java @@ -6,7 +6,7 @@ export CLASSPATH=/Users/adamw/jsr308/checkers/checkers.jar:/Users/adamw/jsr308/j #CHECKER=checkers.javari.JavariChecker CHECKER=checkers.typestate.TypestateChecker -SOURCES=tests/work/work/Test3.java +SOURCES=tests/work/work/Test1.java #SOURCES=src/checkers/typestate/Any.java #SOURCES=tests/typestate/SimpleReceiverTransitionState.java test.sh @@ -9,14 +9,17 @@ public class AnyInMethodReceiverState { @State public static @interface State1 { public abstract Class<?> after() default NoChange.class; } @State public static @interface State2 { public abstract Class<?> after() default NoChange.class; } + // Helper with a given initial state public static class Helper { + public Helper() /*@State1*/ { } + public void onlyInState1() /*@State1*/ { } public void onlyInState2() /*@State2*/ { } public void transit() /*@Any(after=State2.class)*/ { } } - public void testOk() { + public void testOk1() { Helper h = new Helper(); h.transit(); h.onlyInState2(); @@ -32,4 +35,31 @@ public class AnyInMethodReceiverState { Helper h = new Helper(); h.onlyInState2(); // error } + + // Helper without an initial state + public static class Helper2 { + public Helper2() { } + + public void onlyInState1() /*@State1*/ { } + public void onlyInState2() /*@State2*/ { } + + public void transit() /*@Any(after=State2.class)*/ { } + } + + public void testOk2() { + Helper2 h = new Helper2(); + h.transit(); + h.onlyInState2(); + } + + public void testError3() { + Helper2 h = new Helper2(); + h.transit(); + h.onlyInState1(); // error + } + + public void testError4() { + Helper2 h = new Helper2(); + h.onlyInState2(); // error + } } \ No newline at end of file tests/typestate/AnyInMethodReceiverState.java @@ -1,2 +1,4 @@ -:28: (receiver.in.wrong.state) -:33: (receiver.in.wrong.state) +:31: (receiver.in.wrong.state) +:36: (receiver.in.wrong.state) +:58: (receiver.in.wrong.state) +:63: (receiver.in.wrong.state) tests/typestate/AnyInMethodReceiverState.out @@ -9,7 +9,7 @@ public class AnyInParameterState { @State public static @interface State1 { public abstract Class<?> after() default NoChange.class; } @State public static @interface State2 { public abstract Class<?> after() default NoChange.class; } - public static class Helper { } + public static class Helper { public Helper() /*@State1*/ { } } public void acceptHelperInState1(@State1 Helper h) { } public void acceptHelperInState2(@State2 Helper h) { } tests/typestate/AnyInParameterState.java @@ -23,14 +23,12 @@ public class Test1 { public void test() { Test2 o = new Test2(); try { - acceptInState1(o); - throwException(o); - acceptInState2(o); - } catch(Exception e) { - acceptInErrorState(o); - return; + o.read(); + } finally { + o.transit(); } - acceptInState2(o); + + acceptInState1(o); } public static void main(String[] args) { } @@ -38,4 +36,8 @@ public class Test1 { class Test2 { public Test2() /*@State1*/ { } + + void read() /*@State1*/ { } + + void transit() /*@Any(after=State2.class)*/ { } } tests/work/work/Test1.java 2193f552fa5ac47366df554d0dc0cb6601d986d9 Adam Warski adam@warski.org http://github.com/adamw/jsr308-typestate-checker/commit/80894c97ce345bf833a7df6fb9079ec66d7f0c89 80894c97ce345bf833a7df6fb9079ec66d7f0c89 2009-04-14T09:10:24-07:00 2009-04-14T09:10:24-07:00 Fixing bugs, adding InputStream example 2788747f1b0e04a57f0582398f71915ae603ff75 Adam Warski adam@warski.org