diff --git a/latte/src/main/java/typechecking/LatteTypeChecker.java b/latte/src/main/java/typechecking/LatteTypeChecker.java index 3bec793..586667c 100644 --- a/latte/src/main/java/typechecking/LatteTypeChecker.java +++ b/latte/src/main/java/typechecking/LatteTypeChecker.java @@ -534,11 +534,21 @@ public void visitCtIf(CtIf ifElement) { PermissionEnvironment thenPermEnv = permEnv.cloneLast(); exitScopes(); - enterScopes(); - super.visitCtBlock(ifElement.getElseStatement()); - SymbolicEnvironment elseSymbEnv = symbEnv.cloneLast(); - PermissionEnvironment elsePermEnv = permEnv.cloneLast(); - exitScopes(); + SymbolicEnvironment elseSymbEnv; + PermissionEnvironment elsePermEnv; + + if (ifElement.getElseStatement() != null) { + //Else statement + enterScopes(); + super.visitCtBlock(ifElement.getElseStatement()); + elseSymbEnv = symbEnv.cloneLast(); + elsePermEnv = permEnv.cloneLast(); + exitScopes(); + } else { + //No Else statement + elseSymbEnv = symbEnv.cloneLast(); + elsePermEnv = permEnv.cloneLast(); + } joining(thenSymbEnv, thenPermEnv, elseSymbEnv, elsePermEnv); } diff --git a/latte/src/test/examples/MyNodeAllKindsIfs.java b/latte/src/test/examples/MyNodeAllKindsIfs.java new file mode 100644 index 0000000..f11ce1f --- /dev/null +++ b/latte/src/test/examples/MyNodeAllKindsIfs.java @@ -0,0 +1,43 @@ +package latte; + +import specification.Free; +import specification.Unique; + +/* + * This file is part of the Latte test suite. + */ +class MyNode { + + @Unique Object value; + @Unique Node next; + + /** + * Constructor for the Node class using @Free value and next nodes + * @param value + * @param next + */ + public MyNode (@Free Object value, @Free Node next) { + this.value = value; + this.next = next; + } + + public Object test(@Free Object v1, @Free Object v2, boolean c1, boolean c2){ + if (c1) { + this.value = v1; + } else if (c2) { + this.value = v2; + } else { + this.value = v1; + } + + if (c2 || this.value == null) { + this.value = v1; + } else { + this.value = v2; + } + if (c1 && this.value == v1) { + this.value = v2; + } + return this.value; + } +} diff --git a/latte/src/test/examples/MyNodeIfNoElse.java b/latte/src/test/examples/MyNodeIfNoElse.java new file mode 100644 index 0000000..cd23a6c --- /dev/null +++ b/latte/src/test/examples/MyNodeIfNoElse.java @@ -0,0 +1,30 @@ +package latte; + +import specification.Free; +import specification.Unique; + +/* + * This file is part of the Latte test suite. + */ +class MyNode { + + @Unique Object value; + @Unique Node next; + + /** + * Constructor for the Node class using @Free value and next nodes + * @param value + * @param next + */ + public MyNode (@Free Object value, @Free Node next) { + this.value = value; + this.next = next; + } + + public Object test(@Free Object v1, boolean c1){ + if (c1) { + this.value = v1; + } + return this.value; + } +} diff --git a/latte/src/test/examples/MyNodeIfPermissionCheck.java b/latte/src/test/examples/MyNodeIfPermissionCheck.java new file mode 100644 index 0000000..de79418 --- /dev/null +++ b/latte/src/test/examples/MyNodeIfPermissionCheck.java @@ -0,0 +1,20 @@ +package latte; + +import specification.Free; +import specification.Unique; + +class MyNodeIfNoElse { + + @Unique Object value; + + public @Unique Object test(@Free Object v1, boolean cond) { + Object n; + n = new Object(); + + this.value = n; + if (cond) { + this.value = v1; + } + return this.value; // should still be @Unique + } +} \ No newline at end of file diff --git a/latte/src/test/examples/MyNodeIncorrectIfPermission.java b/latte/src/test/examples/MyNodeIncorrectIfPermission.java new file mode 100644 index 0000000..ab77a4e --- /dev/null +++ b/latte/src/test/examples/MyNodeIncorrectIfPermission.java @@ -0,0 +1,23 @@ +package latte; + +import specification.Free; +import specification.Unique; +import specification.Shared; +import specification.Borrowed; + +class MyNodeIfNoElse { + + @Unique Object value; + + public @Unique Object test(@Shared Object v1, boolean cond) { + Object n; + n = new Object(); + + this.value = n; + if (cond) { + this.value = v1; + } + + return this.value; + } +} \ No newline at end of file diff --git a/latte/src/test/java/AppTest.java b/latte/src/test/java/AppTest.java index 5a47da7..3bd77b0 100644 --- a/latte/src/test/java/AppTest.java +++ b/latte/src/test/java/AppTest.java @@ -41,6 +41,9 @@ private static Stream provideCorrectTestCases() { Arguments.of("src/test/examples/searching_state_space/ResultSetNoNext.java"), Arguments.of("src/test/examples/searching_state_space/ResultSetForwardOnly.java"), Arguments.of("src/test/examples/stack_overflow/MediaRecord.java"), + Arguments.of("src/test/examples/MyNodeAllKindsIfs.java"), + Arguments.of("src/test/examples/MyNodeIfNoElse.java"), + Arguments.of("src/test/examples/MyNodeIfPermissionCheck.java"), Arguments.of("src/test/examples/MyNodeInvocationIf.java"), Arguments.of("src/test/examples/MyNodeIfInvocationPermission.java") ); @@ -62,7 +65,8 @@ private static Stream provideIncorrectTestCases() { Arguments.of("src/test/examples/SmallestIncorrectExample.java", "UNIQUE but got BORROWED"), Arguments.of("src/test/examples/MyStackFieldAssignMethod.java", "UNIQUE but got SHARED"), Arguments.of("src/test/examples/FieldAccessNoThis.java", "UNIQUE but got SHARED"), - Arguments.of("src/test/examples/FieldAccessRightNoThis.java", "FREE but got UNIQUE") + Arguments.of("src/test/examples/FieldAccessRightNoThis.java", "FREE but got UNIQUE"), + Arguments.of("src/test/examples/MyNodeIncorrectIfPermission.java", "Expected UNIQUE but got SHARED") ); }